# Multiplicative Pure Type Systems

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?

• Can you give a reference to what "multiplicative" and "additive" rules for natural deduction are? If you are talking about linear logic, you should say so. "Natural deduction" in this context and without further caveats implies that you are talking about intuitionistic logic. – Andrej Bauer Oct 17 '18 at 21:12
• @AndrejBauer: For example, the elimination rule of the implication for intutionistic logic in Troelstra and Schwichtenberg's book (2nd ed., p. 41) is presented like that: premises are \Gamma => A -> B and \Delta => A, conclusion is \Gamma \Delta => B (it is "multiplicative"); the elimination rule of the implication for the STLC in Barendregt-Dekkers-Statman's book (p. 10), premises are \Gamma \vdash M: (A \to B) and \Gamma \vdash N: A, conclusion is \Gamma \vdash (MN): B (it is "additive" - same context in the premises). PTS's are usually presented with "additive" rules. – user251130 Oct 17 '18 at 21:43
• In Andromeda we use the multiplicative version. The upcoming new version will still be closer to the multiplicative formulation, but we threw out explicitly given contexts, as it is a pain to calculate the consistent unions all the time. – Andrej Bauer Oct 18 '18 at 6:57

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.