Craig interpolation

Craig interpolation

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.

Contents

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:

φ ≡ (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 ST denote the smallest theory including both S and T; the signature of ST is the smallest one containing the signatures of S and T. Also let ST be the intersection of the two theories; the signature of ST is the intersection of the signatures of the two theories.

Lyndon's theorem says that if ST is unsatisfiable, then there is a interpolating sentence ρ in the language of ST 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 proof of the Craig interpolation theorem for propositional logic.[1] 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 patoms(φ) but patoms(ψ). 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 connectives 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:

Applications

Craig interpolation has many applications, among them consistency proofs, model checking, proofs in modular specifications, modular ontologies.

References

  1. ^ Harrison pgs. 426-427
  • John Harrison (2009). Handbook of Practical Logic and Automated Reasoning. Cambridge University Press. ISBN 0521899575. 
  • Hinman, P. (2005). Fundamentals of Mathematical Logic. A K Peters. ISBN 1-568-81262-0. 
  • Dov M. Gabbay and Larisa Maksimova (2006). Interpolation and Definability: Modal and Intuitionistic Logics (Oxford Logic Guides). Oxford science publications, Clarendon Press. ISBN 978-0198511748. 
  • 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.

Wikimedia Foundation. 2010.

Игры ⚽ Нужен реферат?

Look at other dictionaries:

  • Craig-Interpolation — Die Craig Interpolation ist ein Ausdruck der Logik. Der zugrunde liegende Satz (Craig’s Lemma, Interpolationstheorem) lautet folgendermaßen: Es seien T1 und T2 zwei Theorien und der Satz sei ein in ableitbarer Satz. Dann gilt: Es gibt ein B mit… …   Deutsch Wikipedia

  • Craig (Name) — Craig ist ein ursprünglich ortsbezogener männlicher Vorname und Familienname, der heute im gesamten englischen Sprachraum vorkommt. Inhaltsverzeichnis 1 Herkunft und Bedeutung 2 Namensträger 2.1 Familienname …   Deutsch Wikipedia

  • Craig — steht für: Craig (Name), einen männlichen Vornamen und Familiennamen Orte in den Vereinigten Staaten: Craig (Alaska) Craig (Colorado) Craig (Indiana) Craig (Iowa) Craig (Kalifornien) Craig (Kansas) Craig (Mississippi) Craig (Missouri) Craig… …   Deutsch Wikipedia

  • Craig's theorem — In mathematical logic, Craig s theorem states that any recursively enumerable set of well formed formulas of a first order language is (primitively) recursively axiomatizable. This result is not related to the well known Craig interpolation… …   Wikipedia

  • William Craig — ist der Name folgender Personen: William Craig (Logiker) (* 1918), amerikanischer Logiker (Craig Interpolation) William Craig (Politiker) (* 1924), nordirischer Politiker William Craig (Autor) (1929–1997), US amerikanischer Autor und Historiker… …   Deutsch Wikipedia

  • William Craig (logician) — William Craig (born 1918) 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… …   Wikipedia

  • Liste de théorèmes — par ordre alphabétique. Pour l établissement de l ordre alphabétique, il a été convenu ce qui suit : Si le nom du théorème comprend des noms de mathématiciens ou de physiciens, on se base sur le premier nom propre cité. Si le nom du théorème …   Wikipédia en Français

  • Institutional model theory — generalizes a large portion of first order model theory to an arbitrary logical system. The notion of logical system here is formalized as an institution. Institutions constitute a model oriented meta theory on logical systems similar to how the… …   Wikipedia

  • Cut-elimination — Der Gentzensche Hauptsatz oder Schnittsatz ist ein Satz der mathematischen Logik, der besagt, dass die Schnittregel in Gentzentypkalkülen gültig ist. Er ist nach Gerhard Gentzen benannt, der ihn 1934 aufstellte und bewies. Inhaltsverzeichnis 1… …   Deutsch Wikipedia

  • Schnittsatz — Der Gentzensche Hauptsatz oder Schnittsatz ist ein Satz der mathematischen Logik, der besagt, dass die Schnittregel in Gentzentypkalkülen gültig ist. Er ist nach Gerhard Gentzen benannt, der ihn 1934 aufstellte und bewies. Inhaltsverzeichnis 1… …   Deutsch Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”