A complementary system for a given logic is a proof system whose theorems are exactly the formulas that are not valid according to the logic in question. This article is a contribution to the complementary proof theory of classical propositional logic. In particular, we present a complementary proof-net system, $$\textsf{CPN}$$ CPN, that is sound and complete with respect to the set of all classically invalid (one-side) sequents. We also show that cut elimination in $$\textsf{CPN}$$ CPN enjoys strong (...) normalization along with strong confluence (and, hence, uniqueness of normal forms). (shrink)

Proof nets provide abstract counterparts to sequent proofs modulo rule permutations; the idea being that if two proofs have the same underlying proof-net, they are in essence the same proof. Providing a convincing proof-net counterpart to proofs in the classical sequent calculus is thus an important step in understanding classical sequent calculus proofs. By convincing, we mean that there should be a canonical function from sequent proofs to proof nets, it should be possible (...) to check the correctness of a net in polynomial time, every correct net should be obtainable from a sequent calculus proof, and there should be a cut-elimination procedure which preserves correctness.Previous attempts to give proof-net-like objects for propositional classical logic have failed at least one of the above conditions. In Richard McKinley [22], the author presented a calculus of proof nets satisfying and ; the paper defined a sequent calculus corresponding to expansion nets but gave no explicit demonstration of . That sequent calculus, called LK⁎LK⁎ in this paper, is a novel one-sided sequent calculus with both additively and multiplicatively formulated disjunction rules. In this paper [22]), we give a full proof of for expansion nets with respect to LK⁎LK⁎, and in addition give a cut-elimination procedure internal to expansion nets – this makes expansion nets the first notion of proof-net for classical logic satisfying all four criteria. (shrink)

We present a novel way of using proof nets for the multimodal Lambek calculus, which provides a general treatment of both the unary and binary connectives. We also introduce a correctness criterion which is valid for a large class of structural rules and prove basic soundness, completeness and cut elimination results. Finally, we will present a correctness criterion for the original Lambek calculus Las an instance of our general correctness criterion.

This paper shows how proof nets can be used to formalize the notion of incomplete dependency used in psycholinguistic theories of the unacceptability of center embedded constructions. Such theories of human language processing can usually be restated in terms of geometrical constraints on proof nets. The paper ends with a discussion of the relationship between these constraints and incremental semantic interpretation.

We provide an alternative proof of the sequentialisation theorem for proof nets of multiplicative linear logic. Namely, we show how a proof net can be transformed into a sequent calculus proof simply by properly adding to it some special edges, called sequential edges, which express the sequentiality constraints given by sequent calculus.

When we cut a multiplicative proof-net of linear logic in two parts we get two modules with a certain border. We call pretype of a module the set of partitions over its border induced by Danos-Regnier switchings. The type of a module is then defined as the double orthogonal of its pretype. This is an optimal notion describing the behaviour of a module: two modules behave in the same way precisely if they have the same type.In this paper we (...) define a procedure which allows to characterize (and calculate) the type of a module only exploiting its intrinsic geometrical properties and without any explicit mention to the notion of orthogonality. This procedure is simply based on elementary graph rewriting steps, corresponding to the associativity, commutativity and weak-distributivity of the multiplicative connectives of linear logic. (shrink)

This work defines homology groups for proof-structures in multiplicative linear logic (see [Gir1], [Gir2], [Dan]). We will show that these groups characterize proof-nets among arbitrary proof-structures, thus obtaining a new correctness criterion and of course a new polynomial algorithm for testing correctness. This homology also bears information on sequentialization. An unexpected geometrical interpretation of the linear connectives is given in the last section. This paper exclusively focuses onabstract proof-structures, i.e. paired-graphs. The relation with actual proofs (...) is investigated in [Gir1], [Gir2], [Dan], [Ret] and [Tro]. (shrink)

We examine 'weak-distributivity' as a rewriting rule $??$ defined on multiplicative proof-structures (so, in particular, on multiplicative proof-nets: MLL). This rewriting does not preserve the type of proof-nets, but does nevertheless preserve their correctness. The specific contribution of this paper, is to give a direct proof of completeness for $??$: starting from a set of simple generators (proof-nets which are a n-ary ⊗ of &-ized axioms), any mono-conclusion MLL proof-net can be (...) reached by $??$ rewriting (up to ⊗ and & associativity and commutativity). (shrink)

