On the meaning of logical rules. II: Multiplicatives and additives (Q2752054)

Following the ideas presented and discussed in Part I [NATO ASI Ser., Ser. F, Comput. Syst. Sci. 165, 215-272 (1999; Zbl 0962.03055)], the author develops an ``interactive explanation'' of the fragment of linear logic built from the neutral elements \(1\), \(\top\), \(0\), \(\bot\) (the linear version of the constants \(T\) and \(F\) of classical logic) by means of the multiplicative and additive connectives \(\otimes\), \(\&\), \(\oplus\), \(\wp\) (the linear version of classical conjuction and disjunction). NEWLINENEWLINENEWLINEIn the first part of the paper, it is shown how the properties of focalization and reversion allow us to represent proofs and paraproofs (that is ``proofs with paralogisms'') as alternations of positive and negative clusters of rules. This leads the author to introduce the Hypersequentialized Calculus HC. One should notice that HC is a sequential way to internalize focalization and reversion. Nothing prevents (in principle) the existence of a parallel way of achieving the same effects, which would be more in the spirit of multiplicative proof-nets (by the way, the translation of multiplicative proof-nets into HC is nondeterministic). A cut-elimination step of HC can be thought of as a move of some play (using the language of game semantics). NEWLINENEWLINENEWLINEIn the second part of the paper, an alternative description of proofs and paraproofs of HC is given. Following the idea that a paraproof of \(A\) should be defined in terms of its interaction (by means of cut-elimination) with all the possible paraproofs of \(\neg A\), the author introduces an abstract notion of (para)proof, called design, and a notion of orthogonality between designs. This leads to behaviors: sets of designs closed w.r.t. the biorthogonal. Paraproofs of HC can be interpreted (in a straightforward way) as designs, and the main theorem of the paper can be stated in a rather traditional way as follows: 1) Every design (resp. winning design) of a behavior is the interpretation of a paraproof (resp. a proof) of HC (full completeness). 2) The interpretation of every paraproof of HC is a design (soundness).NEWLINENEWLINEFor the entire collection see [Zbl 0963.00029].