We investigate uniform interpolants in propositional modal logics from the proof-theoretical point of view. Our approach is adopted from Pitts’ proof of uniform interpolationin intuitionistic propositional logic [15]. The method is based on a simulation of certain quantifiers ranging over propositional variables and uses a terminating sequent calculus for which structural rules are admissible.

A method is presented that connects the existence of uniform interpolants to the existence of certain sequent calculi. This method is applied to several modal logics and is shown to cover known results from the literature, such as the existence of uniform interpolants for the modal logic \. New is the result that \ has uniform interpolation. The results imply that for modal logics \ and \, which are known not to have uniform interpolation, (...) certain sequent calculi cannot exist. (shrink)

We consider the relation between the uniform interpolation property and the elimination of non-standard quantifiers (the bisimulation quantifiers) in the context of the ?-calculus. In particular, we isolate classes of frames where the correspondence between these two properties is nicely smooth.

We consider the problem of the existence of uniform interpolants in the modal logic K4. We first prove that all \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\square}$$\end{document}-free formulas have uniform interpolants in this logic. In the general case, we shall prove that given a modal formula \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\phi}$$\end{document} and a sublanguage L of the language of the formula, we can decide whether \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} (...) \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\phi}$$\end{document} has a uniform interpolant with respect to L in K4. The \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\square}$$\end{document}-free case is proved using a reduction to the Gödel Löb Logic GL, while in the general case we prove that the question of whether a modal formula has uniform interpolants over transitive frames can be reduced to a decidable expressivity problem on the μ-calculus. (shrink)

A logic |$\mathcal{L}$| is said to satisfy the descending chain condition, DCC, if any descending chain of formulas in |$\mathcal{L}$| with ordering induced by |$\vdash _{\mathcal{L}};$| eventually stops. In this short note, we first establish a general theorem, which states that if a propositional logic |$\mathcal{L}$| satisfies both DCC and has the Craig Interpolation Property, CIP, then it satisfies the Uniform Interpolation Property, UIP, as well. As a result, by using the Nishimura lattice, we give a new (...) simply proof of uniform interpolation for |$\textbf{IPL}_2$|⁠, the two-variable fragment of Intuitionistic Propositional Logic; and one-variable uniform interpolation for |$\textbf{IPL}$|⁠. Also, we will see that the modal logics |$\textbf{S}_4$| and |$\textbf{K}_4$| do not satisfy atomic DCC. (shrink)

In this paper, a proof-theoretic method to prove uniform Lyndon interpolation for non-normal modal logics is introduced and applied to show that the logics E\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {E}$$\end{document}, M\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {M}$$\end{document}, MC\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {MC}$$\end{document}, EN\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {EN}$$\end{document}, MN\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {MN}$$\end{document} (...) have that property. In particular, these logics have uniform interpolation. Although for some of them the latter is known, the fact that they have uniform Lyndon interpolation is new. Also, the proof-theoretic proofs of these facts are new, as well as the constructive way to explicitly compute the interpolants that they provide. It is also shown that the non-normal modal logics EC\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {EC}$$\end{document} and ECN\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {ECN}$$\end{document} do not have Craig interpolation, and whence no uniform interpolation. (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)

We discuss the interpolation property on some important families of non classical logics, such as intuitionistic, modal, fuzzy, and linear logics. A special paragraph is devoted to a generalization of the interpolation property, uniform interpolation.

In this paper we investigate the connections between quantifier elimination, decidability and Uniform Craig Interpolation in Δ-core fuzzy logics added with propositional quantifiers. As a consequence, we are able to prove that several propositional fuzzy logics have a conservative extension which is a Δ-core fuzzy logic and has Uniform Craig Interpolation.

Interpolation has become one of the standard properties that logicians investigate when designing a logic. In this paper, we provide strong evidence that the presence of interpolants is not only cogent for scientific reasoning but has also important practical implications in computer science. We illustrate that interpolation in general, and uniform splitting interpolants, in particular, play an important role in applications where formality and modularity are invoked. In recognition of the fact that common logical formalisms often lack (...) uniform interpolants, we advocate the need for developing general methods to engineer a specification logic so that some critical uniform interpolants become available. (shrink)

If S ⊆{0,1}; * and S ′ = {0,1} * \sb S are both recognized within a certain nondeterministic time bound T then, in not much more time, one can write down tautologies A n → A′ n with unique interpolants I n that define S ∩{0,1} n ; hence, if one can rapidly find unique interpolants, then one can recognize S within deterministic time T p for some fixed p \s>0. In general, complexity measures for the problem of finding (...) unique interpolants in sentential logic yield new relations between circuit depth and nondeterministic Turing time, as well as between proof length and the complexity of decision procedures of logical theories. (shrink)

