An extension of the Craig-Lyndon interpolation theorem

Publisher Website
Google Scholar
Abstract
In a work widely quoted and applied,3 Craig has shown that if A and C are any formulas of predicate logic such that A├C, then there is a formula B such that (i) A├B and B├C, and (ii) each predicate symbol occurring in B occurs both in A and in C.4 If, in this theorem, we replace the syntactic notion of derivability, ├, by the semantical notion of consequence, ╞, the resulting proposition is of course equally valid, for by the (strong) completeness theorem of predicate logic5 the relations ├ and ╞ coincide in extension.

This publication has 6 references indexed in Scilit: