Craig interpolation

Craig interpolation is a theorem stating that if a sentence entails another, an intermediate sentence using only their shared nonlogical vocabulary can express the entailment.

Connect

Logical entailment: A relation holding when every interpretation that makes premises true also makes a conclusion true. Interpolation starts with an entailment and factors it through an intermediate sentence.
William Craig: An American logician known for work on mathematical logic, including the interpolation theorem named after him. Craig proved the theorem in 1957 and gave it its enduring name.
Uniform interpolation: A stronger interpolation property requiring one formula to work uniformly across a chosen vocabulary. It strengthens ordinary interpolation by replacing dependence on a particular conclusion with a uniform condition.
Cut-elimination theorem: A theorem stating that proofs in certain calculi can avoid the cut inference rule. Cut elimination often proves interpolation, but it is a proof method rather than the interpolation property itself.
Interpolant: A sentence that lies between two entailed sentences while satisfying a specified vocabulary constraint. It is the intermediate sentence whose existence Craig interpolation guarantees.
1957 in science: The year 1957, a period associated with notable developments across scientific disciplines. Craig published his interpolation result in 1957.
Craig interpolation in model checking: The use of interpolants to derive abstractions and invariants in automated verification of transition systems. Interpolants can summarize unreachable state combinations and help prove system safety.
Craig interpolation in intuitionistic logic: The interpolation property for intuitionistic logic, where entailment is interpreted intuitionistically. The intuitionistic version holds under its own proof-theoretic conditions, unlike a mere change of notation.
Nonlogical vocabulary: The symbols of a formal language other than its logical constants and variables. An interpolant may use only the nonlogical symbols shared by the endpoint sentences.
Proof theory: The study of the structure and properties of mathematical proofs. Interpolation became a major structural theorem in proof theory.