In classical first-order logic, whenever ⊢ φ → ψ there exists an interpolant χ — a formula whose non-logical symbols appear in both φ and ψ — such that ⊢ φ → χ and ⊢ χ → ψ. Craig 1957. Drives the Beth definability theorem (implicit ⇒…
In classical first-order logic, whenever ⊢ φ → ψ there exists an interpolant χ — a formula whose non-logical symbols appear in both φ and ψ — such that ⊢ φ → χ and ⊢ χ → ψ. Craig 1957. Drives the Beth definability theorem (implicit ⇒…