On the meaning of logical rules. I: Syntax versus semantics

Publication date 28 November 1999

full completeness game semantics hypersequentialization linear logic logical rules meaning monism and duality paraproofs and paralogisms proof-nets syntax and semantics time

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Review text

The paper illustrates the main ideas lying behind what the author calls ``a purely interactive approach to logic. The technical features of this approach are not developped in this work, which appears as a research program. One of the main results of traditional logic is Gödel's completeness theorem: a formula is not provable iff it has a countermodel. This induces a duality, which is also a ``dualism, since proofs and models do not live in the same space. In contrast with this approach, the natural notion of duality coming from the so-called game semantics is the exchange between player and opponent that are ``homogeneous in nature (to quote the author). In that same spirit, the author's idea is to describe a proof by means of ``counterproofs, and this leads to the claim of the paper: ``the meaning of logical rules is hidden in the rules themselves. We mention two of the main novelties of this work: 1) the introduction of paralogisms, ``mistakes of logic allowing to widen the space of proofs (thus obtaining ``paraproofs); 2) the discovery that a proof is nothing but an alternation of rules of different polarities (a rule is either ``positive or ``negative). The first point is a (proof-theoretical) way to overcome the ``dualism proofs/models: the idea is to describe a proof of a formula \(A\) by means of its interaction with the proofs of \(\neg A\), so that the duality occurs now between objects living in the same space (the space of proofs). Of course, the problem is that in traditional syntax, if \(A\) is provable then the set of proofs of \(\neg A\) is empty. Proof-nets (introduced by the author some 15 years ago) give a geometric account of proofs: they are graphs satisfying some geometrical condition (say \(C\)), preserved by the cut-elimination procedure. It is then natural to give the logical status of ``paraproof to every graph satisfying (some variant of) \(C\). One can obtain paraproofs of \(A\) and of \(\neg A\), thus establishing a duality within the (geometrical) space of paraproofs. The second point comes from one of the main achievements of linear logic: the discovery and the careful study of reversion and focalization [see \textit{J.-M. Andreoli} and \textit{R. Pareschi}, New Gener. Comput. 9, 445-473 (1991; Zbl 0731.68022), \textit{J.-Y. Girard}, Math. Struct. Comput. Sci. 1, No. 3, 255-296 (1991; Zbl 0752.03027), \textit{V. Danos, J.-B. Joinet} and \textit{H. Schellinx}, J. Symb. Log. 62, No. 3, 755-807 (1997; Zbl 0895.03023),\dots]. These two properties allow to internalize, within the syntax, the isomorphisms of denotational semantics: in the ``hypersequentialized calculus (which is mentioned, but not introduced in this paper), a logical rule is a cluster of usual rules. This implies, for example, that \((A\wedge B)\wedge C\) and \(A\wedge (B\wedge C)\) are the same formula. In the appendix of the paper, several concepts (many of which introduced in the past 20 years by the author) are revisited in the light of the newly proposed approach. For the entire collection see [Zbl 0911.00047].

Recommendations

Cited in

(19)

This page was built for publication: On the meaning of logical rules. I: Syntax versus semantics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4263837)