3
$\begingroup$

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?

$\endgroup$
  • 2
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer Oct 17 '18 at 21:12
  • $\begingroup$ @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. $\endgroup$ – user251130 Oct 17 '18 at 21:43
  • $\begingroup$ 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. $\endgroup$ – Andrej Bauer Oct 18 '18 at 6:57
3
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ My question was about Pure Type Systems, and not about intuitionistic propositional logic. Pure Type Systems are a generalization of natural deduction for Simply Typed Lambda Calculus. Your argument for intuitionistic logic works for STLC, but I was wondering if it can be generalized to Pure Type Systems (which might contain dependent types for instance). I do not see any obstruction, but since I did not see it anywhere, I thought that perhaps there was some trap. The weakening is constraint in PTS's. Perhaps the rule with premises G |- A:B and D |- C:s and conclusion G D x:C |- A:B is sound. $\endgroup$ – user251130 Oct 18 '18 at 21:29
  • $\begingroup$ Andromeda is an extensional dependent type theory with multiplicative rules. The union of contexts becomes more complicated. More or less we represent contexts as directed graphs and when we join them we have to check that no dependency cycles have been introduced. I don’t know how much of this carries over to PTS but I wouldn’t recommend using it. It’s a pain in the neck to implement. A newer version of Andromeda side-steps the issue by not having explicit contexts. $\endgroup$ – Andrej Bauer Oct 19 '18 at 6:43

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.