The sentence between a premise and its consequence

A proof with no lemma in it never leaves its goal’s own subformulas. That was introduced as the property that makes such proofs searchable — nothing about the goal says which lemma to try, so a proof that tries none is a proof that can be looked for.

The same property has a second consequence, and it is about vocabulary rather than search.

Whenever $A$ implies $B$, there is a sentence $I$ that uses only the atoms $A$ and $B$ have in common, such that $A$ implies $I$ and $I$ implies $B$. That is William Craig’s interpolation theorem, from 1957, and $I$ is called an interpolant. In the figure the interpolant is $r \lor s$: what $A$ says about $p$ and $q$ is irrelevant to $B$, which has never heard of them, and what $A$ says that $B$ can use is exactly that $r$ or $s$ holds.

Only the shared words can matter #

The theorem sounds like a technicality and is closer to a statement about communication.

$A$ is a claim about the atoms $p$, $q$, $r$ and $s$. $B$ is a claim about $r$, $s$ and $t$. For $A$ to force $B$, the only channel through which it can do so is what it says about $r$ and $s$, because nothing $A$ says about $p$ and $q$ can constrain $t$, and nothing it says constrains $t$ directly. The interpolant is the content of that channel: everything $A$ has to say about the shared atoms that is needed for $B$, and nothing about the atoms only one side uses.

That is why a formula mentioning $p$ could never serve. Whatever it says about $p$, $B$ cannot use; and if the formula’s truth depended on $p$, there would be values of $p$ making it false while $A$ still held, or true while $B$ still failed. The theorem is the claim that the channel is always wide enough — that whenever $A$ implies $B$ at all, it does so through a statement in their shared vocabulary.

Reading it off a refutation #

The figure does not search for an interpolant. It extracts one from a proof, and the proof is a resolution refutation.

Resolution works on clauses — disjunctions of atoms and their negations — and has a single rule: from a clause containing an atom and another containing its negation, derive the clause with both removed. The same rule, checked against a truth table, refutes a set of clauses exactly when no assignment satisfies them all, and $A$ implies $B$ exactly when $A$ together with the denial of $B$ is unsatisfiable. So the figure turns $A$ into clauses over $A$’s own atoms, turns $\lnot B$ into clauses over $B$’s own atoms, and resolves until the empty clause appears.

Every clause in the refutation then gets a label, by four rules due to Kenneth McMillan. A clause that came from $A$ is labelled with the part of it that uses shared atoms — its literals on $p$ and $q$ dropped. A clause that came from $\lnot B$ is labelled “true.” When two clauses are resolved on an atom that only $A$ mentions, the new clause’s label is the disjunction of the two labels; when they are resolved on any other atom, it is the conjunction. The label of the empty clause is the interpolant.

The rules, run by hand #

The rules are easier to believe on an example small enough to follow completely.

Take $A = p \land (\lnot p \lor r)$ and $B = r \lor s$. As clauses, $A$ is $p$ and $\lnot p \lor r$, and the denial of $B$ is $\lnot r$ and $\lnot s$. The shared atom is $r$; only $A$ mentions $p$, and only $B$ mentions $s$.

The four starting labels come straight from the rules. The clause $p$ is from $A$ and has no shared literal, so its label is “false”. The clause $\lnot p \lor r$ is from $A$ and its shared part is $r$, so its label is $r$. The two clauses from $\lnot B$ are labelled “true”.

Resolving $p$ with $\lnot p \lor r$ on $p$ gives the clause $r$. The atom $p$ belongs to $A$ alone, so the new label is the disjunction of the two, “false or $r$”, which is $r$. Resolving $r$ with $\lnot r$ on $r$ gives the empty clause. The atom $r$ is shared, so the label is the conjunction, “$r$ and true”, which is $r$. The interpolant is $r$: $A$ says $p$ and that $p$ forces $r$, so $A$ implies $r$, and $r$ implies $r \lor s$.

