Society is becoming increasingly reliant upon the dependability of computerbased systems. Achieving and demonstrating the dependability of systems requires the construction and review of valid and coherent arguments. This paper discusses the need for a variety of classes of arguments in dependable systems and reviews existing approaches to the representation of arguments in each of these classes. The issues surrounding the certification of safety critical systems demonstrate the current need for richer representations of dependability arguments which support tools for their (...) construction and review. The paper discusses how a meta-logical framework, informed by aspects of both formal and informal logic, offers a rich and unified means of representing dependability arguments and of thus addressing this need. (shrink)

We prove a full completeness theorem for multiplicative–additive linear logic using a double gluing construction applied to Ehrhard’s *-autonomous category of hypercoherences. This is the first non-game-theoretic full completeness theorem for this fragment. Our main result is that every dinatural transformation between definable functors arises from the denotation of a cut-free proof. Our proof consists of three steps. We show:• Dinatural transformations on this category satisfy Joyal’s softness property for products and coproducts.• Softness, together with multiplicative full completeness, guarantees that (...) every dinatural transformation corresponds to a Girard proof-structure.• The proof-structure associated with any dinatural transformation is a proof-net, hence a denotation of a proof. This last step involves a detailed study of cycles in additive proof-structures.The second step is a completely general result, while the third step relies on the concrete structure of a double gluing construction over hypercoherences. (shrink)

This paper investigates whether the fundamental linguistic insights and intuitions of Lexical Functional Grammar, which is usually presented as a constraint-based linguistic theory, can be reformulated in a resource sensitive framework using a substructural modal logic. In the approach investigated here, LFG's f-descriptions are replaced with expressions from a multi-modal propositional logic. In effect, the feature structure unification basis of LFG's f-structures is replaced with a very different resource based mechanism. It turns out that some linguistic analyses that required non-monotonic (...) devices in LFG analysis of Icelandic) can be straightforwardly expressed in the framework presented here. Moreover, a Curry– Howard correspondence between proofs in this logic and -terms provides a semantic interpretation as a by-product of the process of showing syntactic well-formedness. (shrink)

In other works, I’ve proposed a solution to the semantic paradoxes which, at the technical level, basically relies on failure of contraction. I’ve also suggested that, at the philosophical level, contraction fails because of the instability of certain states of affairs. In this paper, I try to make good on that suggestion.

We introduce a number of logics to reason about collective propositional attitudes that are defined by means of the majority rule. It is well known that majoritarian aggregation is subject to irrationality, as the results in social choice theory and judgment aggregation show. The proposed logics for modelling collective attitudes are based on a substructural propositional logic that allows for circumventing inconsistent outcomes. Individual and collective propositional attitudes, such as beliefs, desires, obligations, are then modelled by means of minimal modalities (...) to ensure a number of basic principles. In this way, a viable consistent modelling of collective attitudes is obtained. (shrink)

This article presents three extracts from the introductory course in mathematical logic that Gödel gave at the University of Notre Dame in 1939. The lectures include a few digressions, which give insight into Gödel's views on logic prior to his philosophical papers of the 1940s. The first extract is Gödel's first lecture. It gives the flavour of Gödel's leisurely style in this course. It also includes a curious definition of logic and a discussion of implication in logic and natural language. (...) The second extract is a discussion on undecidability and on Leibniz. The third extract concerns the paradoxes and Russell's theory of types. (shrink)

ABSTRACT My aim in this paper is to present a pluralist thesis about the inferential role of logical constants, which embraces classical, relevant, linear and ordered logic. That is, I defend that a logical constant c has more than one correct inferential role. The thesis depends on a particular interpretation of substructural logics' vocabulary, according to which classical logic captures the literal meaning of logical constants and substructural logics encode a pragmatically enriched sense of those connectives. The paper is divided (...) into four parts: first, I introduce the motivation for the pluralist thesis of the paper; second I introduce the calculus for the different logics endorsed in the pluralist thesis; third, I motivate how the different behaviors of the logical vocabulary of these logics can be pragmatically interpreted, and fourth, I motivate how the different inferential roles that each substructural logic attribute to logical constants can coexist, and how we should reason with a logical constant c given this plurality. (shrink)

