This book offers a concise introduction to both proof-theory and algebraic methods, the core of the syntactic and semantic study of logic respectively. The importance of combining these two has been increasingly recognized in recent years. It highlights the contrasts between the deep, concrete results using the former and the general, abstract ones using the latter. Covering modal logics, many-valued logics, superintuitionistic and substructural logics, together with their algebraic semantics, the book also provides an introduction to nonclassical logic for undergraduate (...) or graduate level courses.The book is divided into two parts: Proof Theory in Part I and Algebra in Logic in Part II. Part I presents sequent systems and discusses cut elimination and its applications in detail. It also provides simplified proof of cut elimination, making the topic more accessible. The last chapter of Part I is devoted to clarification of the classes of logics that are discussed in the second part. Part II focuses on algebraic semantics for these logics. At the same time, it is a gentle introduction to the basics of algebraic logic and universal algebra with many examples of their applications in logic. Part II can be read independently of Part I, with only minimum knowledge required, and as such is suitable as a textbook for short introductory courses on algebra in logic. (shrink)

It is proved that all bimodal tense logics which contain the logic of the weak orderings and have unbounded depth do not have the interpolation property.

The Craig Interpolation Theorem is intimately connected with the emergence of abstract logic and continues to be the driving force of the field. I will argue in this paper that the interpolation property is an important litmus test in abstract model theory for identifying “natural,” robust extensions of first order logic. My argument is supported by the observation that logics which satisfy the interpolation property usually also satisfy a Lindström type maximality theorem. Admittedly, the range of such logics is small.

The ‘No Ought From Is’ principle (or ‘NOFI’) states that a valid argument cannot have both an ethical conclusion and non-ethical premises. Arthur Prior proposed several well-known counterexamples, including the following: Tea-drinking is common in England; therefore, either tea-drinking is common in England or all New Zealanders ought to be shot. My aim in this paper is to defend NOFI against Prior’s counterexamples. I propose two novel interpretations of NOFI and prove that both are true.

Arrow and turnstile interpolations are investigated in UCL [introduced by Sernadas et al. ], a logic that is a complete extension of classical propositional logic for reasoning about connectives that only behave as expected with a given probability. Arrow interpolation is shown to hold in general and turnstile interpolation is established under some provisos.

The Quantified argument calculus (Quarc) has received a lot of attention recently as an interesting system of quantified logic which eschews the use of variables and unrestricted quantification, but nonetheless achieves results similar to the Predicate calculus (PC) by employing quantifiers applied directly to predicates instead. Despite this noted similarity, the issue of the relationship between Quarc and PC has so far not been definitively resolved. We address this question in the present paper, and then expand upon that result. Utilizing (...) recent developments in structural proof theory, we develop a G3-style sequent calculus for Quarc and briefly demonstrate its structural properties. We put these properties to use immediately to construct direct proofs of the meta-theoretical properties of the system. We then incorporate an abstract (and, as we shall see, logical) predicate into the system in a way that preserves all the structural properties. This allows us to identify a system of Quarc which is deductively equivalent to PC, and also yields a constructive method of demonstrating the Craig interpolation theorem (which speaks in favor of the aforementioned predicate being logical). We further generalize this extension to develop a bivalent system of Quarc with defining clauses that still maintains all the desirable properties of a good proof system. (shrink)

Both the Beth definability theorem and Craig's lemma (interpolation theorem from now on) deal with the issue of the entanglement of one language L1 with another language L2, that is to say, information transfer—or the lack of such transfer—between the two languages. The notion of splitting we study below looks into this issue. We briefly relate our own results in this area as well as the results of other researchers like Kourousias and Makinson, and Peppas, Chopra and Foo.Section 3 does (...) contain one apparently new theorem. (shrink)

