The Interpolation Theorem, first formulated and proved by W. Craig fifty years ago for predicate logic, has been extended to many other logical frameworks and is being applied in several areas of computer science. We give a short overview, and focus on the theory of software systems and modules. An algebra of theories TA is presented, with a nonstandard interpretation of the existential quantifier . In TA, the interpolation property of the underlying logic corresponds with the quantifier combination property . (...) It is shown how the Modularization Theorem, the Factorization Lemma and the Normal Form Theorem for module expressions can be proved in TA. (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)

Craig interpolation theorem implies that the derivability of X,X′ Y′ implies existence of an interpolant I in the common language of X and X′ Y′ such that both X I and I,X′ Y′ are derivable. For classical logic this extends to X,X′ Y,Y′, but for intuitionistic logic there are counterexamples. We present a version true for intuitionistic propositional logic, and more complicated version for the predicate case.

We present a number of, somewhat unusual, ways of describing what Craig’s interpolation theorem achieves, and use them to identify some open problems and further directions.

We give complete sequent-like tableau systems for the modal logics KB, KDB, K5, and KD5. Analytic cut rules are used to obtain the completeness. Our systems have the analytic superformula property and can thus give a decision procedure. Using the systems, we prove the Craig interpolation lemma for the mentioned logics.

In earlier publications Jaakko Hintikka has introduced the interrogative model of inquiry and studied some of its applications.1 At its simplest, the interrogative model takes the form of a game between a player known as the Inquirer and a source of information we call Nature. The inquirer is trying to derive a conclusion C from a given set of premises T by standard deductive means augmented by additional information gained from Nature. (We can think of C as a set of (...) formulas related disjunctively to each other.) The inquirer may obtain this additional information by means of questions put to Nature. The answers to these questions, when available, are then added to the premise set T. When a question is answerable but no true answer is available, Nature may respond with a false answer.The deductive steps employed are subject to certain limitations. For instance, if the derivation is being carried out in a Beth-style tableau system, we require that the deductive steps obey the subformula principle.2. (shrink)

Lindström’s theorem obviously fails as a characterization of first-order logic without identity ( $\mathcal {L}_{\omega \omega }^{-} $ ). In this note, we provide a fix: we show that $\mathcal {L}_{\omega \omega }^{-} $ is a maximal abstract logic satisfying a weak form of the isomorphism property (suitable for identity-free languages and studied in [11]), the Löwenheim–Skolem property, and compactness. Furthermore, we show that compactness can be replaced by being recursively enumerable for validity under certain conditions. In the proofs, we (...) use a form of strong upwards Löwenheim–Skolem theorem not available in the framework with identity. (shrink)

"Necessity is the mother of invention. " Part I: What is in this book - details. There are several different types of formal proof procedures that logicians have invented. The ones we consider are: 1) tableau systems, 2) Gentzen sequent calculi, 3) natural deduction systems, and 4) axiom systems. We present proof procedures of each of these types for the most common normal modal logics: S5, S4, B, T, D, K, K4, D4, KB, DB, and also G, the logic that (...) has become important in applications of modal logic to the proof theory of Peano arithmetic. Further, we present a similar variety of proof procedures for an even larger number of regular, non-normal modal logics. We also consider some quasi-regular logics, including S2 and S3. Virtually all of these proof procedures are studied in both propositional and first-order versions. Finally, we present the full variety of proof methods for Intuitionistic logic. We actually give two quite different kinds of tableau systems for the logics we consider, two kinds of Gentzen sequent calculi, and two kinds of natural deduction systems. Each of the two tableau systems has its own uses; each provides us with different information about the logics involved. They complement each other more than they overlap. Of the two Gentzen systems, one is of the conventional sort, common in the literature. (shrink)

We prove an institutional version of A. Robinson ’s Consistency Theorem. This result is then appliedto the institution of many-sorted first-order predicate logic and to two of its variations, infinitary and partial, obtaining very general syntactic criteria sufficient for a signature square in order to satisfy the Robinson consistency and Craig interpolation properties.

The logic of the weak law of excluded middleKC p is obtained by adding the formula A A as an axiom scheme to Heyting's intuitionistic logicH p . A cut-free sequent calculus for this logic is given. As the consequences of the cut-elimination theorem, we get the decidability of the propositional part of this calculus, its separability, equality of the negationless fragments ofKC p andH p , interpolation theorems and so on. From the proof-theoretical point of view, the formulation presented (...) in this paper makes clearer the relations betweenKC p ,H p , and the classical logic. In the end, an interpretation of classical propositional logic in the propositional part ofKC p is given. (shrink)

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.

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.

We show that for any pair $\phi$ and $\psi$ of contradictory formulas of dependence logic there is a formula $\theta$ of the same logic such that $\phi\equiv\theta$ and $\psi\equiv\neg\theta$. This generalizes a result of Burgess.

Using the framework of categorical logic, this paper analyzes and streamlines Gabbay's semantical proof of the Craig interpolation theorem for intuitionistic predicate logic. In the process, an apparently new and interesting fact about the relation of coherent and intuitionistic logic is found.

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)

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.

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)