We consider a class of graphs embedded in $R^2$ as noncommutative proof-nets with an explicit exchange rule. We give two characterization of such proof-nets, one representing proof-nets as CW-complexes in a two-dimensional disc, the other extending a characterization by Asperti. As a corollary, we obtain that the test of correctness in the case of planar graphs is linear in the size of the data. Braided proof-nets are proof-nets for multiplicative linear (...) logic with Mix embedded in $R^3$ . In order to prove the cut-elimination theorem, we consider proof-nets in $R^2$ as projections of braided proof-nets under regular isotopy. (shrink)

We define proof nets for cyclic multiplicative linear logic as edge bi-coloured graphs. Our characterization is purely graph theoretical and works without further complication for proof nets with cuts, which are usually harder to handle in the non-commutative case. This also provides a new characterization of the proof nets for the Lambek calculus (with the empty sequence) which simply are a restriction on the formulas to be considered (which are asked to be intuitionistic).

Having defined a notion of homology for paired graphs, Métayer ([Ma]) proves a homological correctness criterion for proof nets, and states that for any proof net \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document} $G$\end{document} there exists a Jordan-Hölder decomposition of \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document} ${\mathsf H}_0(G)$\end{document}. This decomposition is determined by a certain enumeration of the pairs in \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document} $G$\end{document}. (...) We correct his proof of this fact and show that there exists a 1-1 correspondence between these Jordan-Hölder decompositions of \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document} ${\mathsf H}_0(G)$\end{document} and the possible ‘construction-orders’ of the par-net underlying \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document} $G$\end{document}. (shrink)

Having defined a notion of homology for paired graphs, Métayer ([Ma]) proves a homological correctness criterion for proof nets, and states that for any proof net $G$ there exists a Jordan-Hölder decomposition of ${\mathsf H}_0(G)$ . This decomposition is determined by a certain enumeration of the pairs in $G$ . We correct his proof of this fact and show that there exists a 1-1 correspondence between these Jordan-Hölder decompositions of ${\mathsf H}_0(G)$ and the possible ‘construction-orders’ of (...) the par-net underlying $G$. (shrink)

This work is devoted to the relations between Lambek’s Syntactic Calculus and noncommutative variants of Girard’s Linear Logic; in particular the paper will consider: the geometrical representation of the laws of LC by means of proof-nets; the discovery - due to such a geometrical representation - of some laws of LC not yet considered; the discussion of possible linguistic uses of these new laws.

We introduce a new correctness criterion for multiplicative non commutative proof nets which can be considered as the non- commutative counterpart to the Danos-Regnier criterion for proof nets of linear logic. The main intuition relies on the fact that any switching for a proof net can be naturally viewed as a series-parallel order variety on the conclusions of the proof net.

This paper presents a new correctness criterion for marked Danos-Reginer graphs (D-R graphs, for short) of Multiplicative Cyclic Linear Logic MCLL and Abrusci's non-commutative Linear Logic MNLL. As a corollary we obtain an affirmative answer to the open question whether a known quadratic-time algorithm for the correctness checking of proof nets for MCLL and MNLL can be improved to linear-time.

This paper presents a new correctness criterion for marked Danos-Reginer graphs of Multiplicative Cyclic Linear Logic MCLL and Abrusci's non-commutative Linear Logic MNLL. As a corollary we obtain an affirmative answer to the open question whether a known quadratic-time algorithm for the correctness checking of proof nets for MCLL and MNLL can be improved to linear-time.

Different natural deduction proof systems for intuitionistic and classical logic —and related logical systems—differ in fundamental properties while sharing significant family resemblances. These differences become quite stark when it comes to the structural rules of contraction and weakening. In this paper, I show how Gentzen and Jaśkowski’s natural deduction systems differ in fine structure. I also motivate directed proof nets as another natural deduction system which shares some of the design features of Genzen and Jaśkowski’s systems, but (...) which differs again in its treatment of the structural rules, and has a range of virtues absent from traditional natural deduction systems. (shrink)

