A refinement of the Craig-Lyndon Interpolation Theorem for classical first-order logic (with identity)

Citation

Milne P (2017) A refinement of the Craig-Lyndon Interpolation Theorem for classical first-order logic (with identity). Logique et Analyse, 60 (240), pp. 389-420. https://doi.org/10.2143/LEA.240.0.3254088

Abstract
We refine the interpolation property of classical first-order logic (without identity and without functionsymbols), showing that if G & , & D and G $ D then there is an interpolant c, constructed using onlynon-logical vocabulary common to both members of G and members of D, such that (i) G entails c in thefirst-order version of Kleene's strong three-valued logic, and (ii) c entails D in the first-order version ofPriest's Logic of Paradox. The proof proceeds via a careful analysis of derivations employing semantictableaux. Lyndon's strengthening of the interpolation property falls out of an observation regardingsuch 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-orderlogic with identity (but without function symbols).

Keywords
Craig–Lyndon Interpolation Theorem (for classical first-order logic); Kleene’s strong 3-valued logic; Priest’s Logic of Paradox; Belnap’s four-valued logic; block tableaux

Journal
Logique et Analyse: Volume 60, Issue 240