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 ψ, and the two have at least one atomic variable symbol in common, then there is a formula ρ, called an interpolant, such that every non-logical 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 interpolation theorem for first-order logic was proved by Roger Lyndon in 1959; the overall result is sometimes called the Craig–Lyndon theorem.

Example

In propositional logic, let ::: \varphi = \lnot(P \land Q) \to (\lnot R \land Q) ::: \psi = (S \to P) \lor (S \to \lnot R) . Then \varphi tautologically implies \psi. This can be verified by writing \varphi in conjunctive normal form: :::\varphi \equiv (P \lor \lnot R) \land Q. Thus, if \varphi holds, then P \lor \lnot R holds. :::\rho = (P \lor \lnot R). In turn, P \lor \lnot R tautologically implies \psi. Because the two propositional variables occurring in P \lor \lnot R occur in both \varphi and \psi, this means that P \lor \lnot R is an interpolant for the implication \varphi \to \psi. == Lyndon's interpolation theorem ==

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 languages of the two theories; the signature of S ∩ T is the intersection of the signatures of the two languages. 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==

Proof of Craig's interpolation theorem

We present here a constructive proof of the Craig interpolation theorem for propositional logic. 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: • 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. • proof-theoretically, via a sequent calculus. If cut elimination is possible and as a result the subformula property holds, 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==

Applications

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

Source: Wikipedia ↗

tickerdossier.com tickerdossier.substack.com