Two things are visible that the general statement hides. The clause $\lnot s$ was never used, and the atom $s$ never entered a label — the clauses from $\lnot B$ contribute only “true”, which is how an interpolant stays clear of the atoms only $B$ mentions. And the disjunction at the first step has a reason. The two labels are what $A$ guarantees in the two cases for $p$, an atom $B$ cannot see; since the outcome for $p$ is invisible from $B$’s side, what passes across is only that one of the two labels holds. When the atom resolved is one both sides see, both labels are needed at once, and they are joined by a conjunction.

The rules keep one property of every clause’s label, and at the empty clause that property becomes exactly the two implications the figure checks: $A$ implies the label, and the label together with $\lnot B$ is contradictory — which is to say the label implies $B$. The labels are built from shared literals, “true” and the two connectives, so the result can mention nothing else. The figure checks all three facts on every assignment rather than trusting the construction.

A strongest and a weakest #

There is usually more than one interpolant, and all of them sit in a definite range.

The strongest interpolant is $A$ with its private atoms removed by allowing them any value: the set of assignments to the shared atoms that can be extended to make $A$ true. Anything $A$ implies about the shared atoms is implied by this. The weakest is $B$ with its private atoms required to work for every value: the set of assignments to the shared atoms that make $B$ true whatever $t$ is. Every interpolant implies the weakest and is implied by the strongest, and every sentence in the shared atoms that lies between them is an interpolant.

The grid is the range drawn. The strongest interpolant is true at one of the four shared assignments, the weakest at two, and the one read off the refutation happens to coincide with the strongest. A different refutation of the same two formulas could have handed over $r$, or anything else true at the assignment $r s$ and false wherever $r$ is false.

The refutation’s answer is correct and not canonical. It depends on which resolutions were performed and in which order, and the formula it produces is written the way the refutation built it — here as a conjunction of three clauses that says no more than $r \land s$. The figure finds the short equivalent and checks the equivalence, because a correct interpolant that nobody can read has not told anybody what the channel between $A$ and $B$ carried.

The same range, seen on a cube #

The strongest and weakest interpolants have a picture that makes their definitions look inevitable.

An assignment to $n$ atoms is a corner of an $n$-dimensional cube, and a formula is the set of corners where it is true. $A$ lives on the cube of its own atoms and $B$ on the cube of its own, and the shared atoms span a face that both cubes project onto.

The strongest interpolant is the shadow of $A$ on that face: a shared corner is in it exactly when some corner of $A$’s cube above it makes $A$ true. Casting the shadow is what “allowing the private atoms any value” means. The weakest interpolant is the set of shared corners whose whole column in $B$’s cube lies inside $B$: a shared corner is in it exactly when every value of $t$ above it makes $B$ true.

That $A$ implies $B$ says the shadow sits inside the set of full columns, and every interpolant is a set of shared corners lying between them. The grids in the figures are those three sets drawn on the face, one row each. Enumerating corners is how the figures compute the two extremes — sixteen assignments or thirty-two, against which each extracted interpolant is compared — and it is also why the extremes are propositional luxuries: a cube with infinitely many corners casts no shadow that can be computed by looking at them.

Why a lemma would spoil it #

The extraction reads the interpolant off a refutation in which every clause was built from clauses of $A$ and $\lnot B$, and every atom in every clause was already in one of them. That confinement is what lets the labels stay inside the shared vocabulary, and it is the subformula property in the setting of resolution.

A proof with a lemma has no such confinement.

The lemma $s \lor \lnot s$ is true and useless, and it brings in an atom neither side of the implication mentions. An interpolant built by walking such a proof would have no reason to avoid $s$. Craig’s theorem is a consequence of the fact that lemmas can be removed: take any proof, remove its lemmas, and in the proof that remains every formula is made of the words the conclusion already used — which is where the interpolant’s words come from. The extraction on this page is that argument carried out on resolution, where there were never any lemmas to remove.

The same extraction works on the other proof systems in this collection, because each has a form without detours. A semantic tableau that closes can be labelled branch by branch in the same spirit, and a natural-deduction derivation with its detours removed has the subformula property that the labelling needs. What differs is only the bookkeeping; what is shared is that a proof records what it used, and a proof with no lemma used nothing outside the problem.

What interpolation is used for #

