Worlds built out of sentences

Every model so far has been handed over ready-made: here are four worlds, here are the arrows, now evaluate. That is fine for checking a formula and useless for the question completeness asks, which is whether a formula with no proof has a countermodel — one nobody has drawn.

The construction that answers it makes the worlds out of the syntax. A world is a consistent set of commitments — for each formula in a fixed finite list, whether it holds — and the arrows are read off those commitments. Nothing is assumed about what a world is.

The closure #

Fix a finite set of formulas closed under subformulas: if $\Box p$ is in it then so is $p$. The hero uses the smallest interesting one, $\{p, \Box p\}$.

A candidate world is a choice, for each formula in the set, of whether to accept it — so with two formulas there are four candidates: accept both, accept $p$ only, accept $\Box p$ only, accept neither.

That is the entire supply of worlds. There is no domain of individuals, no possible-worlds metaphysics, and no appeal to anything outside the syntax: a world is a row of a truth table over the closure, and there are $2^n$ of them for a closure of size $n$.

The arrow #

The relation is defined by one clause. World $w$ sees world $v$ when, for every $\Box\varphi$ in the closure that $w$ accepts, $v$ accepts $\varphi$.

The clause is exactly what makes the truth lemma have a chance. If $\Box\varphi$ is one of $w$’s commitments, then every world $w$ sees must satisfy $\varphi$ — which is what $\Box\varphi$ being true at $w$ requires — and the definition arranges it by fiat.

The other direction is where the content is. If $w$ does not accept $\Box\varphi$, the definition places no obligation, and the truth lemma needs $\Box\varphi$ to come out false at $w$ — which means $w$ must see some world rejecting $\varphi$. That such a world exists among the candidates, and is seen, is what has to be checked.

The definition is one-sided and the lemma is two-sided, and everything interesting is in the gap.

The truth lemma, checked #

The claim: in the model built above, a formula of the closure is true at a world exactly when that world accepted it.

The generator checks it directly. It builds the arrows, computes the truth set of each closure formula in the resulting model, and compares against the labels — at all eight world-and-formula pairs of the hero, and at more when the closure is larger. Where the two disagree, the world is inconsistent and is deleted; deleting worlds changes the arrows, so the check runs again, and what is drawn is the fixed point.

For the closure $\{p, \Box p\}$ nothing is deleted, and the four worlds are worth walking through.

$w$ accepting $p$ and $\Box p$: it sees exactly the worlds accepting $p$, and both of those accept $p$, so $\Box p$ is true. Correct.

$w$ accepting $p$ and rejecting $\Box p$: it accepts no boxed formula, so it sees everything, including a world rejecting $p$ — so $\Box p$ is false. Correct.

The other two run the same way, and the second case is where the one-sided definition pays off: a world with no boxed commitments sees every world, which is exactly what makes its boxes come out false.

Reading the eight-world version #

The larger closure is worth walking through, because it is where the arrow clause’s one-sidedness stops being a technicality.

With $\{p, \Box p, \Box\Box p\}$ there are eight worlds, each labelled by three commitments. Take $w_7$, accepting all three. Its boxed commitments are $\Box p$ and $\Box\Box p$, so it sees the worlds accepting $p$ and accepting $\Box p$ — which are $w_3$ and $w_7$. Both accept $p$, so $\Box p$ is true; both accept $\Box p$, so $\Box\Box p$ is true. The label agrees on both.

Now $w_3$, accepting $p$ and $\Box p$ and rejecting $\Box\Box p$. Its only boxed commitment is $\Box p$, so the clause requires its successors to accept $p$ and says nothing about $\Box p$. So $w_3$ sees every world accepting $p$ — four of them — and two of those reject $\Box p$. Hence $\Box\Box p$ is false at $w_3$, exactly as its label says.

The world that rejects a box is the one with more successors, and that is the whole mechanism. Accepting $\Box\Box p$ narrows what a world can see; rejecting it widens the field until something rejecting $\Box p$ is in view, which is what makes the rejection true.

Every one of the eight works out, so nothing is pruned here either — which is what should happen, since the logic in question is $K$ and $K$ imposes no relation at all between $p$, $\Box p$ and $\Box\Box p$. The pruning loop is there for the logics that do.

Why this is completeness #