In this paper by using a model-theoretic approach, we prove Craig interpolation property for Formal Propositional Logic, FPL, Basic propositional logic, BPL and the uniform left-interpolation property for FPL. We also show that there are countably infinite extensions of FPL with the uniform interpolation property.

The semantic valuations of classical logic, strong Kleene logic, the logic of paradox and the logic of first-degree entailment, all respect the Dunn conditions: we call them Dunn logics. In this paper, we study the interpolation properties of the Dunn logics and extensions of these logics to more expressive languages. We do so by relying on the \ calculus, a signed tableau calculus whose rules mirror the Dunn conditions syntactically and which characterizes the Dunn logics in a uniform (...) way. In terms of the \ calculus, we first introduce two different interpolation methods, each of which uniformly shows that the Dunn logics have the interpolation property. One of the methods is closely related to Maehara’s method but the other method, which we call the pruned tableau method, is novel to this paper. We provide various reasons to prefer the pruned tableau method to the Maehara-style method. We then turn our attention to extensions of Dunn logics with so-called appropriate implication connectives. Although these logics have been considered at various places in the literature, a study of the interpolation properties of these logics is lacking. We use the pruned tableau method to uniformly show that these extended Dunn logics have the interpolation property and explain that the same result cannot be obtained via the Maehara-style method. Finally, we show how the pruned tableau method constructs interpolants for functionally complete extensions of the Dunn logics. (shrink)

This note exploits back-and-forth characteristics to construct, using a single method, short proofs for ten classics of first-order and modal logic: interpolation theorems, preservation theorems, and Lindström's theorem.

A semantical proof of Craig's interpolation theorem for the intuitionistic predicate logic and some intermediate prepositional logics will be given. Our proof is an extension of Henkin's method developed in [4]. It will clarify the relation between the interpolation theorem and Robinson's consistency theorem for these logics and will enable us to give a uniform way of proving the interpolation theorem for them.

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)

A definition is given for formulae $A_1,\ldots,A_n$ in some theory $T$ which is formalized in a propositional calculus $S$ to be (in)dependent with respect to $S$. It is shown that, for intuitionistic propositional logic $\mathbf{IPC}$, dependency (with respect to $\mathbf{IPC}$ itself) is decidable. This is an almost immediate consequence of Pitts' uniform interpolation theorem for $\mathbf{IPC}$. A reasonably simple infinite sequence of $\mathbf{IPC}$-formulae $F_n(p, q)$ is given such that $\mathbf{IPC}$-formulae $A$ and $B$ are dependent if and only if (...) at least on the $F_n(A, B)$ is provable. (shrink)

Ultrafilters play a significant role in model theory to characterize logics having various compactness and interpolation properties. They also provide a general method to construct extensions of first-order logic having these properties. A main result of this paper is that every class $\Omega $ of uniform ultrafilters generates a $\Delta $ -closed logic ${\mathcal {L}}_\Omega $. ${\mathcal {L}}_\Omega $ is $\omega $ -relatively compact iff some $D\in \Omega $ fails to be $\omega _1$ -complete iff ${\mathcal {L}}_\Omega $ (...) does not contain the quantifier “there are uncountably many.” If $\Omega $ is a set, or if it contains a countably incomplete ultrafilter, then ${\mathcal {L}}_\Omega $ is not generated by Mostowski cardinality quantifiers. Assuming $\neg 0^\sharp $ or $\neg L^{\mu }$, if $D\in \Omega $ is a uniform ultrafilter over a regular cardinal $\nu $, then every family $\Psi $ of formulas in ${\mathcal {L}}_\Omega $ with $|\Phi |\leq \nu $ satisfies the compactness theorem. In particular, if $\Omega $ is a proper class of uniform ultrafilters over regular cardinals, ${\mathcal {L}}_\Omega $ is compact. (shrink)

In any model theoretic logic, Beth’s definability property together with Feferman-Vaught’s uniform reduction property for pairs imply recursive compactness, and the existence of models with infinitely many automorphisms for sentences having infinite models. The stronger Craig’s interpolation property plus the uniform reduction property for pairs yield a recursive version of Ehrenfeucht-Mostowski’s theorem. Adding compactness, we obtain the full version of this theorem. Various combinations of definability and uniform reduction relative to other logics yield corresponding results on (...) the existence of non-rigid models. (shrink)

We introduce a natural class of quantifiersTh containing all monadic type quantifiers, all quantifiers for linear orders, quantifiers for isomorphism, Ramsey type quantifiers, and plenty more, showing that no sublogic ofL ωω (Th) or countably compact regular sublogic ofL ∞ω (Th), properly extendingL ωω , satisfies the uniform reduction property for quotients. As a consequence, none of these logics satisfies eitherΔ-interpolation or Beth's definability theorem when closed under relativizations. We also show the failure of both properties for any (...) sublogic ofL ∞ω (Th) in which Chang's quantifier or some cardinality quantifierQ α, with α≧1, is definable. (shrink)