RASP is a recent extension to Answer Set Programming (ASP) that permits declarative specification and reasoning on the consumption and production of resources. ASP can be seen as a particular case of RASP. In this paper, we study the relationship between linear logic and RASP problem specification. We prove that RASP programs can be translated into (a fragment of) linear logic, and vice versa. In doing so, we introduce a linear logic representation of default negation as understood in ASP. We (...) are also able to establish a link between linear logic and here-and-there (HT) logic. (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.

Dialogical logic is a game-theoretical approach to logic. Logic is studied with the help of certain games, which can be thought of as idealized argumentations. Two players, the Proponent, who puts forward the initial thesis and tries to defend it, and the Opponent, who tries to attack the Proponent’s thesis, alternately utter argumentative moves according to certain rules. For a long time the dialogical approach had been worked out only for classical and intuitionistic logic. The seven papers of this dissertation (...) show that this narrowness was uncalled for. The initial paper presents an overview and serves as an introduction to the other papers. Those papers are related by one central theme. As each of them presents dialogical formulations of a different non-classical logic, they show that dialogical logic constitutes a powerful and flexible general framework for the development and study of various logical formalisms and combinations thereof. As such it is especially attractive to logical pluralists that reject the idea of “the single correct logic”. The collection contains treatments of free logic, modal logic, relevance logic, connexive logic, linear logic, and multi-valued logic. (shrink)

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 prove that the full completeness theorem for MLL+Mix holds by the simple interpretation via formulas as objects and proofs as Z-invariant morphisms in the *-autonomous category of topologized vector spaces. We do this by generalizing the recent work of Blute and Scott 101–142) where they used the semantical framework of dinatural transformation introduced by Girard–Scedrov–Scott , Logic from Computer Science, vol. 21, Springer, Berlin, 1992, pp. 217–241). By omitting the use of dinatural transformation, our semantics evidently allows the interpretation (...) of the cut-rule, while the original Blute–Scott's does not. Moreover, our interpretation for proofs is preserved automatically under the cut elimination procedure. In our semantics proofs themselves are characterized by the concrete algebraic notion “Z-invariance”, and our denotational semantics provides the full completeness. Our semantics is naturally extended to the full completeness semantics for CyLL+Mix owing to an elegant method of Blute–Scott 1413–1436) 101–142))). (shrink)

The aim of this paper is to argue that logic can play an important role in the “toolbox” of molecular biology. We show how biochemical pathways, i.e., transitions from a molecular aggregate to another molecular aggregate, can be viewed as deductive processes. In particular, our logical approach to molecular biology — developed in the form of a natural deduction system — is centered on the notion of Curry-Howard isomorphism, a cornerstone in nineteenth-century proof-theory.

We describe how Intuitionistic Linear Logic can be used to provide a unified logical account for agents to find and execute plans. This account supports the modelling of agent interaction, including dialogue; allows agents to be robust to unexpected events and failures; and supports significant reuse of agent specifications. The framework has been implemented and several case studies have been considered. Further applications include human–computer interfaces as well as agent interaction in the semantic web.

The category of coherent phase spaces introduced by the author is a refinement of the symplectic “category” of A. Weinstein. This category is *-autonomous and thus provides a denotational model for Multiplicative Linear Logic. Coherent phase spaces are symplectic manifolds equipped with a certain extra structure of “coherence”. They may be thought of as “infinitesimal” analogues of familiar coherent spaces of Linear Logic. The role of cliques is played by Lagrangian submanifolds of ambient spaces. Physically, a symplectic manifold is the (...) phase space of a classical dynamical system, and a Lagrangian submanifold is a phase of a short-wave oscillation. Typically, Lagrangian submanifolds represent such objects as short-wave approximations of wave functions in asymptotic quantization and wave fronts in geometrical optics. The coherent phase space semantics was motivated to a large extent by methods of geometric and asymptotic quantization and suggests some interesting intuitions on Linear Logic. In particular Lagrangian submanifold-cliques of types A and A can be interpreted as semiclassical limits of eigenstates of respectively position and momentum observables. These observables being canonically conjugate cannot be measured simultaneously, which corresponds to the idea that a formula A and its negation A cannot both simultaneously have proofs . We show that the coherent phase space semantics of Linear Logic enjoys several completeness properties in general much stronger than the usual full completeness with respect to the class of dinatural transformations. These properties of completeness in conjunction with a quite natural -physical meaning make the coherent phase space semantics an interesting object of investigation. (shrink)

We extend to the exponential connectives of linear logic the study initiated in Bucciarelli and Ehrhard 247). We define an indexed version of propositional linear logic and provide a sequent calculus for this system. To a formula A of indexed linear logic, we associate an underlying formula of linear logic, and a family A of elements of , the interpretation of in the category of sets and relations. Then A is provable in indexed linear logic iff the family A is (...) contained in the interpretation of some proof of . We extend to this setting the product phase semantics of indexed multiplicative additive linear logic introduced in Bucciarelli and Ehrhard , defining the symmetric product phase spaces. We prove a soundness result for this truth-value semantics and show how a denotational model of linear logic can be associated to any symmetric product phase space. Considering a particular symmetric product phase space, we obtain a new coherence space model of linear logic, which is non-uniform in the sense that the interpretation of a proof of !A−B contains informations about the behavior of this proof when applied to “chimeric” arguments of type A . In this coherence semantics, an element of a web can be strictly coherent with itself, or two distinct elements can be “neutral”. (shrink)