We describe a categorial system (PPTS) based on partial proof trees(PPTs) as the building blocks of the system. The PPTs are obtained byunfolding the arguments of the type that would be associated with a lexicalitem in a simple categorial grammar. The PPTs are the basic types in thesystem and a derivation proceeds by combining PPTs together. We describe theconstruction of the finite set of basic PPTs and the operations forcombining them. PPTS can be viewed as a categorial system incorporating (...) someof the key insights of lexicalized tree adjoining grammar, namely the notionof an extended domain of locality and the consequent factoring of recursionfrom the domain of dependencies. PPTS therefore inherits the linguistic andcomputational properties of that system, and so can be viewed as a middleground between a categorial grammar and a phrase structure grammar. We alsodiscuss the relationship between PPTS, natural deduction, and linear logicproof-nets, and argue that natural deduction rather than a proof-net systemis more appropriate for the construction of the PPTs. We also discuss howthe use of PPTs allows us to localize the management of resources, therebyfreeing us from this management as the PPTs are combined. (shrink)

We describe a categorial system (PPTS) based on partial proof trees(PPTs) as the building blocks of the system. The PPTs are obtained byunfolding the arguments of the type that would be associated with a lexicalitem in a simple categorial grammar. The PPTs are the basic types in thesystem and a derivation proceeds by combining PPTs together. We describe theconstruction of the finite set of basic PPTs and the operations forcombining them. PPTS can be viewed as a categorial system incorporating (...) someof the key insights of lexicalized tree adjoining grammar, namely the notionof an extended domain of locality and the consequent factoring of recursionfrom the domain of dependencies. PPTS therefore inherits the linguistic andcomputational properties of that system, and so can be viewed as a ’middleground‘ between a categorial grammar and a phrase structure grammar. We alsodiscuss the relationship between PPTS, natural deduction, and linear logicproof-nets, and argue that natural deduction rather than a proof-net systemis more appropriate for the construction of the PPTs. We also discuss howthe use of PPTs allows us to ’localize‘ the management of resources, therebyfreeing us from this management as the PPTs are combined. (shrink)

We show that every MALL proof-structure [9] satisfies the property of softness, originally a categorical notion introduced by Joyal. Furthermore, we show that the notion of hereditary softness precisely captures Girard’s algebraic restriction of the technical condition on proof-structures. Relying on this characterization, we prove a MALL+Mix sequentialization theorem by a proof-theoretical method, using Girard’s notion of jump. Our MALL+Mix correctness criterion subsumes the Danos/Fleury-Retoré criterion [6] for MLL+Mix.

We give the precise correspondence between polarized linear logic and polarized classical logic. The properties of focalization and reversion of linear proofs are at the heart of our analysis: we show that the tq-protocol of normalization for the classical systems and perfectly fits normalization of polarized proof-nets. Some more semantical considerations allow us to recover LC as a refinement of multiplicative.

This paper assumes the success of arguments against the view that informal mathematical proofs secure rational conviction in virtue of their relations with corresponding formal derivations. This assumption entails a need for an alternative account of the logic of informal mathematical proofs. Following examination of case studies by Manders, De Toffoli and Giardino, Leitgeb, Feferman and others, this paper proposes a framework for analysing those informal proofs that appeal to the perception or modification of diagrams or to the inspection or (...) imaginative manipulation of mental models of mathematical phenomena. Proofs relying on diagrams can be rigorous if it is easy to draw a diagram that shares or otherwise indicates the structure of the mathematical object, the information thus displayed is not metrical and it is possible to put the inferences into systematic mathematical relation with other mathematical inferential practices. Proofs that appeal to mental models can be rigorous if the mental models can be externalised as diagrammatic practice that satisfies these three conditions. (shrink)

An alternative proof is given that to each LLM proof net there corresponds at least one LLM sequent proof. The construction is inspired by the sweepline technique from computational geometry and includes a treatment of the multiplicative constants and of proof boxes.

This paper assumes the success of arguments against the view that informal mathematical proofs secure rational conviction in virtue of their relations with corresponding formal derivations. This assumption entails a need for an alternative account of the logic of informal mathematical proofs. Following examination of case studies by Manders, De Toffoli and Giardino, Leitgeb, Feferman and others, this paper proposes a framework for analysing those informal proofs that appeal to the perception or modification of diagrams or to the inspection or (...) imaginative manipulation of mental models of mathematical phenomena. Proofs relying on diagrams can be rigorous if it is easy to draw a diagram that shares or otherwise indicates the structure of the mathematical object, the information thus displayed is not metrical and it is possible to put the inferences into systematic mathematical relation with other mathematical inferential practices. Proofs that appeal to mental models can be rigorous if the mental models can be externalised as diagrammatic practice that satisfies these three conditions. (shrink)