The lemma is a statement about one model, and completeness is a statement about a proof system. The bridge is one sentence.

Suppose $\varphi$ has no proof. Then the set $\{\neg\varphi\}$ is consistent, so it extends to a world in the model over a closure containing $\varphi$. By the truth lemma, $\varphi$ is false at that world.

So a formula with no proof is false somewhere — which is the contrapositive of completeness: valid everywhere implies provable.

The model is not found, it is manufactured, and it is manufactured out of the very syntax whose proof system is in question. That is the manoeuvre, and it is the same one Henkin used for first-order logic, where the individuals of the model are the terms of the language.

Consistency, and what the pruning does #

The construction as described admits every row of the truth table, and not every row is consistent. Where the truth lemma fails at a world, that world was asserting something the semantics forbids, and dropping it is the right response.

For both closures drawn here nothing is dropped, which is not an accident: over $K$ every combination of these commitments is satisfiable, because $K$ imposes no relation between a formula and its box.

Add axioms and the picture changes. In the logic $T$, where $\Box p \to p$ is provable, the world accepting $\Box p$ and rejecting $p$ is inconsistent and gets deleted. In $S5$ many more go. The axioms of a logic show up as worlds that cannot exist, which is a pleasingly concrete reading of what an axiom does.

The general construction handles this by defining a world to be a maximal consistent subset of the closure, where consistency is with respect to the logic being proved complete. The pruning loop here computes the same thing semantically, which is legitimate for $K$ because $K$ is sound and complete for all frames — the argument is circular if run in general and correct if run for the base logic.

Why the closure has to be finite here #

The classical canonical model is infinite: its worlds are maximal consistent sets of all formulas, of which there are as many as there are sets of formulas.

That version proves completeness for the whole language in one construction and cannot be drawn. The finite version above, over a closure, proves something weaker and more useful: every satisfiable formula is satisfiable in a model with at most $2^n$ worlds, where $n$ counts its subformulas.

That is the finite model property, and it is what makes modal validity decidable: to test a formula, enumerate the models of bounded size and check. The bound is exponential and the enumeration is finite, and that is the whole decision procedure.

The technique of collapsing an infinite model to a finite one over a closure is called filtration, and the construction here is its by-hand version. A search that terminates is what a tableau gives for the same question, and the finite model property is what guarantees the search can stop.

Soundness is the easy half, and the other half of the pair #

Completeness has a companion that is usually mentioned in one line and is worth more, because the two together are what make a proof system worth having.

Soundness says every provable formula is valid: if there is a proof, there is no countermodel. It is proved by induction on the proof — check each axiom is valid and each rule preserves validity — and it is short.

Completeness says the converse, and it is the construction above. Together they say provable and valid are the same set of formulas, so a syntactic question and a semantic one have the same answer.

The value of the pair is that the two questions have different costs. Showing a formula valid means checking every model, of which there are infinitely many; showing it provable means exhibiting one proof. Showing a formula invalid means exhibiting one model; showing it unprovable means an argument about every proof. So each direction converts an open-ended search into a finite exhibit, in the direction the other cannot.

A tableau that closes is the search organised so that failure produces a countermodel directly, which is a constructive completeness proof rather than a manufactured one — and for the propositional and modal cases it is the version that gets implemented.

What the worlds are not #

It is worth clearing away a reading the construction invites, because the vocabulary encourages it.

The worlds here are sets of formulas. They are not possible situations, not states of affairs, not anything with content beyond the list of sentences accepted. A world accepting $p$ and rejecting $\Box p$ is a bookkeeping object, and asking what it is like is a category error.

That austerity is the point. Completeness is proved by exhibiting a model, and the cheapest model to exhibit is one whose worlds are made of the material already lying about — the syntax. Anything richer would need justifying.

A model is a mathematical structure satisfying a definition, and the definition asks for a set, a relation on it, and a valuation. Sets of formulas supply all three, and the interpretive weight the word world carries is borrowed from elsewhere.

Reading an axiom as a deleted world rather than as a drawn arrow is worth keeping, because it explains why a stronger logic has a smaller canonical model. Each axiom rules out some commitments as inconsistent, the count of surviving worlds falls, and the model that comes out is more constrained — which is the same trade as a stronger hypothesis giving a sharper theorem, seen from the model’s side.

The same manoeuvre elsewhere #