Lyndon's Interpolation Theorem asserts that for any valid implication between two purely relational sentences of first-order logic, there is an interpolant in which each relation symbol appears positively (negatively) only if it appears positively (negatively) in both the antecedent and the succedent of the given implication. We prove a similar, more general interpolation result with the additional requirement that, for some fixed tuple U of unary predicates U, all formulae under consideration have all quantifiers explicitly relativised to one of the (...) U. Under this stipulation, existential (universal) quantification over U contributes a positive (negative) occurrence of U. It is shown how this single new interpolation theorem, obtained by a canonical and rather elementary model theoretic proof, unifies a number of related results: the classical characterisation theorems concerning extensions (substructures) with those concerning monotonicity, as well as a many-sorted interpolation theorem focusing on positive vs. negative occurrences of predicates and on existentially vs. universally quantified sorts. (shrink)

All extensions of the modal Grzegorczyk logic Grz possessing projective Beth's property PB2 are described. It is proved that there are exactly 13 logics over Grz with PB2. All of them are finitely axiomatizable and have the finite model property. It is shown that PB2 is strongly decidable over Grz, i.e. there is an algorithm which, for any finite system Rul of additional axiom schemes and rules of inference, decides if the calculus Grz+Rul has the projective Beth property.

A restricted interpolation property IPR is investigated in modal and superintuitionistic logics. The problem of description of logics with IPR over the intuitionistic logic Int and the modal Grzegorczyk logic Grz is solved. It is proved that in extensions of Int or Grz IPR is equivalent to the projective Beth property PB2. It follows that IPR is decidable over Int and strongly decidable over Grz.

In a previous paper [ 21 ] all extensions of Johansson’s minimal logic J with the weak interpolation property WIP were described. It was proved that WIP is decidable over J. It turned out that the weak interpolation problem in extensions of J is reducible to the same problem over a logic Gl, which arises from J by adding tertium non datur. In this paper we consider extensions of the logic Gl. We prove that only finitely many logics over Gl (...) have the Craig interpolation property CIP, the restricted interpolation property IPR or the projective Beth property PBP. The full list of Gl-logics with the mentioned properties is found, and their description is given. We note that IPR and PBP are equivalent over Gl. It is proved that CIP, IPR and PBP are decidable over the logic Gl. (shrink)

It is proved that there are exactly 16 superintuitionistic propositional logics with the projective Beth property. These logics are finitely axiomatizable and have the finite model property. Simultaneously, all varieties of Heyting algebras with strong epimorphisms surjectivity are found.

A family of prepositional logics is considered to be intermediate between the intuitionistic and classical ones. The generalized interpolation property is defined and proved is the following.Theorem on interpolation. For every intermediate logic L the following statements are equivalent:(i) Craig's interpolation theorem holds in L, (ii) L possesses the generalized interpolation property, (iii) Robinson's consistency statement is true in L.

Three variants of Beth's definability theorem are considered. Let L be any normal extension of the provability logic G. It is proved that the first variant B1 holds in L iff L possesses Craig's interpolation property. If L is consistent, then the statement B2 holds in L iff L = G + {0}. Finally, the variant B3 holds in any normal extension of G.

Algebraic approach to study of classical and non-classical logical calculi was developed and systematically presented by Helena Rasiowa in [48], [47]. It is very fruitful in investigation of non-classical logics because it makes possible to study large families of logics in an uniform way. In such research one can replace logics with suitable classes of algebras and apply powerful machinery of universal algebra. In this paper we present an overview of results on interpolation and definability in modal and positive logics,and (...) also in extensions of Johansson's minimal logic. All these logics are strongly complete under algebraic semantics. It allows to combine syntactic methods with studying varieties of algebras and to flnd algebraic equivalents for interpolation and related properties. Moreover, we give exhaustive solution to interpolation and some related problems for many families of propositional logics and calculi. (shrink)

We investigate transfer of interpolation in such combinations of modal logic which lead to interaction of the modalities. Combining logics by taking products often blocks transfer of interpolation. The same holds for combinations by taking unions, a generalization of Humberstone's inaccessibility logic. Viewing first-order logic as a product of modal logics, we derive a strong counterexample for failure of interpolation in the finite variable fragments of first-order logic. We provide a simple condition stated only in terms of frames and bisimulations (...) which implies failure of interpolation. Its use is exemplified in a wide range of cases. (shrink)

