A typed calculus based on a fragment of linear logic (Q908909)

The author considers the so-called multiplicative second order linear logic \(LL^*\) (cf. LL in \textit{J.-Y. Girad}'s ``Linear logic'' [ibid. 50, 1-102 (1987; Zbl 0625.03037)]) in sequent and natural deduction form. Logical symbols of \(LL^*\) are the propositional connectives \(\otimes\), \(\cup\) and the quantifiers \(\forall\), \(\exists\) over propositional variables. The negation \(A^{\perp}\) is defined formally via de Morgan laws for \(\otimes\), \(\cup\) and \(\forall\), \(\exists\). It is supposed that each propositional variable X has its dual \(X^{\perp}\) so that \(X^{\perp \perp}\equiv X\). The corresponding natural deduction system is based on the notion of proof-net instead of proof-tree so that there is no strong distinction between assumptions and conclusions, and axiom links \(\overline{A A}^{\perp}\) are used in these nets. Then \(\nu\)- calculus is introduced whose terms are canonical representations of proofs. Each typed term has the general form \(\nu \bar w.\bar t:\bar A\) where \(\bar w\) is a list of pair variables \(x^ A\), \(y^{A^{\perp}}\) declared to be linked in \(\bar t,\) and \(\bar t\) is a list of terms of corresponding types \(\bar A.\) The symbol CUT may occur in \(\bar A.\) Term formation rules correspond to sequent rules: \(\vdash \nu xy.x^ A,y^{A^{\perp}}:A,A^{\perp};\) \(\vdash \nu \bar w_ 1.\bar t',a:\Gamma,A\) \(\vdash \nu \bar w_ 2.\bar t'',b:\Delta,B/\vdash \nu \bar w_ 1,\bar w_ 2.\bar t',\bar t'',a\times b:\Gamma,\Delta,A\otimes B;\) \(\vdash \nu \bar w.\bar t,a,b:\Gamma,A,B/\vdash \nu \bar w.\bar t,a\cup b:\Gamma,A\cup B;\) \(\vdash \nu \bar w_ 1.\bar t',a:\Gamma,A^{\perp}\) \(\vdash \nu \bar w_ 2.\bar t'',b:\Delta,A/\vdash \nu \bar w_ 1,\bar w_ 2.\bar t',a*b:\Gamma,\Delta,CUT;\) \(\vdash \nu \bar w.\bar t,a:\Gamma,A(X)/\vdash \nu \bar w.\bar t,\lambda X.a:\Gamma,\forall X.A(X);\) \(\vdash \nu \bar w.\bar t,a:\Gamma,A(B)/\vdash \nu \bar w.\bar t,\epsilon (X.a,B):\Gamma,\exists X.A(X).\) Strong normalization and Church-Rosser properties of the corresponding reduction rules are stated. It is argued that \(\nu\)-calculus gives a better comprehension of the computational aspects of the process of cut elimination and that a computational constructive interpretation of the proof of a linear implication \(A-\circ B\equiv A^{\perp}\cup B\equiv B^{\perp}-\circ A^{\perp}\) is not simply a function, but should be a more general object.