There are several areas in logic where the monotonicity of the consequence relation fails to hold. Roughly these are the traditional non-monotonic systems arising in Artificial Intelligence (such as defeasible logics, circumscription, defaults, ete), numerical non-monotonic systems (probabilistic systems, fuzzy logics, belief functions), resource logics (also called substructural logics such as relevance logic, linear logic, Lambek calculus), and the logic of theory change (also called belief revision, see Alchourron, Gärdenfors, Makinson [2224]). We are seeking a common axiomatic and semantical approach (...) to the notion of consequence whieh can be specialised to any of the above areas. This paper introduces the notions of structured consequence relation, shift operators and structural connectives, and shows an intrinsic connection between the above areas. (shrink)

The purpose of this paper is to connect the proof theory and the model theory of a family of propositional logics weaker than Heyting's. This family includes systems analogous to the Lambek calculus of syntactic categories, systems of relevant logic, systems related toBCK algebras, and, finally, Johansson's and Heyting's logic. First, sequent-systems are given for these logics, and cut-elimination results are proved. In these sequent-systems the rules for the logical operations are never changed: all changes are made in the structural (...) rules. Next, Hubert-style formulations are given for these logics, and algebraic completeness results are demonstrated with respect to residuated lattice-ordered groupoids. Finally, model structures related to relevant model structures (of Urquhart, Fine, Routley, Meyer, and Maksimova) are given for our logics. These model structures are based on groupoids parallel to the sequent-systems. This paper lays the ground for a kind of correspondence theory for axioms of logics with implication weaker than Heyting's, a correspondence theory analogous to the correspondence theory for modal axioms of normal modal logics.The first part of the paper, which follows, contains the first two sections, which deal with sequent-systems and Hubert-formulations. The second part, due to appear in the next issue of this journal, will contain the third section, which deals with groupoid models. (shrink)

There are several areas in logic where the monotonicity of the consequence relation fails to hold. Roughly these are the traditional non-monotonic systems arising in Artificial Intelligence, numerical non-monotonic systems, resource logics, and the logic of theory change. We are seeking a common axiomatic and semantical approach to the notion of consequence whieh can be specialised to any of the above areas. This paper introduces the notions of structured consequence relation, shift operators and structural connectives, and shows an intrinsic connection (...) between the above areas. (shrink)

This book sets out the foundations, methodology, and practice of a formal framework for the description of language. The approach embraces the trends of lexicalism and compositional semantics in computational linguistics, and theoretical linguistics more broadly, by developing categorial grammar into a powerful and extendable logic of signs. Taking Montague Grammar as its point of departure, the book explains how integration of methods from philosophy (logical semantics), computer science (type theory), linguistics (categorial grammar) and meta-mathematics (mathematical logic ) provides a (...) categorial foundation with coverage including intensionality, quantification, featural polymorphism, domains and constraints. For the first time, the book systematises categorial thinking into a unified program which is at once both logically secured, and a practical tool for pure lexical grammar development with type-theoretic semantics. It should be of interest to all those active in computational linguistics and formal grammar and is suitable for use at advanced undergraduate, postgraduate, and research levels. (shrink)

Linear logic, introduced by Girard, is a refinement of classical logic with a natural, intrinsic accounting of resources. This accounting is made possible by removing the ‘structural’ rules of contraction and weakening, adding a modal operator and adding finer versions of the propositional connectives. Linear logic has fundamental logical interest and applications to computer science, particularly to Petri nets, concurrency, storage allocation, garbage collection and the control structure of logic programs. In addition, there is a direct correspondence between polynomial-time computation (...) and proof normalization in a bounded form of linear logic. In this paper we show that unlike most other propositional logics, full propositional linear logic is undecidable. Further, we prove that without the modal storage operator, which indicates unboundedness of resources, the decision problem becomes PSPACE-complete. We also establish membership in NP for the multiplicative fragment, NP-completeness for the multiplicative fragment extended with unrestricted weakening, and undecidability for fragments of noncommutative propositional linear logic. (shrink)

