this issue
next article in this issue

Document Details :

Title: A Refinement of the Craig-Lyndon Interpolation Theorem for Classical First-Order Logic with Identity
Author(s): MILNE, Peter
Journal: Logique et Analyse
Volume: 240    Date: 2017   
Pages: 389-420
DOI: 10.2143/LEA.240.0.3254088

Abstract :
We refine the interpolation property of classical first-order logic (without identity and without function symbols), showing that if Γ ⊬, ⊬ Δ and Γ ⊢ Δ then there is an interpolant χ, constructed using only non-logical vocabulary common to both members of Γ and members of Δ, such that (i) Γ entails χ in the first-order version of Kleene’s strong three-valued logic, and (ii) χ entails Δ in the first-order version of Priest’s Logic of Paradox. The proof proceeds via a careful analysis of derivations employing semantic tableaux. Lyndon’s strengthening of the interpolation property falls out of an observation regarding such derivations and the steps involved in the construction of interpolants. Through an analysis of tableaux rules for identity, the proof is then extended to classical first-order logic with identity (but without function symbols).

Download article