Chapter 6: Model Theory

Suppose you look after the platform at a company of five people, and you want, more than anything, never to be surprised by your own system. On Tuesday the finance director asks you to confirm something everyone takes for granted: that everybody earns less than their boss. The personnel table, Figure 6.1, is short enough to print.

You don’t check the claim row by row. Like anyone who has written SQL, you ask the database for the rows that break it:

SELECT e.name, b.name AS boss
FROM   staff e JOIN staff b ON e.boss = b.name
WHERE  NOT (b.salary > e.salary);

One row comes back: Thorne | Thorne. The chief executive is her own boss, and she doesn’t earn more than herself. You add AND e.name <>
'Thorne' to the query, it returns nothing, and you reply that the claim holds.

The finance director answers with one line: “Can that ever stop being true?” This is a different question. The table changes continually as people are hired, promoted, or given rises. He does not want to know whether the claim is true now, but whether it is true of every table the personnel system can produce given the HR policy.

The story contains two ideas, and we should keep them apart from the start. One is that of a sentence being true here, of this table on this Tuesday. The other is that of a sentence being true everywhere the constraints allow, of every table that obeys them. The first is a matter of looking, and the query engine settles it in a fraction of a second. The second is a claim about infinitely many tables, most of which nobody will see, and no amount of looking settles it.

This chapter is about the two ideas and the connection between them. It asks three questions:

• What does it mean for a sentence to be true of a system?

• What does it mean for a sentence to follow from the requirements on a system, so that it is true of every system that meets them?

• Is there a finite way to show that it does?

The first two questions are answered by definitions, and the third by a theorem, though the first rules of proof we try turn out to fall short. Section 6.1 makes a system into a mathematical object, a structure. Section 6.2 gives a language for talking about structures, and Section 6.3 defines when a sentence of that language is true in a structure. Section 6.4 defines what it is for a sentence to follow from others: to be true in every structure in which they are true. Section 6.5 tries the proofs we already have, Gentzen’s natural deduction system $\mathrm{NJ}$: they never lead from true premisses to a false conclusion, but they miss some sentences that follow, all for want of a single law. Adding that law, the law of the excluded middle, gives the system $\mathrm{NK}$ (Section 6.6), and Section 6.7 proves it complete: a sentence follows from others exactly when it has a derivation from them in $\mathrm{NK}$. Section 6.8 counts what the extra law costs.

6.1 Structures

Before the word true can mean anything, we must say what a sentence is true of. Engineers use the word system for almost anything with parts, and we begin from what the word covers rather than from a definition. Figure 6.2 lists five systems.

The five have nothing in common as subject matter, yet each comes in the same three pieces:

• a collection of things;

• some relations among the things, each true of some tuples of things and false of others;

• some functions, each taking things and returning a thing.

Some systems also have a few things with names of their own: a company has the chief executive, the numbers have the starting number $0$, and a program has the initial state.

The arity says how many inputs each function or relation symbol takes. Given only the symbol $f$, nobody could tell whether it names a function of one variable, of two, or of a million.

A relation with $n$ places is a table with $n$ columns and one row for each tuple of which it holds, so a structure is a database: one table for each relation symbol, one lookup table for each function symbol, and a few named rows.¹

Example 6.3 (the company). Harriet Ashworth looks after the platform at the company of the opening, and the personnel table of Figure 6.1 is hers. Its vocabulary is the company signature

$${\mathrm{\Sigma }}_{\mathrm{C}}=(\{\mathsf{ceo}\},\{\mathsf{boss}\},\{=,\mathsf{Eng},\mathsf{Mgr},\mathsf{Richer}\},\mathrm{ar})$$

with $\mathrm{ar}(\mathsf{boss})=\mathrm{ar}(\mathsf{Eng})=\mathrm{ar}(\mathsf{Mgr})=1$ and $\mathrm{ar}(=)=\mathrm{ar}(\mathsf{Richer})=2$. The formula $\mathsf{Richer}(x,y)$ is read “$x$ earns more than $y$”. The symbol $=$ is a two-place relation symbol like the others, written between its arguments as usual.

Tuesday’s table is the ${\mathrm{\Sigma }}_{\mathrm{C}}$-structure $\mathfrak{C}=({\mathbb{D}}_{\mathrm{C}},I_{\mathrm{C}})$ given by