We introduce and investigate the notion of uniform Lyndon interpolation property which is a strengthening of both uniform interpolation property and Lyndon interpolation property. We prove several propositional modal logics including \, \, \ and \ enjoy ULIP. Our proofs are modifications of Visser’s proofs of uniform interpolation property using layered bisimulations Gödel’96, logical foundations of mathematics, computer science and physics—Kurt Gödel’s legacy, Springer, Berlin, 1996). Also we give a new upper bound on the complexity of uniform interpolants for \ (...) and \. (shrink)

The splitting theorem says that any set of formulae has a finest representation as a family of letter-disjoint sets. Parikh formulated this for classical propositional logic, proved it in the finite case, used it to formulate a criterion for relevance in belief change, and showed that AGMpartial meet revision can fail the criterion. In this paper we make three further contributions. We begin by establishing a new version of the well-known interpolation theorem, which we call parallel interpolation, use it to (...) prove the splitting theorem in the infinite case, and show how AGM belief change operations may be modified, if desired, so as to ensure satisfaction of Parikh’s relevance criterion. (shrink)

. We explore a connection between different ways of representing information in computer science. We show that relational databases, modules, algebraic specifications and constraint systems all satisfy the same ten axioms. A commutative semigroup together with a lattice satisfying these axioms is then called an “information algebra”. We show that any compact consequence operator satisfying the interpolation and the deduction property induces an information algebra. Conversely, each finitary information algebra can be obtained from a consequence operator in this way. Finally (...) we show that arbitrary (not necessarily finitary) information algebras can be represented as some kind of abstract relational database called a tuple system. (shrink)

In prior work [7] we considered networks of agents who have knowledge bases in first order logic, and report facts to their neighbors that are in their common languages and are provable from their knowledge bases, in order to help a decider verify a single sentence. In report complete networks, the signatures of the agents and the links between agents are rich enough to verify any deciderʼs sentence that can be proved from the combined knowledge base. This paper introduces a (...) more general setting where new observations may be added to knowledge bases and the decider must choose a sentence from a set of alternatives. We consider the question of when it is possible to prepare in advance a finite plan to generate reports within the network. We obtain conditions under which such a plan exists and is guaranteed to produce the right choice under any new observations. (shrink)

The Craig interpolation theorem is shown for an extended LJ with strong negation. A new simple proof of this theorem is obtained. © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim.

First-order intuitionistic and classical Nelson–Wansing and Arieli–Avron–Zamansky logics, which are regarded as paradefinite and connexive logics, are investigated based on Gentzen-style sequent calculi. The cut-elimination and completeness theorems for these logics are proved uniformly via theorems for embedding these logics into first-order intuitionistic and classical logics. The modified Craig interpolation theorems for these logics are also proved via the same embedding theorems. Furthermore, a theorem for embedding first-order classical Arieli–Avron–Zamansky logic into first-order intuitionistic Arieli–Avron–Zamansky logic is proved using a modified (...) Gödel–Gentzen negative translation. The failure of a theorem for embedding first-order classical Nelson–Wansing logic into first-order intuitionistic Nelson–Wansing logic is also shown. (shrink)

Two new multilattice logics called submultilattice logic and indexed multilattice logic are introduced as a monosequent calculus and an indexed monosequent calculus, respectively. The submultilattice logic is regarded as a monosequent calculus version of Shramko’s original multilattice logic, which is also known as the logic of logical multilattices. The indexed multilattice logic is an extension of the submultilattice logic, and is regarded as the logic of multilattices. A completeness theorem with respect to a lattice-valued semantics is proved for the submultilattice (...) logic, and a completeness theorem with respect to a multilattice-valued semantics is proved for the indexed multilattice logic. (shrink)

