next article in this issue |
Preview first page |
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). |
|