In this paper, we present a categorical model for Multiplicative Additive Polarized Linear Logic , which is the linear fragment of Olivier Laurent’s Polarized Linear Logic. Our model is based on an adjunction between reflective/coreflective full subcategories / of an ambient *-autonomous category . Similar structures were first introduced by M. Barr in the late 1970’s in abstract duality theory and more recently in work on game semantics for linear logic. The paper has two goals: to discuss concrete models and (...) to present various completeness theorems.As concrete examples, we present a hypercoherence model, using Ehrhard’s hereditary/anti-hereditary objects, a Chu-space model, a double gluing model over our categorical framework, and a model based on iterated double gluing over a *-autonomous category.For the multiplicative fragment of. (shrink)

Permutative logic is a non-commutative conservative extension of linear logic suggested by some investigations on the topology of linear proofs. In order to syntactically reflect the fundamental topological structure of orientable surfaces with boundary, permutative sequents turn out to be shaped like q-permutations. Relaxation is the relation induced on q-permutations by the two structural rules divide and merge; a decision procedure for relaxation has been already provided by stressing some standard achievements in theory of permutations. In these pages, we provide (...) a parallel procedure in which the problem at issue is approached from the point of view afforded by geometry of 2-manifolds and solved by making specific surfaces interact. (shrink)

Just as intuitionistic proofs can be modeled by functions, linear logic proofs, being symmetric in the inputs and outputs, can be modeled by relations . However generic relations do not establish any functional dependence between the arguments, and therefore it is questionable whether they can be thought as reasonable generalizations of functions. On the other hand, in some situations one can speak in some precise sense about an implicit functional dependence defined by a relation. It turns out that it is (...) possible to model linear logic with implicit functions rather than general relations, an adequate language for such a semantics being differential calculus. This results in a non-degenerate model enjoying quite strong completeness properties. (shrink)

A new characterization of all the MV-algebras embedded in a CL-algebra has been presented. A new sequent calculus for Lukasiewicz ℵ0-valued logic is introduced. Some links between this calculus and the sequent calculus for multiplicative additive linear logic are established. It has been shown that Lukasiewicz ℵ0-valued logic can be embedded in a suitable extension of MALL.

The goal of the paper is to discuss whether substructural non-contractive accounts of the truth-theoretic paradoxes can be philosophically motivated. First, I consider a number of explanations that have been offered to justify the failure of contraction and I argue that they are not entirely compelling. I then present a non-contractive theory of truth that I’ve proposed elsewhere. After looking at some of its formal properties, I suggest an explanation of the failure of structural contraction that is compatible with it.

This paper is a sequel to my [7]. It focuses on the notion of natural number as introduced in section 11 of that paper with regard to forms of induction and recursive definitions. One point is that this notion of natural number is somewhat weaker than the classical one in so far as it is defined in terms of a weak implication. The other point is the lack of even a weak form of extensionality. As a main result of the (...) present paper it will turn out that the means provided in [7] are sufficient to account for an interpretation of primitive recursive arithmetic. (shrink)

We present a reading of the traditional syllogistics in a fragment of the propositional intuitionistic multiplicative linear logic and prove that with respect to a diagrammatic logical calculus that we introduced in a previous paper, a syllogism is provable in such a fragment if and only if it is diagrammatically provable. We extend this result to syllogistics with complemented terms à la De Morgan, with respect to a suitable extension of the diagrammatic reasoning system for the traditional case and a (...) corresponding reading of such De Morgan style syllogistics in the previously referred to fragment of linear logic. (shrink)

This collection of papers, celebrating the contributions of Swedish logician Dag Prawitz to Proof Theory, has been assembled from those presented at the Natural Deduction conference organized in Rio de Janeiro to honour his seminal research. Dag Prawitz’s work forms the basis of intuitionistic type theory and his inversion principle constitutes the foundation of most modern accounts of proof-theoretic semantics in Logic, Linguistics and Theoretical Computer Science. The range of contributions includes material on the extension of natural deduction with higher-order (...) rules, as opposed to higher-order connectives, and a paper discussing the application of natural deduction rules to dealing with equality in predicate calculus. The volume continues with a key chapter summarizing work on the extension of the Curry-Howard isomorphism, via methods of category theory that have been successfully applied to linear logic, as well as many other contributions from highly regarded authorities. With an illustrious group of contributors addressing a wealth of topics and applications, this volume is a valuable addition to the libraries of academics in the multiple disciplines whose development has been given added scope by the methodologies supplied by natural deduction. The volume is representative of the rich and varied directions that Prawitz work has inspired in the area of natural deduction. (shrink)

In this paper we consider the relations existing between four deductive systems that have been called categorial grammars and have relevant connections with linguistic investigations: the syntactic calculus, bilinear logic, compact bilinear logic and Curry''s semantic calculus.