SummaryCarnap tried to overcome metaphysics through a distinction between empirical and conceptual truths. The distinction has since been challenged, but not on the basis of a systematic logical analysis of language. It is suggested here that the logical theory of identifiability based on the author's interrogative model will provide the tools for such a systematic analysis. As an example of what the model can do, a criticism is offered of Quine's and Chomsky's implicit assumption that language learning is based on (...) atomistic “answers” .RésuméCarnap a essayé de dépasser la métaphysique par une distinction entre des vérités empiriques et des vérités conceptuelles. Cette distinction a ensuite été contestée, mais non sur la base ?une analyse systematique du langage. On suggére ici que la théorie logique de ľidentifiabilité basée sur le modéle interrogatif de ľauteur fournira les outils ?une telle analyse systématique. Comme exemple de ce que peut faire ce modéle, on présente une critique de la supposition implicite de Quine et de Chomsky selon laquelle ľapprentissage du langage repose sur des ≫réponses≪ atomiques .ZusammenfassungCarnap versuchte Metaphysik durch eine Unterscheidung zwischen empirischen und konzep‐tuellen Wahrheiten zu iiberwinden. Seither wurde die Unterscheidung immer wieder angegriffen, jedoch nicht auf der Basis einer systematischen logischen Analyse der Sprache. In vorliegendem Artikel wird vorgeschlagen, dass eine logische Theorie der Identifizierbarkeit, welche auf dem Frage‐Antwort‐Modell des Autors grilndet, die Instrumente fur eine solche logische Analyse bereitstellt. Als Beispiel dafiir, was das Modell leisten kann, dient eine Kritik an Quines und Chomskys impliziter Voraussetzung, dass das Erlernen von Sprache auf atomaren ≫Antworten≪ aufbaut. (shrink)

A (normalized) interpolant I in Craig's theorem is a kind of explanation why the consequence relation (from F to G) holds. This is because I is a summary of the interaction of the configurations specified by F and G, respectively, that shows how G follows from F. If explaining E means deriving it from a background theory T plus situational information A and if among the concepts of E we can separate those occurring only in T or only in A, (...) then the interpolation theorem applies in two different ways yielding two different explanations and two different covering laws. (shrink)

We prove a generalization of Maehara’s lemma to show that the extensions of classical and intuitionistic first-order logic with a special type of geometric axioms, called singular geometric axioms, have Craig’s interpolation property. As a corollary, we obtain a direct proof of interpolation for (classical and intuitionistic) first-order logic with identity, as well as interpolation for several mathematical theories, including the theory of equivalence relations, (strict) partial and linear orders, and various intuitionistic order theories such as apartness and positive partial (...) and linear orders. (shrink)

The problem of interpolation is a classical problem in logic. Given a consequence relation |~ and two formulas φ and ψ with φ |~ ψ we try to find a “simple" formula α such that φ |~ α |~ ψ. “Simple" is defined here as “expressed in the common language of φ and ψ". Non-monotonic logics like preferential logics are often a mixture of a non-monotonic part with classical logic. In such cases, it is natural examine also variants of the (...) interpolation problem, like: is there “simple" α such that φ ⊢ α |~ ψ where ⊢ is classical consequence? We translate the interpolation problem from the syntactic level to the semantic level. For example, the classical interpolation problem is now the question whether there is some “simple" model set X such that M(φ) ⫅ X ⫅ M(ψ). We can show that such X always exist for monotonic and antitonic logics. The case of non-monotonic logics is more complicated, there are several variants to consider, and we mostly have only partial results. (shrink)

Though deceptively simple and plausible on the face of it, Craig's interpolation theorem (published 50 years ago) has proved to be a central logical property that has been used to reveal a deep harmony between the syntax and semantics of first order logic. Craig's theorem was generalized soon after by Lyndon, with application to the characterization of first order properties preserved under homomorphism. After retracing the early history, this article is mainly devoted to a survey of subsequent generalizations and applications, (...) especially of many-sorted interpolation theorems. Attention is also paid to methodological considerations, since the Craig theorem and its generalizations were initially obtained by proof-theoretic arguments while most of the applications are model-theoretic in nature. The article concludes with the role of the interpolation property in the quest for "reasonable" logics extending first-order logic within the framework of abstract model theory. (shrink)