This paper contributes to the theory of hybrid substructural logics, i.e. weak logics given by a Gentzen-style proof theory in which there is only alimited possibility to use structural rules. Following the literture, we use an operator to mark formulas to which the extra structural rules may be applied. New in our approach is that we do not see this as a modality, but rather as themeet of the marked formula with a special typeQ. In this way we can make (...) the specific structural behaviour of marked formulas more explicit.The main motivation for our approach is that we can provide a nice, intuitive semantics for hybrid substructural logics. Soundness and completeness for this semantics are proved; besides this we consider some proof-theoretical aspects like cut-elimination and embeddings of the strong system in the hybrid one. (shrink)

We present a semantic study of a family of modal intuitionistic linear systems, providing various logics with both an algebraic semantics and a relational semantics, to obtain completeness results. We call modality a unary operator on formulas which satisfies only one rale (regularity), and we consider any subsetW of a list of axioms which defines the exponential of course of linear logic. We define an algebraic semantics by interpreting the modality as a unary operation on an IL-algebra. Then we introduce (...) a relational semantics based on pretopologies with an additional binary relationr between information states. The interpretation of is defined in a suitable way, which differs from the traditional one in classical modal logic. We prove that such models provide a complete semantics for our minimal modal system, as well as, by requiring the suitable conditions onr (in the spirit of correspondence theory), for any of its extensions axiomatized by any subsetW as above. We also prove an embedding theorem for modal IL-algebras into complete ones and, after introducing the notion of general frame, we apply it to obtain a duality between general frames and modal IL-algebras. (shrink)

This important book provides a new unifying methodology for logic. It replaces the traditional view of logic as manipulating sets of formulas with the notion of structured families of labelled formulas with algebraic structures. This approach has far reaching consequences for the methodology of logics and their semantics, and the book studies the main features of such systems along with their applications. It will interest logicians, computer scientists, philosophers and linguists.

