The Craig Interpolation Theorem states that if a first-order logical formula implies another, then there exists an intermediate formula, using only the non-logical symbols common to both, that is implied by the first and itself implies the second. Named for William Craig, it is a foundational result of model theory with applications throughout logic, including to definability and to modular reasoning in automated verification.
Facts
StatementIf a formula implies another formula and the two share at least one atomic variable symbol, then there is an interpolant formula whose non-logical symbols occur in both, which the first implies and which implies the second. 1 Sources
1. Craig's interpolation theorem, Wikipedia
Lead paragraph
Roughly stated, the theorem says that if a formula φ implies a formula ψ, and the two have at least one atomic variable symbol in common, then there is a formula ρ, called an interpolant, such that every non-logical symbol in ρ occurs both in φ and ψ, φ implies ρ, and ρ implies ψ.
Lead paragraph, sentence on first proof
The theorem was first proved for first-order logic by William Craig in 1957.
View the SourceReader Challenges (0)
No disputes yet. Spotted an error or a better source? Open the first one.
Sign in to dispute this or suggest a correction.