Multiplicative Pure Type Systems

Question

All the references about Pure Type Systems I know consider only systems that allow to recover natural deduction systems with additive rules. Is there any variant that allows it to recover natural deduction systems with multiplicative rules? Otherwise, is it just by tradition or by inclination that such a Pure Type System is never considered, or is there any good and deep reason why it is not considered?

Answer 1

The rule from Troelstra and Schwichtenberg that you call multiplicative, namely $$\frac{\Gamma \vdash A \Rightarrow B \qquad \Delta \vdash A}{\Gamma \cup \Delta \vdash B} \tag{1}$$ is equivalent to the additive formulation because we have weakening. More precisely, the multiplicative and the additive formulations prove the same judgements. In one direction, it is obvious that the additive version $$\frac{\Theta \vdash A \Rightarrow B \qquad \Theta \vdash A}{\Theta \vdash B} \tag{2}$$ follows from the above multiplicative one, just take $\Gamma = \Delta = \Theta$. In the other direction we can use weakening: assuming there are derivations of $$\Gamma \vdash A \Rightarrow B \qquad\text{and}\qquad \Delta \vdash A$$ then by weakening there are derivations of $$\Gamma \cup \Delta \vdash A \Rightarrow B \qquad\text{and}\qquad \Gamma \cup \Delta \vdash A$$ and then by the additive rule (2) we get the desired conclusion $$\Gamma \cup \Delta \vdash B.$$ So for the most part the difference in formulation is largely stylistic, although the difference may matter when we consider proof complexity, and other apsects of derivations, apart from just derivability.

Let me also say that from the semantic point of view it is a bit simpler to give the semantics of the additive formulation than the multiplicative one. In the additive rule one has to cope with the question on how the meaning of $\Gamma \vdash \mathcal{J}$ for some judgement $\mathcal{J}$ relates to $\Gamma \cup \Delta \vdash \mathcal{J}$. No such consideration is necessary in the additive formulation.