Craig interpolation
Encyclopedia
In mathematical logic
, Craig's interpolation theorem is a result about the relationship between different logical theories
. Roughly stated, the theorem says that if a formula φ implies a formula ψ then there is a third formula ρ, called an interpolant, such that every nonlogical symbol in ρ occurs both in φ and ψ, φ implies ρ, and ρ implies ψ. The theorem was first proved for first-order logic
by William Craig
in 1957. Variants of the theorem hold for other logics, such as propositional logic. A stronger form of Craig's theorem for first-order logic was proved by Roger Lyndon
in 1959; the overall result is sometimes called the Craig–Lyndon theorem.
Then φ tautologically implies ψ. This can be verified by writing φ in conjunctive normal form
:
Thus, if φ holds, then (P ∨ ~R) holds. In turn, (P ∨ ~R) tautologically implies ψ. Because the two propositional variables occurring in (P ∨ ~R) occur in both φ and ψ, this means that (P ∨ ~R) is an interpolant for the implication φ → ψ.
Lyndon's theorem says that if S ∪ T is unsatisfiable, then there is a interpolating sentence ρ in the language of S ∩ T that is true in all models of S and false in all models of T. Moreover, ρ has the stronger property that every relation symbol that has a positive occurrence in ρ has a positive occurrence in some formula of S and a negative occurrence in some formula of T, and every relation symbol with a negative occurrence in ρ has a negative occurrence in some formula of S and a positive occurrence in some formula of T.
of the Craig interpolation theorem for propositional logic. Formally, the theorem states:
If ⊨φ → ψ then there is a ρ (the interpolant) such that ⊨φ → ρ and ⊨ρ → ψ, where atoms(ρ) ⊆ atoms(φ) ∩ atoms(ψ). Here atoms(φ) here is the set of propositional variables
occurring in φ, and ⊨ is the semantic entailment relation
for propositional logic.
Proof.
Assume ⊨φ → ψ. The proof proceeds by induction on the number of propositional variables occurring in φ that do not occur in ψ, denoted |atoms(φ) - atoms(ψ)|.
Base case |atoms(φ) - atoms(ψ)| = 0: In this case, φ is suitable. This is because since |atoms(φ) - atoms(ψ)| = 0, we know that atoms(φ) ⊆ atoms(φ) ∩ atoms(ψ). Moreover we have that ⊨φ → φ and ⊨φ → ψ. This suffices to show that φ is a suitable interpolant in this case.
Next assume for the inductive step that the result has been shown for all χ where |atoms(χ) - atoms(ψ)| = n. Now assume that |atoms(φ) - atoms(ψ)| = n+1. Pick a p ∈ atoms(φ) but p ∉ atoms(ψ). Now define:
φ' := φ[⊤/p] ∨ φ[⊥/p]
Here φ[⊤/p] is the same as φ with every occurrence of p replaced by ⊤ and φ[⊥/p] similarly replaces p with ⊥. We may observe three things from this definition:
(1) ⊨φ' → ψ
(2) |atoms(φ') - atoms(ψ)| = n
(3) ⊨φ → φ'
From (1), (2) and the inductive step we have that there is an interpolant ρ such that:
(4) ⊨φ' → ρ
(5) ⊨ρ → ψ
But from (3) and (4) we know that
(6) ⊨φ → ρ
Hence, ρ is a suitable interpolant for φ and ψ.
QED
Since the above proof is constructive, one may extract an algorithm
for computing interpolants. Using this algorithm, if n = |atoms(φ') - atoms(ψ)|, then the interpolant ρ has O(EXP(n)) more logical connective
s than φ (see Big O Notation
for details regarding this assertion). Similar constructive proofs may be provided for the basic modal logic
K, intuitionistic logic
and μ-calculus, with similar complexity measures.
Craig interpolation can be proved by other methods as well. However, these proofs are generally non-constructive:
s, model checking
, proofs in modular
specifications
, modular ontologies
.
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, Craig's interpolation theorem is a result about the relationship between different logical theories
Theory (mathematical logic)
In mathematical logic, a theory is a set of sentences in a formal language. Usually a deductive system is understood from context. An element \phi\in T of a theory T is then called an axiom of the theory, and any sentence that follows from the axioms is called a theorem of the theory. Every axiom...
. Roughly stated, the theorem says that if a formula φ implies a formula ψ then there is a third formula ρ, called an interpolant, such that every nonlogical symbol in ρ occurs both in φ and ψ, φ implies ρ, and ρ implies ψ. The theorem was first proved for first-order logic
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
by William Craig
William Craig (logician)
William Lane Craig is Emeritus professor of Philosophy at University of California, Berkeley in Berkeley, California. His interests include mathematical logic, and philosophy of science. He is mostly known for the Craig interpolation theorem.Craig received his Ph.D. at Harvard University.-...
in 1957. Variants of the theorem hold for other logics, such as propositional logic. A stronger form of Craig's theorem for first-order logic was proved by Roger Lyndon
Roger Lyndon
Roger Conant Lyndon was an American mathematician, for many years a professor at the University of Michigan. He is known for Lyndon words, the Curtis–Hedlund–Lyndon theorem, Craig–Lyndon interpolation and the Lyndon–Hochschild–Serre spectral sequence.-Biography:Lyndon was born on December 18, 1917...
in 1959; the overall result is sometimes called the Craig–Lyndon theorem.
Example
In propositional logic, let- φ = ~(P ∧ Q) → (~R ∧ Q)
- ψ = (T → P) ∨ (T → ~R).
Then φ tautologically implies ψ. This can be verified by writing φ in conjunctive normal form
Conjunctive normal form
In Boolean logic, a formula is in conjunctive normal form if it is a conjunction of clauses, where a clause is a disjunction of literals.As a normal form, it is useful in automated theorem proving...
:
- φ ≡ (P ∨ ~R) ∧ Q.
Thus, if φ holds, then (P ∨ ~R) holds. In turn, (P ∨ ~R) tautologically implies ψ. Because the two propositional variables occurring in (P ∨ ~R) occur in both φ and ψ, this means that (P ∨ ~R) is an interpolant for the implication φ → ψ.
Lyndon's interpolation theorem
Suppose that S and T are two first-order theories. As notation, let S ∪ T denote the smallest theory including both S and T; the signature of S ∪ T is the smallest one containing the signatures of S and T. Also let S ∩ T be the intersection of the two theories; the signature of S ∩ T is the intersection of the signatures of the two theories.Lyndon's theorem says that if S ∪ T is unsatisfiable, then there is a interpolating sentence ρ in the language of S ∩ T that is true in all models of S and false in all models of T. Moreover, ρ has the stronger property that every relation symbol that has a positive occurrence in ρ has a positive occurrence in some formula of S and a negative occurrence in some formula of T, and every relation symbol with a negative occurrence in ρ has a negative occurrence in some formula of S and a positive occurrence in some formula of T.
Proof of Craig's interpolation theorem
We present here a constructive proofConstructive proof
In mathematics, a constructive proof is a method of proof that demonstrates the existence of a mathematical object with certain properties by creating or providing a method for creating such an object...
of the Craig interpolation theorem for propositional logic. Formally, the theorem states:
If ⊨φ → ψ then there is a ρ (the interpolant) such that ⊨φ → ρ and ⊨ρ → ψ, where atoms(ρ) ⊆ atoms(φ) ∩ atoms(ψ). Here atoms(φ) here is the set of propositional variables
Propositional variable
In mathematical logic, a propositional variable is a variable which can either be true or false...
occurring in φ, and ⊨ is the semantic entailment relation
Entailment
In logic, entailment is a relation between a set of sentences and a sentence. Let Γ be a set of one or more sentences; let S1 be the conjunction of the elements of Γ, and let S2 be a sentence: then, Γ entails S2 if and only if S1 and not-S2 are logically inconsistent...
for propositional logic.
Proof.
Assume ⊨φ → ψ. The proof proceeds by induction on the number of propositional variables occurring in φ that do not occur in ψ, denoted |atoms(φ) - atoms(ψ)|.
Base case |atoms(φ) - atoms(ψ)| = 0: In this case, φ is suitable. This is because since |atoms(φ) - atoms(ψ)| = 0, we know that atoms(φ) ⊆ atoms(φ) ∩ atoms(ψ). Moreover we have that ⊨φ → φ and ⊨φ → ψ. This suffices to show that φ is a suitable interpolant in this case.
Next assume for the inductive step that the result has been shown for all χ where |atoms(χ) - atoms(ψ)| = n. Now assume that |atoms(φ) - atoms(ψ)| = n+1. Pick a p ∈ atoms(φ) but p ∉ atoms(ψ). Now define:
φ' := φ[⊤/p] ∨ φ[⊥/p]
Here φ[⊤/p] is the same as φ with every occurrence of p replaced by ⊤ and φ[⊥/p] similarly replaces p with ⊥. We may observe three things from this definition:
(1) ⊨φ' → ψ
(2) |atoms(φ') - atoms(ψ)| = n
(3) ⊨φ → φ'
From (1), (2) and the inductive step we have that there is an interpolant ρ such that:
(4) ⊨φ' → ρ
(5) ⊨ρ → ψ
But from (3) and (4) we know that
(6) ⊨φ → ρ
Hence, ρ is a suitable interpolant for φ and ψ.
QED
Since the above proof is constructive, one may extract an algorithm
Algorithm
In mathematics and computer science, an algorithm is an effective method expressed as a finite list of well-defined instructions for calculating a function. Algorithms are used for calculation, data processing, and automated reasoning...
for computing interpolants. Using this algorithm, if n = |atoms(φ') - atoms(ψ)|, then the interpolant ρ has O(EXP(n)) more logical connective
Logical connective
In logic, a logical connective is a symbol or word used to connect two or more sentences in a grammatically valid way, such that the compound sentence produced has a truth value dependent on the respective truth values of the original sentences.Each logical connective can be expressed as a...
s than φ (see Big O Notation
Big O notation
In mathematics, big O notation is used to describe the limiting behavior of a function when the argument tends towards a particular value or infinity, usually in terms of simpler functions. It is a member of a larger family of notations that is called Landau notation, Bachmann-Landau notation, or...
for details regarding this assertion). Similar constructive proofs may be provided for the basic modal logic
Modal logic
Modal logic is a type of formal logic that extends classical propositional and predicate logic to include operators expressing modality. Modals — words that express modalities — qualify a statement. For example, the statement "John is happy" might be qualified by saying that John is...
K, intuitionistic logic
Intuitionistic logic
Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...
and μ-calculus, with similar complexity measures.
Craig interpolation can be proved by other methods as well. However, these proofs are generally non-constructive:
- model-theoreticallyModel theoryIn mathematics, model theory is the study of mathematical structures using tools from mathematical logic....
, via Robinson's joint consistency theoremRobinson's joint consistency theoremRobinson's joint consistency theorem is an important theorem of mathematical logic. It is related to Craig interpolation and Beth definability.The classical formulation of Robinson's joint consistency theorem is as follows:...
: in presence of compactnessCompactness theoremIn mathematical logic, the compactness theorem states that a set of first-order sentences has a model if and only if every finite subset of it has a model...
, negation and conjunction, Robinson's joint consistency theorem and Craig interpolation are equivalent. - proof-theoreticallyProof theoryProof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...
, via a Sequent calculusSequent calculusIn proof theory and mathematical logic, sequent calculus is a family of formal systems sharing a certain style of inference and certain formal properties. The first sequent calculi, systems LK and LJ, were introduced by Gerhard Gentzen in 1934 as a tool for studying natural deduction in...
. If cut elimination is possible and as a result the subformula property holds, then Craig interpolation is provable via induction over the derivations. - algebraicallyAbstract Algebraic LogicIn mathematical logic, abstract algebraic logic is the study of the algebraization of deductive systemsarising as an abstraction of the well-known Lindenbaum-Tarski algebra, and how the resulting algebras are related to logical systems.-Overview:...
, using amalgamation theorems for the varietyVariety (universal algebra)In mathematics, specifically universal algebra, a variety of algebras is the class of all algebraic structures of a given signature satisfying a given set of identities. Equivalently, a variety is a class of algebraic structures of the same signature which is closed under the taking of homomorphic...
of algebras representing the logic. - via translation to other logics enjoying Craig interpolation.
Applications
Craig interpolation has many applications, among them consistency proofConsistency proof
In logic, a consistent theory is one that does not contain a contradiction. The lack of contradiction can be defined in either semantic or syntactic terms. The semantic definition states that a theory is consistent if and only if it has a model, i.e. there exists an interpretation under which all...
s, model checking
Model checking
In computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....
, proofs in modular
Modularity (programming)
Modular programming is a software design technique that increases the extent to which software is composed of separate, interchangeable components called modules by breaking down program functions into modules, each of which accomplishes one function and contains everything necessary to accomplish...
specifications
Specification language
A specification language is a formal language used in computer science.Unlike most programming languages, which are directly executable formal languages used to implement a system, specification languages are used during systems analysis, requirements analysis and systems design.Specification...
, modular ontologies
Ontology (computer science)
In computer science and information science, an ontology formally represents knowledge as a set of concepts within a domain, and the relationships between those concepts. It can be used to reason about the entities within that domain and may be used to describe the domain.In theory, an ontology is...
.