Craig Interpolant

Definition

For two formulas A and B such that A implies B, a Craig Interpolant is a formula I such that

1. A implies I
2. I implies B
3. the non-logical symbols of I occur in A and B.

this definition is independent of the logic system. A logic system has interpolation property, if it satisfies that, if $A⟹B$ is valid, then a Craig interpolant exists.

Craig proved that FOL has interpolation property. There is a constructive proof of the interpolation property of PL in Wikipedia. Proof for FOL can be found online

Lyndon later proves a stronger version.

reverse interpolant

If $A\wedge B$ is contradictory, a reverse interpolant is a formula I such that

1. A implies I
2. $I\wedge B$ is contradictory
3. the non-logical symbols of I occur in A and B.

note: the reverse interpolant of A and B is the interpolant of A and $\neg B$, since $A⟹B$ is valid iff $A\wedge \neg B$ is contradictory

in verification, interpolant usually means reverse interpolant