Voor de taalgebruiker spreekt taal vanzelf, maar de taalonderzoeker staat voor raadsels. Woordvormen lijken in niets op hun betekenis. En taalconstructies lijken onlogisch in elkaar te zitten. Toch kunnen we in een enkele zin onze bedoelingen tot in de subtielste nuances duidelijk maken. We hebben geen toegang tot het bewustzijn van de Ander maar kunnen desondanks gedachten met elkaar uitwisselen. We kunnen de werkelijkheid met elkaar bespreken en fictieve werelden met elkaar delen alsof ze toch ergens buiten onszelf bestaan. De (...) taalgebruiker heeft er allemaal geen moeite mee. In De magie van taal brengt Net Koene stap voor stap in kaart wat zich in ons hoofd afspeelt wanneer we naar de Ander luisteren. Ze isoleert taalvormen, woorden, constructies, toonhoogte- en ritmekenmerken die we als informatief herkennen in wat de Ander zegt. Ze laat zien hoe al die vormen systematisch hun eigen bijdrage leveren aan onze voorstelling van waar de Ander het over heeft. De auteur toont deze processen vanuit een denkbeeldig alwetend perspectief, in dit boek Omega genoemd. Binnen dit theoretische kader legt ze per hypothese verband tussen wat in het bewustzijn opkomt en de machinerie van het brein: hoe vormt de wereld van onze zintuigen zich, hoe komt ons voorstellingsvermogen tot stand, hoe transformeert de zintuiglijke wereld in een bespreekbare wereld? En vooral: hoe werkt het dat we de inhoud van ons bewustzijn op dat van de Ander kunnen afstemmen? (shrink)

Jeff Bernard was a distinguished semiotician, always au courant with the main accomplishments in the field. Although Jeff himself had specialized in socio-semiotics, his architectural training and his artistic youth had lent him a really open mind, able to comprehend almost everything.Jeff Bernard was also an excellent administrator. He and Gloria organized countless international conferences, most of them based in Vienna (at the Institute for Socio-Semiotic Studies Jeff was the director of ), but also in other places in Austria, Germany, (...) Italy. All of them were a success. Jeff ran the ISSS almost single-handed. He edited books (he published three of mine, among many, many others), anthologies, semiotic journals. He knew how to raise funding, of which the whole semiotic community benefitted. In 2003, he acted as my “impresario”, as he jokingly said, and organized a lecturing tour through Central Europe for me.Jeff was also a wonderful host; he considered his guests as part of the family and treated them accordingly. Many were the times when he picked me up from one Viennese railway station or the other, or when he drove me there, when I stopped in Vienna, to or from other places. It was owing to Jeff and Gloria that I discovered Grinzig, Baden, and various other cozy places in and around Vienna. Last but not least, it was also due to Jeff and Gloria that I discovered the charm of many Viennese restaurants.Jeff was kind and generous, elegant and discreet. He helped quite a lot of semioticians to forward their careers, and more important still, he did it unobtrusively. Jeff was also a likeable person, with an entertaining conversation and a fine sense of humor.“I am a Feminist”, Jeff once said. (For the sake of historical accuracy, it was in September 1997, round a dinner table at the Early-Fall School of Semiotics, thenheld in Bankya, Bulgaria). And he further expanded: “Otherwise, we couldn’t be living with Gloria. And my life would be pretty difficult, virtually surrounded as I am by so many professional women. But they all think I am a Feminist, and they are happy to work for my benefit. So I sit at my desk in Vienna, and my women colleagues from all over the world send me contributions for this and that, come over to participate in conferences, etc. It pays being a Feminist”.“Ich bin ein Berliner”, said Jeff on another occasion. For historical accuracy, it was in September 2003, during the conference celebrating his 60th birthday, in answer to a remark made by Roland Posner. It seemed a humorous statement, and everybody smiled. But I think this was true in spirit. These few lines, as well as (I suppose) those written by other colleagues who have contributed to the present issue, are meant to illustrate this self-definition. Jeff had always sympathized with the less privileged people everywhere. (shrink)