Craig interpolation
In
Example
In
- .
Then
- .
Thus, if holds, then holds. In turn, tautologically implies . Because the two propositional variables occurring in occur in both and , this means that 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
Lyndon's theorem says that if S ∪ T is unsatisfiable, then there is an 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
If ⊨φ → ψ then there is a ρ (the interpolant) such that ⊨φ → ρ and ⊨ρ → ψ, where atoms(ρ) ⊆ atoms(φ) ∩ atoms(ψ). Here atoms(φ) is the set of
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: Since |atoms(φ) − atoms(ψ)| = 0, we have that atoms(φ) ⊆ atoms(φ) ∩ atoms(ψ). Moreover we have that ⊨φ → φ and ⊨φ → ψ. This suffices to show that φ is a suitable interpolant in this case.
Let’s 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 q ∈ atoms(φ) but q ∉ atoms(ψ). Now define:
φ' := φ[⊤/q] ∨ φ[⊥/q]
Here φ[⊤/q] is the same as φ with every occurrence of q replaced by ⊤ and φ[⊥/q] similarly replaces q with ⊥. We may observe three things from this definition:
-
⊨φ' → ψ(1)
-
|atoms(φ') − atoms(ψ)| = n(2)
-
⊨φ → φ'(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
Craig interpolation can be proved by other methods as well. However, these proofs are generally
- model-theoretically, via Robinson's joint consistency theorem: in the presence of compactness, negation and conjunction, Robinson's joint consistency theorem and Craig interpolation are equivalent.
- subformula propertyholds, then Craig interpolation is provable via induction over the derivations.
- algebraically, using amalgamation theorems for the variety of algebras representing the logic.
- via translation to other logics enjoying Craig interpolation.
Applications
Craig interpolation has many applications, among them
References
- .
- ISBN 978-0-521-77911-1.
- ^ Harrison pgs. 426–427
- S2CID 10190144.
Further reading
- John Harrison (2009). Handbook of Practical Logic and Automated Reasoning. Cambridge, New York: ISBN 978-0-521-89957-4.
- Hinman, P. (2005). Fundamentals of Mathematical Logic. A K Peters. ISBN 1-56881-262-0.
- ISBN 978-0-19-851174-8.
- Eva Hoogland, Definability and Interpolation. Model-theoretic investigations. PhD thesis, Amsterdam 2001.
- W. Craig, Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory, The Journal of Symbolic Logic 22 (1957), no. 3, 269–285.