This text centers around three main subjects. The first is the concept of modularity and independence in classical logic and nonmonotonic and other nonclassical logic, and the consequences on syntactic and semantical interpolation and language change. In particular, we will show the connection between interpolation for nonmonotonic logic and manipulation of an abstract notion of size. Modularity is essentially the ability to put partial results achieved independently together for a global result. The second aspect of the book is (...) the authors' uniform picture of conditionals, including many-valued logics and structures on the language elements themselves and on the truth value set. The third topic explained by the authors is neighbourhood semantics, their connection to independence, and their common points and differences for various logics, e.g., for defaults and deontic logic, for the limit version of preferential logics, and for general approximation"--Publisher. (shrink)

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)

This chapter examines global policing as it takes shape through the work of Interpol, the International Criminal Police Organization. Global policing emerges in the legal, political and technological amalgam through which transnational police cooperation is carried out, and includes the police practices inflected and made possible by this phenomenon. Interpol’s role is predominantly in the circulation of information, through which it enters into relationships and provides services that affect aspects of governance, from the local to national, regional and global. The (...) chapter describes this assemblage as a noteworthy experiment in developing what McKeon called a frame for common action. Drawing on Interpol publications, news stories, interviews with staff, and fieldwork at the General Secretariat in Lyon, France, the history, institutional structure, and daily practices are described. Three cases are analyzed, concerning Red Notices, national sovereignty, and terrorism, in order to explore some of the problems arising in Interpol’s political and technical operating arrangements. In conclusion, international and global policing are compared schematically, together with Interpol’s attempts to give institutional and procedural direction to the still-evolving form of global policing. (shrink)

In this article we show that bi-intuitionistic predicate logic lacks the Craig Interpolation Property. We proceed by adapting the counterexample given by Mints, Olkhovikov and Urquhart for intuitionistic predicate logic with constant domains [13]. More precisely, we show that there is a valid implication $\phi \rightarrow \psi $ with no interpolant. Importantly, this result does not contradict the unfortunately named ‘Craig interpolation’ theorem established by Rauszer in [24] since that article is about the property more correctly named ‘deductive (...) interpolation’ (see Galatos, Jipsen, Kowalski and Ono’s use of this term in [5]) for global consequence. Given that the deduction theorem fails for bi-intuitionistic logic with global consequence, the two formulations of the property are not equivalent. (shrink)

We analyse the structure of propositional proofs in the sequent calculus focusing on the well-known procedures of Interpolation and Cut Elimination. We are motivated in part by the desire to understand why a tautology might be ‘hard to prove’. Given a proof we associate to it a logical graph tracing the flow of formulas in it . We show some general facts about logical graphs such as acyclicity of cut-free proofs and acyclicity of contraction-free proofs , and we give (...) a proof of a strengthened version of the Craig Interpolation Theorem based on flows of formulas. We show that tautologies having minimal interpolants of non-linear size must have proofs with certain precise structural properties. We then show that given a proof Π and a cut-free form Π′ associated to it , certain subgraphs of Π′ which are logical graphs correspond to subgraphs of Π which are logical graphs for the same sequent. This locality property of cut elimination leads to new results on the complexity of interpolants, which cannot follow from the known constructions proving the Craig Interpolation Theorem. (shrink)

Preservation and interpolation results are obtained for L ∞ω and sublogics $\mathscr{L} \subseteq L_{\infty\omega}$ such that equivalence in L can be characterized by suitable back-and-forth conditions on sets of partial isomorphisms.

A new technique is presented for proving that a consequence system enjoys Craig interpolation or Maehara interpolation based on the fact that these properties hold in another consequence system. This technique is based on the existence of a back and forth translation satisfying some properties between the consequence systems. Some examples of translations satisfying those properties are described. Namely a translation between the global/local consequence systems induced by fragments of linear logic, a Kolmogorov-Gentzen-Gödel style translation, and a new (...) translation between the global consequence systems induced by full Lambek calculus and linear logic, mixing features of a Kiriyama-Ono style translation with features of a Kolmogorov-Gentzen-Gödel style translation. These translations establish a strong relationship between the logics involved and are used to obtain new results about whether Craig interpolation and Maehara interpolation hold in that logics . (shrink)

Preservation and interpolation results are obtained for L ∞ω and sublogics $\mathscr{L} \subseteq L_{\infty\omega}$ such that equivalence in L can be characterized by suitable back-and-forth conditions on sets of partial isomorphisms.

We investigate interpolation properties of many-valued propositional logics related to continuous t-norms. In case of failure of interpolation, we characterize the minimal interpolating extensions of the languages. For finite-valued logics, we count the number of interpolating extensions by Fibonacci sequences.

