Skip header navigation

University of Stirling

×

Article

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

StatusPublished
Author(s)Milne, Peter
Publication date31/12/2017
Publication date online08/2016
Date accepted by journal04/07/2016
URLhttp://hdl.handle.net/1893/24183
PublisherPeeters Publishers
ISSN0024-5836
Scroll back to the top