Craig proved the theorem in order to prove another one, and it is a theorem about what a vocabulary can say — the question a game between two players settles for a different purpose. Evert Beth had shown in 1953 that in first-order logic, if a theory pins a concept down uniquely — any two interpretations agreeing on everything else must agree on it — then the theory already contains an explicit definition of the concept. Craig’s interpolation theorem gives a short proof: uniqueness says that one copy of the concept implies another, and the interpolant between them, being in the shared vocabulary, is a definition that mentions neither copy.

Roger Lyndon sharpened the theorem in 1959: the interpolant can be chosen so that every atom appears in it only with a sign it has in both $A$ and $B$, positively where both use it positively and negatively where both use it negatively. The figure’s first example obeys that — $r$ and $s$ occur only positively in both formulas, and the interpolant $r \lor s$ has them only positively.

The theorem has also become practical. Systems that check whether a design can reach a bad state use interpolants as summaries: a refutation showing that no bad state is reached within some number of steps yields an interpolant describing, in the vocabulary of the current step alone, a set of states that includes every reachable one and excludes every bad one. The interpolant is an abstraction that the proof chose, rather than one a person had to guess.

Where the theorem needs its hypotheses #

$A$ must actually imply $B$. There is nothing to interpolate otherwise, and the figures check the implication on every assignment before building anything.

The shared vocabulary may be empty. Then the interpolant has no atoms and must be a constant. If it is “false”, $A$ was unsatisfiable on its own; if it is “true”, $B$ was valid on its own. The theorem is still true and says something sharp: a premise and a consequence with nothing in common can only be related by one of them being trivial.

The formulas here are propositional and small. The figures turn each formula into clauses by listing the assignments that falsify it, which is exact and grows with the number of atoms, and they keep to at most six atoms between the two formulas for that reason.

And the figures check the interpolant, not the extraction’s invariant. The two implications and the vocabulary are tested on every assignment. The property the labelling rules maintain at intermediate clauses is what makes the construction correct in general, and it is quoted rather than drawn.

One interpolant a pair, and labels computed but not drawn #

The figures show three pairs of formulas and one interpolant each, read off one refutation. The theorem is about every pair and every proof, and the range between the strongest and weakest interpolants usually contains many sentences a single refutation never produces.

They also cannot show the refutation and its labels together. The resolution figure draws a refutation’s shape on a smaller set of clauses; the interpolation figures report the refutation’s length and its final label. The labels on the intermediate clauses — the actual content of McMillan’s rules — exist in the computation and are not drawn.

Still open: what the shared vocabulary is when there are quantifiers #

In propositional logic the shared vocabulary is a set of atoms and the strongest interpolant can be computed by trying every value of the private ones. With quantifiers neither is so simple, and the question of what an interpolant must be allowed to say becomes the real content of the theorem.

Craig proved his theorem for first-order logic, where the shared vocabulary is the relation symbols both formulas use, and the interpolant may contain quantifiers over the domain even when neither formula quantifies over anything in particular. Constants and function symbols need care, since a formula can mention an individual that the other formula names in a different way, and equality has to be counted as shared. The search for a refutation to read one off can also fail to finish, since first-order validity has no decision procedure. And there is no longer a strongest interpolant to compute by enumeration: projecting a private relation symbol away cannot be done by trying its values, and in general the result is not expressible in first-order logic at all. The theorem survives the move to quantifiers; the strongest and weakest interpolants of this page do not, and what replaces them is a question about which logics are expressive enough to state their own projections.

A proof that says what was used #

The habit is about reading a proof for more than its conclusion.

A refutation of $A$ together with $\lnot B$ was produced to establish one bit: that $A$ implies $B$. It turns out to contain much more — a sentence stating precisely what part of $A$ was needed, in words $B$ understands. A proof is a record of what was used, and a proof with no lemma in it is a record that cannot have used anything outside the problem’s own vocabulary.

That is worth asking of any argument, formal or not. When a conclusion follows from a premise, what is the smallest statement about the things they share that carries the inference? Often it is shorter than either, and it is the part of the argument that would survive a change to everything else.