Though deceptively simple and plausible on the face of it, Craig's interpolation theorem has proved to be a central logical property that has been used to reveal a deep harmony between the syntax and semantics of first order logic. Craig's theorem was generalized soon after by Lyndon, with application to the characterization of first order properties preserved under homomorphism. After retracing the early history, this article is mainly devoted to a survey of subsequent generalizations and applications, especially of many-sorted interpolation (...) theorems. Attention is also paid to methodological considerations, since the Craig theorem and its generalizations were initially obtained by proof-theoretic arguments while most of the applications are model-theoretic in nature. The article concludes with the role of the interpolation property in the quest for "reasonable" logics extending first-order logic within the framework of abstract model theory. (shrink)

In this essay we analyse and elucidate the method to establish and clarify the scope of logic theorems offered within the theory of institutions. The method presented pervades a lot of abstract model theoretic developments carried out within institution theory. The power of the proposed general method is illustrated with the examples of interpolation and definability, as they appear in the literature of institutional model theory. Both case studies illustrate a considerable extension of the original scopes of the two classical (...) theorems. Our presentation is rather narrative with the relevant logic and institution theory concepts introduced and explained gradually to the non-expert reader. (shrink)

Work on how to axiomatize the subtheories of a first-order theory in which only a proper subset of their extra-logical vocabulary is being used led to a theorem on recursive axiomatizability and to an interpolation theorem for first-order logic. There were some fortuitous events and several logicians played a helpful role.

In this paper we give a new proof of Richardson's theorem [31]: a global function G[MATHEMATICAL DOUBLE-STRUCK CAPITAL A] of a cellular automaton [MATHEMATICAL DOUBLE-STRUCK CAPITAL A] is injective if and only if the inverse of G[MATHEMATICAL DOUBLE-STRUCK CAPITAL A] is a global function of a cellular automaton. Moreover, we show a way how to construct the inverse cellular automaton using the method of feasible interpolation from [20]. We also solve two problems regarding complexity of cellular automata formulated by Durand (...) [12]. (shrink)

Lambek elegantly characterized part of natural language. As is well-known, his substructural logic L, and its non-associative version NL, handle basic function/argument composition well, but not scope taking and syntactic displacement—at least, not in their full generality. In previous work, I propose $$\text {NL}_\lambda $$, which is NL supplemented with a single structural inference rule (“abstraction”). Abstraction closely resembles the traditional linguistic rule of quantifier raising, and characterizes both semantic scope taking and syntactic displacement. Due to the unconventional form of (...) the abstraction inference, there has been some doubt that $$\text {NL}_\lambda $$ should count at a legitimate substructural logic. This paper argues that $$\text {NL}_\lambda $$ is perfectly well-behaved. In particular, it enjoys cut elimination and an interpolation result. In addition, perhaps surprisingly, it is decidable. Finally, I prove that it is sound and complete with respect to the usual class of relational frames. (shrink)

Lambek elegantly characterized part of natural language. As is well-known, his substructural logic L, and its non-associative version NL, handle basic function/argument composition well, but not scope taking and syntactic displacement—at least, not in their full generality. In previous work, I propose \, which is NL supplemented with a single structural inference rule.ion closely resembles the traditional linguistic rule of quantifier raising, and characterizes both semantic scope taking and syntactic displacement. Due to the unconventional form of the abstraction inference, there (...) has been some doubt that \ should count at a legitimate substructural logic. This paper argues that \ is perfectly well-behaved. In particular, it enjoys cut elimination and an interpolation result. In addition, perhaps surprisingly, it is decidable. Finally, I prove that it is sound and complete with respect to the usual class of relational frames. (shrink)