Several extensions of the basic modal language are characterized in terms of interpolation. Our main results are of the following form: Language ℒ' is the least expressive extension of ℒ with interpolation. For instance, let ℳ be the extension of the basic modal language with a difference operator [7]. First-order logic is the least expressive extension of ℳ with interpolation. These characterizations are subsequently used to derive new results about hybrid logic, relation algebra and the guarded fragment.

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.

Craig's interpolation lemma (if φ → ψ is valid, then φ → θ and θ → ψ are valid, for θ a formula constructed using only primitive symbols which occur both in φ and ψ) fails for many propositional and first order modal logics. The interpolation property is often regarded as a sign of well-matched syntax and semantics. Hybrid logicians claim that modal logic is missing important syntactic machinery, namely tools for referring to worlds, and that adding such (...) machinery solves many technical problems. The paper presents strong evidence for this claim by defining interpolation algorithms for both propositional and first order hybrid logic. These algorithms produce interpolants for the hybrid logic of every elementary class of frames satisfying the property that a frame is in the class if and only if all its point-generated subframes are in the class. In addition, on the class of all frames, the basic algorithm is conservative: on purely modal input it computes interpolants in which the hybrid syntactic machinery does not occur. (shrink)

We provide a direct method for proving Craig interpolation for a range of modal and intuitionistic logics, including those containing a "converse" modality. We demonstrate this method for classical tense logic, its extensions with path axioms, and for bi-intuitionistic logic. These logics do not have straightforward formalisations in the traditional Gentzen-style sequent calculus, but have all been shown to have cut-free nested sequent calculi. The proof of the interpolation theorem uses these calculi and is purely syntactic, without resorting (...) to embeddings, semantic arguments, or interpreted connectives external to the underlying logical language. A novel feature of our proof includes an orthogonality condition for defining duality between interpolants. (shrink)

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)

We show in this paper that all fragments of intuitionistic propostional logic based on a subset of the connectives $\wedge, \vee, \rightarrow, \neg$ satisfy interpolation. Fragments containing $\leftrightarrow$ or $\neg\neg$ are briefly considered.

An interpolation theorem holds for many standard modal logics, but first order $S5$ is a prominent example of a logic for which it fails. In this paper it is shown that a first order $S5$ interpolation theorem can be proved provided the logic is extended to contain propositional quantifiers. A proper statement of the result involves some subtleties, but this is the essence of it.

This paper defines the form of prior knowledge that is required for sound inferences by analogy and single-instance generalizations, in both logical and probabilistic reasoning. In the logical case, the first order determination rule defined in Davies (1985) is shown to solve both the justification and non-redundancy problems for analogical inference. The statistical analogue of determination that is put forward is termed 'uniformity'. Based on the semantics of determination and uniformity, a third notion of "relevance" is defined, both logically and (...) probabilistically. The statistical relevance of one function in determining another is put forward as a way of defining the value of information: The statistical relevance of a function F to a function G is the absolute value of the change in one's information about the value of G afforded by specifying the value of F. This theory provides normative justifications for conclusions projected by analogy from one case to another, and for generalization from an instance to a rule. The soundness of such conclusions, in either the logical or the probabilistic case, can be identified with the extent to which the corresponding criteria (determination and uniformity) actually hold for the features being related. (shrink)

An interpolation Theorem is proved for first order logic with infinitary predicates. Our proof is algebraic via cylindric algebras.1.

Decision theory requires agents to assign probabilities to states of the world and utilities to the possible outcomes of different actions. When agents commit to having the probabilities and/or utilities in a decision problem defined by objective features of the world, they may find themselves unable to decide which actions maximize expected utility. Decision theory has long recognized that work-around strategies are available in special cases; this is where dominance reasoning, minimax, and maximin play a role. Here we describe a (...) different work around, wherein a rational decision about one decision problem can be reached by ‘interpolating’ information from another problem that the agent believes has already been rationally solved. (shrink)

A uniform theory of conditionals is one which compositionally captures the behavior of both indicative and subjunctive conditionals without positing ambiguities. This paper raises new problems for the closest thing to a uniform analysis in the literature (Stalnaker, Philosophia, 5, 269–286 (1975)) and develops a new theory which solves them. I also show that this new analysis provides an improved treatment of three phenomena (the import-export equivalence, reverse Sobel-sequences and disjunctive antecedents). While these results concern central issues in (...) the study of conditionals, broader themes in the philosophy of language and formal semantics are also engaged here. This new analysis exploits a dynamic conception of meaning where the meaning of a symbol is its potential to change an agent’s mental state (or the state of a conversation) rather than being the symbol’s content (e.g. the proposition it expresses). The analysis of conditionals is also built on the idea that the contrast between subjunctive and indicative conditionals parallels a contrast between revising and consistently extending some body of information. (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.