A number of general points behind the story of this paper may be worth setting out separately, now that we have come to the end.There is perhaps one obvious omission to be addressed right away. Although the word “information” has occurred throughout this paper, it must have struck the reader that we have had nothing to say on what information is. In this respect, our theories may be like those in physics: which do not explain what “energy” is (a notion (...) which seems quite similar to “information” in several ways), but only give some basic laws about its behaviour and transmission.The eventual recommendation made here has been to use a broad type-theoretic framework for studying various more classical and more dynamic notions of proposition in their interaction. This is not quite the viewpoint advocated by many current authors in the area, who argue for a whole-sale switch from a ‘static’ to a ‘dynamic’ perspective on propositions. This is not the place, however, to survey the conceptual arguments for and against such a more radical move.This still leaves many questions about possible reductions from one perspective to another. For instance, it would seem that classical systems ought to serve as a ‘limiting case’, which should still be valid after procedural details of some cognitive process have been forgotten. There are various ways of implementing the desired correspondence: e.g. by considering extreme cases with ⫅ equal to identity, or, in the pure relational algebra framework by considering only pairs (x, x). What we shall want then are reductions of dynamic logics, in those special cases, to classical logic. But perhaps also, more sophisticated views are possible. How do we take a piece of ‘dynamic’ prose, remove control instructions and the like, and obtain a piece of ‘classical’ text, suitable for inference ‘in the light of eternity’?There is also a more technical side to the matter of ‘reduction’. By now, Logic has reached such a state of ‘inter-translatability’ that almost all known variant logics can be embedded into each other, via suitable translations. In particular, once an adequate semantic has been given for a new system, this usually induces an embedding into standard logic: as we know, e.g., for the case of Modal Logic. Like-wise, all systems of dynamic interpretation or inference proposed so far admit of direct embedding into an ordinary ‘static’ predicate logic having explicit transition predicates (cf. van Benthem 1988b). Thus, our moral is this. The issue is not whether the new systems of information structure or processing are essentially beyond the expressive resources of traditional logical systems: for, they are not. The issue is rather which interesting phenomena and questions will be put into the right focus by them.The next broad issue concerns the specific use of the perspective proposed here, vis-à-vis concrete proposals for information-oriented or dynamic semantics. The general strategy advocated here is to locate some suitable base calculus and then consider which ‘extras’ are peculiar to the proposal. For instance, this is the spirit in which modal S4 would be a base logic of information models, and intuitionistic logicthe special theory devoting itself to upward persistent propositions. Or, with the examples in Section 4.1, the underlying base logic is our relational algebra, whereas, say, ordinary updates then impose special properties, such as ‘idempotence’: $$xRy \Rightarrow yRy$$ Does this kind of application presuppose the existence of one distinguished base logic, of which all others are extensions? This would be attractive-and some form of relational algebra or linear logic might be a reasonable candidate. Nevertheless, the enterprise does not rest on this outcome. What matters is an increased sensitivity to the ‘landscape’ of dynamic logics, just as with the ‘Categorial Hierarchy’ in Categorial Grammar (cf. van Benthem 1989a, 1991) where the family of logics with their interconnections seems more important than any specific patriarch.Finally, perhaps the most important issue in the new framework is the possibility of new kinds of questions arising precisely because of its differences from standard logic. Notably, given the option of regarding propositions as programs, it will be of interest to consider systematically which major questions about programming languages now make sense inside logic too.EXAMPLE. Correctness. When do we have $$\left[\kern-0.15em\left[ \pi \right]\kern-0.15em\right](\left[\kern-0.15em\left[ A \right]\kern-0.15em\right]) \subseteq \left[\kern-0.15em\left[ B \right]\kern-0.15em\right]$$ for (s, t) propositions A, B and a dynamic (s, (s, t)) proposition π?Program Synthesis. Which dynamic proposition will take us from an information state satisfying A to one satisfying B? (This question needs refinement, lest there be trivial answers.)Determinism. Which propositions as programs are deterministic, in the sense of defining single-valued functions from states to states?Querying. What does it mean to ask for information in the present setting? (Again, individual types referring to e will be crucial here.)This is not merely an agenda for wishful thinking. Within Logic, there are various ways of introducing such concerns into semantics, especially, using tools from Automata Theory. (See van Benthem 1989c for further discussion of such computational perspectives in ‘cognitive programming’.)At least if one believes that ‘dynamics’ is of the essence in cognition (rather than a mere interfacing problem between the halls of eternal truth and the noisy streets of reality), the true test for the present enterprise is the development of a significant new research program not merely copying the questions of old. (shrink)

Models for the Lambek calculus of syntactic categories surveyed here are based on frames that are in principle of the same type as Kripke frames for intuitionistic logic. These models are extracted from the literature on models for relevant logics, in particular the ternary relationed models introduced in the early seventies. The purpose of this brief survey is to locate some open completeness problems for variants of the Lambek calculus in the context of completeness results based on various types of (...) ternary relational models. (shrink)

This paper contributes to the theory of hybrid substructural logics, i.e. weak logics given by a Gentzen-style proof theory in which there is only a limited possibility to use structural rules. Following the literature, we use an operator to mark formulas to which the extra structural rules may be applied. New in our approach is that we do not see this ▽ as a modality, but rather as the meet of the marked formula with a special type Q. In this (...) way we can make the specific structural behaviour of marked formulas more explicit. The main motivation for our approach is that we can provide a nice, intuitive semantics for hybrid substructural logics. Soundness and completeness for this semantics are proved; besides this we consider some proof-theoretical aspects like cut-elimination and embeddings of the 'strong' system in the hybrid one. (shrink)

We present a single sequent calculus common to classical, intuitionistic and linear logics. The main novelty is that classical, intuitionistic and linear logics appear as fragments, i.e. as particular classes of formulas and sequents. For instance, a proof of an intuitionistic formula A may use classical or linear lemmas without any restriction: but after cut-elimination the proof of A is wholly intuitionistic, what is superficially achieved by the subformula property and more deeply by a very careful treatment of structural rules. (...) This approach is radically different from the one that consists in “changing the rule of the game” when we want to change logic, e.g. pass from one style of sequent to another: here, there is only one logic, which—depending on its use—may appear classical, intuitionistic or linear. (shrink)