Building a model out of syntax is a standard move and it is worth seeing the family, because the modal case is the smallest member.

For first-order logic, Henkin’s proof builds a model whose individuals are the closed terms of an extended language, with equality read as provable equality. The truth lemma is the same statement: a sentence is true in the term model exactly when it is provable.

For propositional logic the construction is so small it is usually not noticed: a consistent set of literals is a valuation, and the completeness of the truth-table method is that observation.

For intuitionistic logic the worlds are stages of knowledge and the construction produces exactly the Kripke models the same frames carry. One picture, two logics, and the canonical construction runs the same way in both.

In every case the model’s carrier is made of expressions, and the truth lemma says the manufactured semantics agrees with the syntax it was manufactured from. That agreement is what completeness means, and it is not a coincidence that it is provable — the model was built to make it true.

Where the construction stops working #

The canonical model is not universal and its failures are instructive, because they mark the boundary of the method rather than of the subject.

For most standard modal logics it works: $K$, $T$, $S4$, $S5$, and every logic axiomatised by Sahlqvist formulas has a canonical model whose frame satisfies the corresponding condition. That last clause is the theorem the next rung is about, and it is what makes the method routine.

It fails for logics whose frame conditions are not preserved by the construction. The Gödel–Löb logic of the last rung is the standard example: its frames must have no infinite ascending chains, and the canonical model has plenty, so the model built from the syntax is not a frame of the logic. Completeness for it is true and needs a different proof — a finite one, by filtration, which is where the finite version above earns its keep.

And there are logics with no complete semantics of this kind at all. Incomplete modal logics exist: sets of formulas closed under the rules that are consistent, and valid on no class of frames whatever. The first was found by Thomason in 1974, and their existence is why complete is a property a logic may or may not have rather than something that comes free.

What the construction does not decide #

A limitation worth naming, since the construction looks as though it settles everything about a logic and settles one thing.

It produces a model for every consistent set, which is completeness. It says nothing about whether the frame of that model has any particular property — and for logics whose intended frames are constrained, that is the whole remaining question.

The gap shows up whenever the intended class of frames is not the class the axioms happen to define. A logic can be complete for the frames its axioms define and not for the smaller class its author had in mind, and telling the two apart takes a separate argument each time.

Completeness is a relation between a proof system and a class of models, and changing the class changes the claim. The construction fixes the proof system and manufactures models; which class those models land in is decided by the axioms and not by the method.

What the pictures cannot show #

Consistency is checked and not drawn. The pruning loop deletes worlds where the lemma fails, and for the small closures drawn it deletes none. A picture of a construction that removes nothing looks like a construction with no pruning in it.

The infinite canonical model has no drawing at all. The version proved here is the finite one, and the classical statement is about a model with uncountably many worlds.

And the arrows are dense. Eight worlds with the arrows the definition produces is a nearly complete graph, which is honest and hard to read. The larger closure’s figure is at the edge of what a diagram of this kind can carry.

Where the ladder goes next #

The first rung matched axioms to frame properties one at a time and by hand. The next asks whether that matching can be automated — whether there is a recipe taking an axiom to its condition — and finds that there is, for a large class, and that the class is not everything. One axiom answers to no property of the arrows at all, and showing so is a different kind of argument from anything on this ladder so far.

Sideways: the tableau is the proof system this construction proves complete for, in its propositional version, and what the language cannot distinguish is what limits how much a manufactured model has to get right.

What is worth carrying away #

When a proof needs an object nobody has, the material to build it from is often the problem’s own statement.

Completeness asks for a model of every consistent set, and there is no supply of models to draw on. The construction makes them out of sets of formulas — the one thing definitely available — and then has to check that the manufactured object behaves. That check is the truth lemma and it is the whole of the work.

The pattern is worth recognising because it recurs whenever an existence claim has no obvious witness. Build the witness out of the syntax, then prove it works; and the proof that it works is usually an induction over exactly the formulas that went into building it.

The second thing worth carrying is what the finite version buys over the classical one. The infinite canonical model proves completeness and nothing else; the finite one proves completeness, the finite model property, and decidability, in the same construction, because a bound on the model’s size is a bound on the search that tests a formula. Doing a construction over a finite closure rather than over the whole language costs a paragraph and produces three theorems instead of one.