$$\begin{array}{rl}{\mathbb{D}}_{\mathrm{C}}& =\{\text{Thorne},\text{Finch},\text{Pratt},\text{Bell},\text{Cole}\},\\ \text{⟦}\mathsf{ceo}{\text{⟧}}^{\mathfrak{C}}& =\text{Thorne},\\ \text{⟦}\mathsf{boss}{\text{⟧}}^{\mathfrak{C}}& =\{\text{Thorne}\mapsto \text{Thorne},\text{Finch}\mapsto \text{Thorne},\text{Pratt}\mapsto \text{Thorne},\\ & \phantom{=\{}\text{Bell}\mapsto \text{Finch},\text{Cole}\mapsto \text{Finch}\},\\ \text{⟦}\mathsf{Eng}{\text{⟧}}^{\mathfrak{C}}& =\{\text{Bell},\text{Cole}\},\\ \text{⟦}\mathsf{Mgr}{\text{⟧}}^{\mathfrak{C}}& =\{\text{Thorne},\text{Finch}\},\\ \text{⟦}={\text{⟧}}^{\mathfrak{C}}& =\{(d,d):d\in {\mathbb{D}}_{\mathrm{C}}\},\\ \text{⟦}\mathsf{Richer}{\text{⟧}}^{\mathfrak{C}}& =\{(d,e)\in {\mathbb{D}}_{\mathrm{C}}^2:\mathit{sal}(d)>\mathit{sal}(e)\},\end{array}$$

where $\mathit{sal}:{\mathbb{D}}_{\mathrm{C}}\to \mathbb{N}$ is the salary column of Figure 6.1.

The structure interprets $=$ as identity, the relation of each person to herself. Nothing in the definition of a structure demands that, since $=$ may be interpreted as any set of pairs, but every structure for the company signature that we describe interprets it as identity.

The salaries are all different, so exactly half of the twenty ordered pairs of different people are in $\text{⟦}\mathsf{Richer}{\text{⟧}}^{\mathfrak{C}}$: ten pairs, from (Thorne, Finch) down to (Bell, Cole). The function $\mathit{sal}$ is not part of the structure. The signature has no symbol for a salary, so the structure keeps only what the symbols can ask about: who earns more than whom.

Figure 6.3 draws the structure, with an arrow from each person to their boss; M marks a manager and E an engineer. Thorne’s loop is the row that Harriet’s first query returned.

A structure with a finite domain can be listed, table by table, as a personnel table can. A structure with an infinite domain can be described but not printed, and how to describe one exactly is a delicate matter.² The counting numbers of Figure 6.2 are of that kind.

6.2 Syntax

A structure can be asked questions, and this section builds the language to ask them in. We start from a signature $\mathrm{\Sigma }=(\mathcal{C},\mathcal{F},\mathcal{R},\mathrm{ar})$ and a countably infinite set $\mathrm{Var}$ of variables, $x$, $y$, $z$, $x_1$, $x_2$ and so on, disjoint from the symbols of $\mathrm{\Sigma }$. Constants and variables name elements of the domain, and function symbols build new names from old ones.

Having named things, we want to say something about them. A relation applied to terms is the smallest such statement, and it is called an atomic formula: $\mathsf{Richer}(\mathsf{boss}(x),x)$ says that the boss of $x$ earns more than $x$, and $\mathrm{\perp }$ says something false outright. Atomic formulas are combined into complex ones by the logical symbols. We use Greek letters $\phi$, $\psi$ and $\chi$ for formulas, and Latin letters $p$ and $q$ for propositional letters.

Familiar two-place symbols are written between their arguments, as usual: $x+y<z$ is the atomic formula $<(+(x,y),z)$, and $t_1=t_2$ is $=(t_1,t_2)$. Brackets are kept down by the usual conventions:

• The outermost pair is dropped.

• $\wedge$ and $\vee$ take precedence over $\to$, which groups to the right.

• $\mathrm{\neg }$ and the quantifiers $\mathrm{\forall }$ and $\mathrm{\exists }$ take precedence over everything else.

A symbol that takes precedence applies first, to as little of the formula as it can, just as $\times$ applies before $+$ in $2+3\times 4$.

A formula with variables does not yet say anything definite. $\mathsf{Richer}(\mathsf{boss}(x),x)$ is true or false according to who $x$ is, whereas $\mathrm{\forall }x\mathsf{Richer}(\mathsf{boss}(x),x)$ makes one claim about the whole domain: everyone earns less than their boss. The next definition separates the variables whose values must be supplied from those that a quantifier has already taken charge of.

Using the language is mostly translation, in both directions, and one choice causes most mistakes: which connective joins a quantifier to the condition that restricts it. “Every $P$ …” restricts a universal quantifier, and the restriction goes in with $\to$: for every $x$, if $x$ is a $P$, then …. “Some $P$ …” restricts an existential quantifier, and the restriction goes in with $\wedge$: some $x$ is a $P$ and …. The rule of thumb, universal with $\to$ and existential with $\wedge$, is reliable but not infallible.

Proofs pass from a claim about anybody to the same claim about somebody in particular, as ($\mathrm{\forall }$E) does, and the other way round, as ($\mathrm{\exists }$I) does. The syntactic tool is substitution: put a term in place of $x$, so that $\mathsf{Richer}(\mathsf{boss}(x),x)$ becomes $\mathsf{Richer}(\mathsf{boss}(\mathsf{ceo}),\mathsf{ceo})$, which says it of the chief executive. Substitution is an operation on strings, and truth is not defined through it (Remark 6.24 says why). It comes with a danger. The term put in may have variables of its own, and a quantifier in the formula can capture them, so that the result says something quite different. The definition of substitution is therefore followed by a second, of the condition that rules capture out.

We write $\phi [t/x]$ only when $t$ is substitutable for $x$ in $\phi$. A closed term always is, having no variables to capture.

The sentences of Figure 6.4 look as if they speak about a particular firm, and we have read them so. But nothing in this section says how a string of symbols speaks about anything, and so nothing here decides whether $\mathrm{\forall }x\mathsf{Richer}(\mathsf{boss}(x),x)$ is true. Nothing could, since the string mentions no structure: every structure for its signature reads it. The reading we have been doing by intuition needs a definition, and the next section gives it.

6.3 Satisfaction

A structure says what the symbols of a formula mean. It does not say what the variables stand for, and a formula with free variables is true or false only once something does.

Together, a structure and an assignment settle what every term names and whether every formula is true.

We already know what the logical words mean in English, and the definition writes that meaning down, one kind of formula at a time: a conjunction is true when both conjuncts are, a disjunction when at least one disjunct is, and “for every $x$” when what follows holds whichever element $x$ stands for. The structure enters only at the atomic formulas: $R(t_1,\dots ,t_n)$ is true when the things the terms name stand in the relation that $R$ names.

The clause for $\mathrm{\perp }$ says that it is true nowhere. Since $\mathrm{\neg }\phi$ is $\phi \to \mathrm{\perp }$, the clause for $\to$ yields one for negation: $\mathfrak{M},s\models \mathrm{\neg }\phi$ if and only if $\mathfrak{M},s⊭\phi$.

The clause for $\to$ is a deliberate choice. It ignores any connection of content between the two halves, so that “if $2+2=5$ then $1+1=3$” is true, because its antecedent is false. Other readings of “if”, which ask for such a connection, have been studied, and none would make the truth of $\phi \to \psi$ depend only on the truth of $\phi$ and of $\psi$. This one does, and that is what lets the definition decide an implication by deciding its two halves.

The quantifier clauses are where the assignment earns its keep. To decide whether $\mathrm{\forall }x\psi$ is true, we must look at $\psi$ with $x$ standing for each element of the domain in turn, while every other variable keeps the value it had. The assignment $s[d/x]$ is exactly that: $s$ with $x$ pointed at $d$ and nothing else changed. Whatever $s$ gave $x$ before does not matter, since the quantifier has taken charge of $x$.⁴ The job falls to the assignment because a structure fixes once and for all what each constant symbol names, while a variable can stand for one element now and for another a moment later.

On a finite structure the definition is also an algorithm: to decide whether a sentence is true, unfold it clause by clause. Each quantifier clause runs through the domain, so a sentence with $k$ nested quantifiers, on a domain of $n$ elements, needs about $n^k$ cases. On an infinite domain, such as the counting numbers, the quantifier clauses ask about infinitely many elements. The definition still makes sense, since it says what truth is, but it no longer tells us how to find it out.

The same sentence can be true in one structure and false in another: truth belongs to the pair of a sentence and a structure, not to the sentence alone.

The same clauses cover the simplest formulas of all, those built from propositional letters, and there they reduce to something familiar.

So for formulas built from letters a structure amounts to a choice of true or false for each letter, a valuation: a row of a truth table. With two letters there are four rows, and the clauses for the connectives compute the familiar tables. For $p\to q$, writing T and F for true and false:

Propositional logic is the part of first-order logic in which every relation symbol has no places.

The definition asks for an assignment even when the formula is a sentence, yet a sentence has no free variables, and its truth ought not to depend on what they stand for. If it did, “true in this structure” would mean nothing until somebody chose an assignment, and a question such as whether everybody earns less than their boss would have no answer. The next lemma removes the worry.

In words: a formula cares only about the variables it leaves free.

In particular, the truth of a sentence in $\mathfrak{M}$ does not depend on the assignment. We write $\mathfrak{M}\models \phi$, read “$\phi$ is true in the structure $\mathfrak{M}$”, when $\mathfrak{M},s\models \phi$ for one assignment $s$, and hence for all.

Substitution was introduced to pass from a claim about anybody to the same claim about somebody in particular. The passage is safe only if $\phi [t/x]$ says about the thing $t$ names exactly what $\phi$ says about $x$, and the next lemma shows that it does, provided nothing is captured.

In words: putting the term $t$ in for $x$ has the same effect as letting $x$ stand for whatever $t$ names. Without the proviso the lemma fails: when a quantifier captures a variable of $t$, the formula $\phi [t/x]$ no longer says of the thing $t$ names what $\phi$ says of $x$ (Example 6.19 shows a case).

The proof, by induction on $\phi$, is long and unilluminating, and we omit it, as most textbooks do; but the omission is of length, not of difficulty. The case of terms, on which the rest is built, is Exercise 6.15, which also asks where substitutability is used.

One feature of the definition looks too obvious to mention, yet its consequences are subtle and contentious. The clause for negation makes $\mathrm{\neg }\phi$ true in $\mathfrak{M}$ under $s$ exactly when $\phi$ is not, so exactly one of $\phi$ and $\mathrm{\neg }\phi$ is true, and by the clause for disjunction $\phi \vee \mathrm{\neg }\phi$ is true in every structure under every assignment, whatever $\phi$ says. This property of the definition, that every formula has exactly one of two truth values in a structure under an assignment, is called bivalence.

6.4 Entailment

Satisfaction answers a question about one structure and one assignment: is this formula true here? Often we want something else. We have no particular system in mind, only requirements that every acceptable system must meet, and we want to know what holds in every system that meets them: whether everybody earns less than their boss in every table a personnel system could ever accept, say.

A set of sentences that says what any acceptable system must satisfy, written down before any particular system is in view, is called a theory.

Entailment is defined for sets of formulas, whose members may have free variables and are then true or false only under an assignment. For such a set $\mathrm{\Gamma }$ we write $\mathfrak{M},s\models \mathrm{\Gamma }$ when $\mathfrak{M},s\models \psi$ for every $\psi \in \mathrm{\Gamma }$, and say that $\mathfrak{M},s$ satisfies $\mathrm{\Gamma }$. When $\mathrm{\Gamma }$ is a theory the assignment makes no difference, by the relevance lemma, and $\mathfrak{M},s\models \mathrm{\Gamma }$ says just that $\mathfrak{M}$ is a model of $\mathrm{\Gamma }$.

When $\mathrm{\Theta }$ is a theory and $\phi$ a sentence, $\mathrm{\Theta }\models \phi$ says that $\phi$ is true in every model of $\mathrm{\Theta }$. Validity is entailment by the empty theory, of which every structure is a model, and it is rarely what we want. A claim such as “nobody but the person at the top is their own boss” is not valid, and nobody expects it to be: it holds, if it holds, because of the theory a system satisfies. The three notions differ in what they examine, as Figure 6.7 shows.

One relation symbol needs a theory of its own. A structure may interpret $=$ as any set of pairs, but a system that compares names relies on two facts about identity: everything is equal to itself, and equals may be put for equals. Written as sentences, these facts are the equality axioms.

The list does not mention symmetry or transitivity, and need not: because (Eq2) allows every formula $\phi$, both follow from (Eq1) and (Eq2) (Exercise 6.8).

A structure that interprets $=$ as identity is normal. Every normal structure satisfies ${\mathrm{Eq}}_{\mathrm{\Sigma }}$. The axiom (Eq1) holds because everything is identical to itself, and each instance of (Eq2) holds by the substitution lemma, since under an assignment that gives $x$ and $y$ the same value, $\phi$ and $\phi [y/x]$ have the same truth value.

The two kinds of answer are not on an equal footing. A non-entailment comes with a certificate, a structure, which anyone can check by evaluating sentences in it. An entailment comes with an argument, “let $\mathfrak{M}$ be a model of the theory and $d$ an element”, which is convincing but cannot be checked by running anything: it speaks of every model of the theory, of every size, including the infinite ones, and no loop runs over all of those (Examples 6.39 and 6.40 show one of each).

6.5 Soundness and Incompleteness of $\mathrm{NJ}$

How can we certify that $\mathrm{\Gamma }\models \phi$? Listing the structures that satisfy $\mathrm{\Gamma }$ and checking each one is out of the question: there are infinitely many, and most of them are infinite. What we want instead is a proof, a finite object showing that the commitments made by $\mathrm{\Gamma }$ yield $\phi$, each step of which a program can check. Part 1 supplied one, Gentzen’s $\mathrm{NJ}$. We write $\mathrm{\Gamma }{⊢}_{\mathrm{NJ}}\phi$ when some derivation in $\mathrm{NJ}$ has conclusion $\phi$ and all its open hypotheses in $\mathrm{\Gamma }$.

Two notions of consequence are now available, $\mathrm{\Gamma }\models \phi$ and $\mathrm{\Gamma }{⊢}_{\mathrm{NJ}}\phi$. The first quantifies over all structures and assignments, the second asks for one finite object, and they can be related in two ways:

• Soundness: if $\mathrm{\Gamma }{⊢}_{\mathrm{NJ}}\phi$, then $\mathrm{\Gamma }\models \phi$.

• Completeness: if $\mathrm{\Gamma }\models \phi$, then $\mathrm{\Gamma }{⊢}_{\mathrm{NJ}}\phi$.

Soundness says that derivations are safe: none leads from true hypotheses to a false conclusion. Completeness says that derivations are enough: whatever follows has one.

A derivation is the certificate we asked for: a finite object, each step of which a program can check against the rules.

Is $\mathrm{NJ}$ also complete? It is not. To show that a sentence has no derivation in $\mathrm{NJ}$ we use two properties of the rules.

In words: a proof in $\mathrm{NJ}$, from no hypotheses, of “$\phi$ or $\psi$” says which of the two holds, and a proof of “there is an $x$ such that $\phi$” names a term for $x$.

The reason fits in three sentences. Every derivation can be rewritten, step by step, into one with no detours, that is, no introduction rule followed at once by the elimination rule for the same symbol. A derivation with no detours and no open hypotheses ends with an introduction rule. For $\phi \vee \psi$ that rule is ($\vee$I), and the tree above it derives $\phi$ or derives $\psi$; for $\mathrm{\exists }x\phi$ it is ($\mathrm{\exists }$I), and the tree above it derives $\phi [t/x]$ for a particular term $t$.⁶

The proof used soundness to pass from a derivation to validity, and two structures to take validity away. It used nothing about $p$ except that a structure can make it true and another false, so the same proof works for every sentence $\phi$ of which that holds: $\mathrm{NJ}$ does not derive $\phi \vee \mathrm{\neg }\phi$.

The sentence $\phi \vee \mathrm{\neg }\phi$ is the law of the excluded middle: every structure obeys it, and $\mathrm{NJ}$ lacks it. The rules come close, since they derive $\mathrm{\neg }\mathrm{\neg }(\phi \vee \mathrm{\neg }\phi )$, but no rule leads from $\mathrm{\neg }\mathrm{\neg }\phi$ to $\phi$. The gap is no isolated freak, and the next example meets it again.

6.6 Law of the Excluded Middle

The gap in $\mathrm{NJ}$ is a principle that every structure obeys: of a claim and its denial, one is true, and there is no third option in the middle. This is the law of the excluded middle (LEM), and it is more than two thousand years old.⁸ In a structure it holds because the clause for negation makes exactly one of $\phi$ and $\mathrm{\neg }\phi$ true (bivalence); in a proof system it becomes a rule with no premisses, for every formula $\phi$:

The law is not the only principle that $\mathrm{NJ}$ lacks. Three more fall into the gap, each a schema with an instance for every choice of formulas:

• The first, double negation, says that what is not false is true;

• the second, Peirce’s law,⁹ says much the same without negation;

• the third says that if not everything lacks the property $\phi$, then something has it.

Every instance of each is valid, as a check against the clauses shows, but $\mathrm{NJ}$ does not derive every instance: already $\mathrm{\neg }\mathrm{\neg }p\to p$, $((p\to q)\to p)\to p$ and $\mathrm{\neg }\mathrm{\forall }x\mathrm{\neg }P(x)\to \mathrm{\exists }xP(x)$, for propositional letters $p$, $q$ and a relation symbol $P$, have no derivation (Exercise 6.10).

With the law added, all three become derivable. Here is double negation:

We write (DN) for this derivation used as a step. The system with the law added is classical logic.

Every derivation of $\mathrm{NJ}$ is a derivation of $\mathrm{NK}$, so $\mathrm{\Gamma }{⊢}_{\mathrm{NJ}}\phi$ implies $\mathrm{\Gamma }{⊢}_{\mathrm{NK}}\phi$. The letters are J for intuitionistisch and K for klassisch.¹⁰ One rule with no premisses looks like a small addition. The next example shows what it buys.

So far, so good: $\mathrm{NK}$ is sound, and it reaches sentences that $\mathrm{NJ}$ missed. But is one more rule enough? Soundness is half of the connection between ${⊢}_{\mathrm{NK}}$ and $\models$. The other half asks whether $\mathrm{NK}$ derives everything that follows, or whether further laws are missing.

6.7 Completeness of $\mathrm{NK}$

Soundness puts derivability inside entailment: whatever $\mathrm{NK}$ derives from $\mathrm{\Gamma }$ is true in every model of $\mathrm{\Gamma }$. For $\mathrm{NJ}$ the converse failed, and the law of the excluded middle was the missing step. For $\mathrm{NK}$ the converse holds.

In words: whatever is true in every model of a theory can be derived from it in $\mathrm{NK}$.

To show that $\mathrm{\Gamma }\models \phi$ implies $\mathrm{\Gamma }{⊢}_{\mathrm{NK}}\phi$, we prove the contrapositive: if $\mathrm{\Gamma }{⊬}_{\mathrm{NK}}\phi$, then some model of $\mathrm{\Gamma }$ makes $\phi$ false. We are handed a failure to derive and must build a structure from it. Two definitions name what the construction aims at.

Keep the two words apart. Consistent is about derivations: no derivation leads from the set to $\mathrm{\perp }$. Having a model is about structures: some structure makes the whole set true.

Soundness gives one direction at once, since a set with a model cannot derive $\mathrm{\perp }$, which is true in no structure. The proof below gives the other, and in this vocabulary that is the whole of the completeness theorem: every consistent set of sentences has a model. (Applied to $\mathrm{\Gamma }\cup \{\mathrm{\neg }\phi \}$, this gives the theorem as stated, by Step 1 below.) The proof has five steps.

1. Show that $\mathrm{\Gamma }\cup \{\mathrm{\neg }\phi \}$ is consistent.

2. Add new constants, and sentences that make each of them a witness for an existential sentence.

3. Extend the result to a maximal consistent set $\mathrm{\Delta }$.

4. Build a structure from the closed terms of the language, so that its elements are pieces of syntax.

5. Prove that a sentence is true in this structure exactly when it belongs to $\mathrm{\Delta }$. Since $\mathrm{\Gamma }$ and $\mathrm{\neg }\phi$ are in $\mathrm{\Delta }$, the structure is the one we want.

Steps 2 and 4 are needed only for the quantifiers, so we first carry out the propositional case in full and then extend it.

Step 1

Excluded middle enters the propositional proof here and nowhere else, through (DN), and here the proof breaks down for $\mathrm{NJ}$. With $\mathrm{\Gamma }$ empty and $\phi$ the sentence $p\vee \mathrm{\neg }p$, the lemma fails for $\mathrm{NJ}$: the system does not derive $p\vee \mathrm{\neg }p$, yet $\{\mathrm{\neg }(p\vee \mathrm{\neg }p)\}$ is inconsistent, by the tree that derived $\mathrm{\neg }\mathrm{\neg }(p\vee \mathrm{\neg }p)$.

Steps 3 to 5, propositional case

In words: a set of sentences that does not contradict itself can be enlarged until it takes a side on every question, and still not contradict itself.

The proof is not an algorithm. At each step it asks whether a set of sentences is consistent, and nothing in it says how that question is to be answered; it needs only that the question has an answer. The proof shows that $\mathrm{\Delta }$ exists without constructing it. Nor is $\mathrm{\Delta }$ unique: another order of the list can give another maximal consistent set. The lemma promises a maximal consistent set, not a particular one, and the completeness proof needs only one.

The next lemma shows, one connective at a time, that a maximal consistent set behaves like the set of truths of a single structure.

For a signature of propositional letters a structure amounts to a valuation, and the obvious one serves: make a letter true exactly when it belongs to $\mathrm{\Delta }$.