A form (or pattern) of inference, let us say, explicitlysubsumes just such particular inferences as are instances of the form, and implicitly subsumes thoseinferences with a premiss and conclusion logically equivalent to the premiss and conclusion of an instanceof the form in question. (For simplicity we restrict attention to one-premiss inferences.) A form ofinference is archetypal if it implicitly subsumes every correct inference. A precise definition (Section 1)of these concepts relativizes them to logics, since different logics classify different inferences ascorrect, (...) as well as ruling differently on the matter of logical equivalence which entered into the definitionof implicit subsumption. When relativized to classical propositional logic, we find (Section 2) thatall but a handful of `degenerate' inference forms turn out to be archetypal, whereas matters are verydifferent in this respect for the case of intuitionistic propositional logic (Sections 3 and 4), and an interestingstructure emerges in this case (the poset of equivalence classes of inference forms, with respect tothe equivalence relation of implicitly subsuming the same inferences). Thus a more accurate, if excessivelylong-winded title would be 'Archetypal and Non-Archetypal Forms of Inference in Classical andIntuitionistic Propositional Logic'. Some left-overs are postponed for a final discussion (Section 5).The overall intention is to introduce a new subject matter rather than to have the last word on thequestions it raises; indeed several significant questions are left as open problems. (shrink)

Hempel and Oppenheim, in their paper 'The Logic of Explanation', have offered an analysis of the notion of scientific explanation. The present paper advances considerations in the light of which their analysis seems inadequate. In particular, several theorems are proved with roughly the following content: between almost any theory and almost any singular sentence, certain relations of explainability hold.

We ask, when is a property of a model a logical property? According to the so-called Tarski–Sher criterion this is the case when the property is preserved by isomorphisms. We relate this to model-theoretic characteristics of abstract logics in which the model class is definable. This results in a graded concept of logicality in the terminology of Sagi [46]. We investigate which characteristics of logics, such as variants of the Löwenheim–Skolem theorem, Completeness theorem, and absoluteness, are relevant from the logicality (...) point of view, continuing earlier work by Bonnay, Feferman, and Sagi. We suggest that a logic is the more logical the closer it is to first order logic. We also offer a refinement of the result of McGee that logical properties of models can be expressed in $L_{\infty \infty }$ if the expression is allowed to depend on the cardinality of the model, based on replacing $L_{\infty \infty }$ by a “tamer” logic. (shrink)

Given some links between Lyndon’s Interpolation Theorem, term distribution, and Sommers and Englebretsen’s logic, in this contribution we attempt to capture a sense of interpolation for Sommers and Englebretsen’s Term Functor Logic. In order to reach this goal we first expound the basics of Term Functor Logic, together with a sense of term distribution, and then we offer a proof of our main contribution.

In this note we study a counterpart in predicate logic of the notion of logical friendliness, introduced into propositional logic in [15]. The result is a new consequence relation for predicate languages with equality using first-order models. While compactness, interpolation and axiomatizability fail dramatically, several other properties are preserved from the propositional case. Divergence is diminished when the language does not contain equality with its standard interpretation.

The rules for Core Logic are stated, and various important results about the system are summarized. We describe its relationship to other systems, such as Classical Logic, Intuitionistic Logic, Minimal Logic, and the Anderson–Belnap relevance logicR. A precise, positive explication is offered of what it is for the premises of a proof to connect relevantly with its conclusion. This characterization exploits the notion of positive and negative occurrences of atoms in sentences. It is shown that all Core proofs are relevant (...) in this precisely defined sense. We survey extant results about variable-sharing in rival systems of relevance logic, and find that the variable-sharing conditions established for them are weaker than the one established here for Core Logic (and for its classical extension). Proponents of other systems of relevance logic (such asRand its subsystems) are challenged to formulate a stronger variable-sharing condition, and to prove thatRor any of its subsystems satisfies it, but that Core Logic does not. We give reasons for pessimism about the prospects for meeting this challenge. (shrink)

After some motivating remarks in Section 1, in Section 2 we show how to replace an axiomatic basis for any one of a broad range of sentential logics having finitely many axiom schemes and Modus Ponens as the sole proper rule, by a basis with the same axiom schemes and finitely many one-premiss rules. Section 3 mentions some questions arising from this replacement procedure , explores another such procedure, and discusses some aspects of the consequence relations associated with the different (...) axiomatizations in play. Several open problems are mentioned. An appendix briefly treats the issue of a similar ‘at most one-premiss rules’ reformulation of proof systems with sequent-to-sequent rules. (shrink)

A structure which generalizes formulas by including substitution terms is used to represent proofs in classical logic. These structures, called expansion trees, can be most easily understood as describing a tautologous substitution instance of a theorem. They also provide a computationally useful representation of classical proofs as first-class values. As values they are compact and can easily be manipulated and transformed. For example, we present an explicit transformations between expansion tree proofs and cut-free sequential proofs. A theorem prover which represents (...) proofs using expansion trees can use this transformation to present its proofs in more human-readable form. Also a very simple computation on expansion trees can transform them into Craig-style linear reasoning and into interpolants when they exist. We have chosen a sublogic of the Simple Theory of Types for our classical logic because it elegantly represents substitutions at all finite types through the use of the typed -calculus. Since all the proof-theoretic results we shall study depend heavily on properties of substitutions, using this logic has allowed us to strengthen and extend prior results: we are able to prove a strengthen form of the firstorder interpolation theorem as well as provide a correct description of Skolem functions and the Herbrand Universe. The latter are not straightforward generalization of their first-order definitions. (shrink)