1Propositional Logic

We are going to introduce formal languages in which one can regiment mathematical and philosophical reasoning, without the distracting complexities and vagaries of natural language. In this chapter, we begin with the language of propositional logic: the logic of the connectives \(\neg \), \(\to \), \(\land \), \(\lor \), etc. This language is woefully inadequate for any serious applications, but it is a useful prototype to introduce general ideas and techniques that we’ll also use for more powerful languages.

1.1Syntax

When talking about language, we must distinguish the language that is being talked about, the object language, from the meta-language in which the talking takes place. Throughout these notes, the meta-language will be English, with added technical vocabulary that will be introduced as we go along. Our first object language is the language of propositional logic, or \(\mathfrak {L}_{0}\).

The primitive symbols of \(\mathfrak {L}_{0}\) are:

• a non-empty (and countable) set of sentence letters,

• the connectives ‘\(\neg \)’ and ‘\(\to \)’, and

• the parentheses, ‘(’ and ‘)’.

The sentence letters are classified as non-logical symbols; the other expressions are logical. The point of this classification will become clear in section 1.3.

In definition 1.1, I use ‘\(A\)’ and ‘\(B\)’ as metalinguistic variables for strings of symbols in the object language. Throughout these notes, I will often use capital letters from the beginning of the alphabet for sentences in the object language. I’ll sometimes use the lowercase letters ‘\(p\)’ and ‘\(q\)’ to denote arbitrary sentence letters. I haven’t said what the sentence letters of \(\mathfrak {L}_{0}\) look like. It doesn’t matter (as long as none of them has any other primitive \(\mathfrak {L}_{0}\)-symbol as a part, which I hereby stipulate). Strictly speaking, \(\mathfrak {L}_{0}\) is therefore not a single language, but a family of languages, with different stocks of sentence letters.

Unless stated otherwise, metalinguistic variables are to be understood as universally quantified. Condition (ii) in definition 1.1, for example, doesn’t talk about a particular string \(A\), which I failed to specify. Rather, it says that for all strings \(A\), if \(A\) is a sentence then \(\neg A\) is a sentence. By ‘\(\neg A\)’, I mean the string obtained by putting ‘\(\neg \)’ in front of whatever string ‘\(A\)’ picks out. Similarly for ‘\((A \to B)\)’ and other such cases.

We introduce ‘\(\land \)’, ‘\(\lor \)’, and ‘\(\leftrightarrow \)’ as metalinguistic abbreviations. That is, if \(A\) and \(B\) are \(\mathfrak {L}_{0}\)-sentences, we write

• \((A \land B)\) for \(\neg (A \to \neg B)\);

• \((A \lor B)\) for \((\neg A \to B)\);

• \((A \leftrightarrow B)\) for \(\neg ((A \to B) \to \neg (B \to A))\).

We could have added ‘\(\land \)’, ‘\(\lor \)’, and ‘\(\leftrightarrow \)’ as primitive symbols; you’ll soon understand why we didn’t. At any rate, you should remember that nothing is lost by restricting the primitive connectives to ‘\(\neg \)’ and ‘\(\to \)’: in classical propositional logic, all connectives can be defined in terms of these two.

It is convenient to also have a zero-ary connective \(\top \) that is always true, and a dual \(\bot \) that is always false. We introduce these as further metalinguistic abbreviations. Where \(p\) is an arbitrary sentence letter (say, the first in some alphabetical order), we write

• \(\top \) for \(p \to p\);

• \(\bot \) for \(\neg (p \to p)\).

Where no ambiguity threatens, I’ll often omit parentheses and quotation marks. For example, I might write \(A \to B\) instead of ‘\((A \to B)\)’.

Suppose we want to show that every \(\mathfrak {L}_{0}\)-sentence has some property. The standard method for doing this is called proof by induction on complexity.

Proofs by induction on complexity are based on the fact that every \(\mathfrak {L}_{0}\)-sentence is built up from sentence letters by finitely many applications of the formation rules in definition 1.1. The complexity of a sentence is the number of applications of these rules. A sentence letter has complexity 0; \(\neg p\) has complexity 1; \((p \to \neg q)\) has complexity 2; and so on. To show that every \(\mathfrak {L}_{0}\)-sentence has some property, it suffices to show two things:

(i)

Every sentence of complexity 0 has the property.

(ii)

If every sentence of complexity below \(n\) has the property then so does every sentence of complexity \(n\).

Step (i) is called the base case of the proof; step (ii) the inductive step. The antecedent of (ii), that every sentence of complexity below \(n\) has the property, is called the induction hypothesis.

As an example, let’s prove that every \(\mathfrak {L}_{0}\)-sentence has an even number of parentheses.

We’ll use this method again and again, not just when we talk about sentences of \(\mathfrak {L}_{0}\). Whenever a set of objects is generated from some base objects by finitely many applications of some operations, we can use the method to show that all of the objects have some property.

By the way: Now you can see why it is useful to have only two primitive connectives. If we had ‘\(\land \)’, ‘\(\lor \)’, and ‘\(\leftrightarrow \)’ as well, we would have to check three more cases in every proof by induction on complexity.

1.2The propositional calculus

In this section, I’ll explain how one can reason in \(\mathfrak {L}_{0}\). We’ll start with the ancient idea that to prove a statement means to derive it from some axioms. On this conception, a proof system consists of some axioms and some rules for deriving new sentences from old ones.

The first complete proof system for propositional logic, of this kind, was proposed by Gottlob Frege in 1879. I’ll present a slightly simplified version, due to Jan Łukasiewicz and John von Neumann. We have three axiom schemas, meaning that every instance of these schemas is an axiom:

An instance of an axiom schema is a sentence obtained by uniformly replacing the metalinguistic variables ‘\(A\)’, ‘\(B\)’, and ‘\(C\)’ by object-language sentences. For example, ‘\(p \to ((p \to p) \to p)\)’ is an instance of A1, with ‘\(A\)’ replaced by ‘\(p\)’ and ‘\(B\)’ by ‘\((p \to p)\)’.

The only rule of inference is modus ponens, which in this context is also known as detachment:

I’ll call this proof system the propositional calculus, although it is really only one of many equivalent calculi, all of which could be given that name.

We write ‘\(\vdash _{0} A\)’ (in the meta-language) to express that there is a proof of \(A\) in the propositional calculus.

Here is a proof of \(p \to p\), showing that \(\vdash _{0} p \to p\):

\begin {flalign*} \quad 1.\quad &p \to ((p \to p) \to p) &&\text {Instance of A1} & \\[0.5em] \quad 2.\quad &(p \to ((p \to p) \to p)) \to ((p \to (p \to p)) \to (p \to p)) &&\text {Instance of A2}& \\[0.5em] \quad 3.\quad &(p \to (p \to p)) \to (p \to p) &&\text {From 1, 2 by MP}& \\[0.5em] \quad 4.\quad &p \to (p \to p) &&\text {Instance of A1}& \\[0.5em] \quad 5.\quad &p \to p &&\text {From 3, 4 by MP} & \end {flalign*}

The result can be generalized. If we replace the sentence letter \(p\) by any sentence \(A\) throughout the proof, we still get a proof that conforms to definition 2.2. So we’ve effectively shown that \(\vdash _{0} A \to A\) for any sentence \(A\).

Proof systems like our propositional calculus are called axiomatic calculi or Hilbert-style calculi. As the example illustrates, they tend to be difficult to use. They are also unnatural in that they focus on establishing logical truths. More often than not, when we turn to logic, we’re interested in consequence: we want to know whether a certain conclusion follows from some premises, where these premises aren’t logical truths. In a strict axiomatic calculus, any question about consequence must be reformulated as a question about logical truth: to test whether \(B\) is a logical consequence of \(A_1,...,A_n\), one would check whether \((A_1 \land ...\land A_n) \to B\) is a logical truth.

We can, however, also extend our calculus to handle deductions from non-logical premises.

We write ‘\(\Gamma \vdash _{0} A\)’ to express that there is a deduction of \(A\) from \(\Gamma \). For example, ‘\(\{ p,q \} \vdash _{0} p\)’ is a sentence in our metalanguage saying that \(p\) is deducible from \(p\) and \(q\). We usually omit the set braces and simply write ‘\(p,q \vdash _0 q\)’.

The following structural principles about the \(\vdash _{0}\) relation immediately follow from definition 1.3.

Here, ‘Id’ stands for ‘Identity’ and ‘Mon’ for ‘Monotonicity’. As usual, ‘\(A\)’ and ‘\(B\)’ range over arbitrary \(\mathfrak {L}_{0}\)-sentences; ‘\(\Gamma \)’ and ‘\(\Delta \)’ (‘delta’) range over arbitrary sets of \(\mathfrak {L}_{0}\)-sentences; ‘\(\Gamma , B\)’ is shorthand for ‘\(\Gamma \cup \{ B \}\)’, the union of \(\Gamma \) and \(\{ B \}\). (The union of two sets is the set that contains all and only the elements that are in either of the two sets.)

The Id principle says that for any sentence \(A\), there is a deduction of \(A\) from \(A\). Why is this true? By definition 1.3, a deduction of \(A\) from \(A\) would be a sequence of sentences ending in \(A\), each of which is either an instance of A1–A3, the sentence \(A\) itself, or follows from previous sentences by MP. The sequence consisting of the single sentence \(A\) meets these conditions. (As do many longer sequences. But one sequence is enough to show that \(A \vdash _0 A\).)

A proof (in the sense of definition 2.2) is a special case of a deduction (in the sense of definition 1.3), with an empty set of premises \(\Gamma \). The following theorem shows that every deduction can be converted into a proof.

We’ll prove this in a moment. First I want to explain how it converts deductions into proofs. Suppose there is a deduction of \(B\) from \(\Gamma \). Being finite, this deduction can use only finitely many premises from \(\Gamma \). Call them \(A_{1},\ldots ,A_{n}\). So we have \[ A_{1},\ldots ,A_{n} \vdash _{0} B. \] By the Deduction Theorem, we can infer that \[ A_{1},\ldots ,A_{n-1} \vdash _{0} A_{n} \to B. \] Applying the theorem again, we get \[ A_{1},\ldots ,A_{n-2} \vdash _{0} A_{n-1} \to (A_{n} \to B). \] Continuing in this way, we can move all the premises to the right, until we get \[ \vdash _{0} A_{1} \to (A_{2} \to (\ldots (A_{n} \to B)\ldots )). \]

To prove the Deduction Theorem, we use induction on the lines in a proof. We assume that there is a deduction \(B_{1}, B_{2}, \ldots , B_{n}\) of \(B\) from \(\Gamma \cup \{ A \}\). We then show that \(\Gamma \vdash _{0} A \to B_{k}\) for each \(k = 1, 2, \ldots , n\). Since \(B_{n} = B\), this will show that \(\Gamma \vdash _{0} A \to B\). To show that \(\Gamma \vdash _{0} A \to B_{k}\) for each \(k = 1, 2, \ldots , n\), it suffices to show that

(i)

\(\Gamma \vdash _{0} A \to B_{1}\), and

(ii)

if \(\Gamma \vdash _{0} A \to B_{i}\) for all \(0 < i < k\), then \(\Gamma \vdash _{0} A \to B_{k}\).

In fact, (ii) alone is sufficient. To see this, consider the case \(k = 1\). Since there is no \(i\) with \(0 < i < 1\), the if -part of (ii) is vacuously true. If we can show (ii), we can therefore also show that \(\Gamma \vdash _{0} A \to B_{1}\).

The proof of the Deduction Theorem requires axioms A1 and A2. If we’re interested in what can and can’t be deduced in the propositional calculus, we never need to invoke A1 and A2 again. If needed, they can be recovered from DT and MP. Here is how we can recover A1 (\(A \to (B \to A)\)):

\begin {flalign*} \quad 1.\quad & A \vdash _0 A &&\text {(Id)}& \\[0.5em] \quad 2.\quad & A, B \vdash _0 A &&\text {(1, Mon)}& \\[0.5em] \quad 3.\quad & A \vdash _0 B \to A &&\text {(2, DT)}& \\[0.5em] \quad 4.\quad & \vdash _0 A \to (B \to A) &&\text {(3, DT)} & \end {flalign*}

Note that this is not a proof in the propositional calculus. It is a metalinguistic argument showing that a certain proof in the propositional calculus exists. Let me go through the steps.

Line 1 says that \(A\) is deducible from \(A\). This is the Id principle for deductions. I’ve explained above why it holds. Line 2 says that \(A\) is deducible from \(A\) and \(B\). This follows from line 1 by the general fact (called Monotonicity) that if \(A\) is deducible from some premises then \(A\) is also deducible from these premises together with any further premises. In the present case, it’s easy to see directly why the claim on line 2 holds: the sentence \(A\) qualifies a deduction of \(A\) from \(A\) and \(B\). Line 3 now applies the Deduction Theorem. It claims there is a deduction of \(B \to A\) from \(A\). It’s not immediately obvious what this deduction looks like, and we don’t need to know: since we’ve proved the Deduction Theorem, we can be sure that such a deduction exists. In the same way, line 4 infers that there is a proof of \(A \to (B \to A)\). Of course, we knew that all along: if \(A\) and \(B\) are arbitrary sentences, \(A \to (B \to A)\) is an axiom (A1), so it can be proved in one line, by simply writing it down. The point of the argument is that we didn’t need to invoke A1: all A1 instances are provable in any calculus that satisfies the structural rules and DT.

Now for some facts about negation.

We needed A3 in the derivation of these facts. As in the case of A1 and A2, we won’t need A3 any more, now that we have EFQ, DNE, and RAA. The relation \(\vdash _{0}\) is fully characterized by the structural rules Id, Mon, Cut, together with MP, DT, EFQ, DNE, and RAA.

We could have used different axioms, or a different combination of axioms and inference rules to obtain the same result. Frege’s original calculus, for example, has six axioms and an additional rule of substitution. But it is equivalent to the calculus I’ve introduced, since it determines the same relation \(\vdash _{0}\),

We can also design different types of proof systems that are equivalent to the propositional calculus. For example, you may have noticed that our metalinguistic proofs, using Id, Mon, Cut, MP, DT, etc., are generally simpler than proofs in our official calculus. We can turn these proofs into their own calculus. Each line of a proof, in this calculus, is a sequent \(\Gamma \vdash _{0} A\). There are no axioms. Instead, we have the rules Id, Mon, Cut, MP, etc. to operate on sequents. To show that \(A\) follows from \(\Gamma \), one tries to derive the sequent \(\Gamma \vdash _{0} A\).

Now, I’ve introduced ‘\(\Gamma \vdash _{0} A\)’ to mean ‘there is a deduction of \(A\) from \(\Gamma \) in the propositional calculus’. We don’t want the lines in our new calculus to refer to deductions in another calculus. So we should replace ‘\(\vdash _{0}\)’ by a different symbol. The standard choice is‘\(\Rightarrow \)’. Also, it turns out that we can drop Mon and Cut in favour of a slightly strengthened form of Id:

We can also drop EFQ, as it is derivable from RAA. The remaining rules of our new calculus are:

This is a stripped-down version of the sequent calculus invented by Gerhard Gentzen in the 1930s. It determines the same proof relation as our propositional calculus: a sequence \(\Gamma \Rightarrow A\) is provable in the sequent calculus iff there is a deduction of \(A\) from \(\Gamma \) in the propositional calculus.

Here is a simple schematic proof in the sequent calculus to show that \(A \to B\) and \(B \to C\) together entail \(A \to C\).

\begin {flalign*} \quad 1.\quad & A\to \! B,\; B\to \! C,\; A \Rightarrow A\to \! B && \text {Id$^+$} & \\[0.5em] \quad 2.\quad & A\to \! B,\; B\to \! C,\; A \Rightarrow B\to \! C && \text {Id$^+$} & \\[0.5em] \quad 3.\quad & A\to \! B,\; B\to \! C,\; A \Rightarrow A && \text {Id$^+$} & \\[0.5em] \quad 4.\quad & A\to \! B,\; B\to \! C,\; A \Rightarrow B && \text {1, 3, MP} & \\[0.5em] \quad 5.\quad & A\to \! B,\; B\to \! C,\; A \Rightarrow C && \text {2, 4, MP} & \\[0.5em] \quad 6.\quad & A\to \! B,\; B\to \! C \Rightarrow A\to \! C && \text {5, DT} & \end {flalign*}

When writing out proofs like this, one often needs to repeat the same sentences on the left of ‘\(\Rightarrow \)’ again and again. So-called natural deduction calculi introduce shortcuts to avoid these repetitions, dropping the ‘\(\Rightarrow \)’ symbol and using lines or boxes to indicate the sentences to its left. You may have encountered such a calculus in your intro logic course. If so, you may want to write down a natural-deduction proof of the above entailment and compare it with the sequent-calculus proof. (Can you see how the two are related?)

You may also have come across tableau calculi or tree proof calculi. These are, in effect, upside-down sequent proofs (of a slightly different type) in which all sentences are pushed to the left of the arrow.

All these calculi are much easier to use than our propositional calculus. On the flip side, proofs in the propositional calculus are easier to describe than proofs in the other calculi: a proof in our calculus is simply a list of \(\mathfrak {L}_{0}\)-sentences, each of which is either an instance of A1–A3 or follows from earlier sentences by MP. This makes it easier to prove metatheorems about what is or is not provable in the calculus. Since all the calculi are equivalent, and we’re mostly interested in metatheorems, we’ll take the propositional calculus to be the official calculus of classical propositional logic.

We’ll focus on classical logic in this course. But it is worth mentioning that there are also non-classical logics for \(\mathfrak {L}_{0}\). These always drop one or more of the principles Id, Mon, Cut, MP, DT, EFQ, DNE, and RAA, and sometimes replace them by other principles. For example, intuitionistic logic drops DNE. This has the possibly attractive consequence that the rules for negation become self-contained in the sense that they don’t allow proving any negation-free sentences that can’t already be proved without them.

1.3Semantics

You may have noticed that I have introduced \(\mathfrak {L}_0\) without saying anything about what the expressions of the language mean. Introductory logic texts often suggest that ’\(\neg \)’ and ’\(\to \)’ have roughly the same meaning as ‘not’ and ‘if …then’ in English. But we haven’t built this tenuous connection to English into the formal language. In this section, we’re going to study a more rigorous theory of meaning for \(\mathfrak {L}_0\).

The status of this kind of theory is controversial. Some hold that the meaning of a logical expression is given by the rules for reasoning with the expression, which we’ve already described. This approach to meaning is sometimes called inferential role semantics. (Semantics is the study of meaning.)

The kind of theory we’re about to develop instead belongs to the tradition of truth-conditional semantics. The guiding idea of truth-conditional semantics is that the meaning of a sentence can be given by stating what (typically non-linguistic) conditions must be satisfied for the sentence to be true. The German sentence ’Schnee ist weiss’, for example, is true iff snow is white, and arguably this information captures the core of its meaning. On the truth-conditional approach, the meaning of sub-sentential expressions like ’weiss’ or ’\(\neg \)’ is determined by their contribution to the truth-conditions of sentences in which they occur.

If we apply this approach to \(\mathfrak {L}_0\), we first need to assign truth-conditions to the sentence letters. To a first approximation, this might look as follows:

\(p\): snow is white.
\(q\): grass is purple.
…

Here I give the truth-conditions by using English sentences. This is not ideal, because English sentences may not have fully precise and determinate truth-conditions. (It isn’t clear what, exactly, must be the case for ’snow is white’ to be true.) Fortunately, we’ll see in a moment that we don’t need to worry about this problem because we won’t really need to assign a meaning to the sentence letters after all.

Moving on, we need to explain how the logical operators contribute to the truth-conditions of sentences in which they occur. This is the important part. We do this inductively, as follows:

(i)

\(\neg A\) is true iff \(A\) is not true.

(ii)

\(A \to B\) is true iff \(A\) is not true or \(B\) is true.

To see what this is saying, let’s pretend that I managed to assign precise truth-conditions to the sentence letter \(p\). We thereby know in what kinds of scenarios \(p\) is true and in what kinds of scenarios it is false. The above statement about \(\neg \) now tells us \(\neg p\) is true in precisely those scenarios in which \(p\) is not true. In general, it tells us how to determine the conditions under which \(\neg A\) is true based on the conditions under which \(A\) is true. Similarly, the statement about \(\to \) tells us how to determine the conditions under which \(A \to B\) is true based on the conditions under which \(A\) and \(B\) are true.

The truth-conditional conception of meaning is useful in logic because it ties in with a natural conception of entailment. Intuitively, some premises entail a conclusion iff the truth of the premises guarantee the truth of the conclusion; that is, there is no conceivable scenario in which the premises are true while the conclusion is false. If that’s right then knowledge of truth-conditions is exactly what we need if we want to know whether some premises entail some conclusion.

In fact, logic is about a particular type of entailment. Suppose we give the following truth-conditions to \(p\) and \(q\):

\(p\): Snow is white.
\(q\): Snow is purple.

Then \(p\) entails \(\neg q\): there is no scenario in which snow is white and also purple. The inference from \(p\) to \(\neg q\) is valid, but it is not logically valid. That’s because it depends on the meaning of the non-logical expression \(p\) and \(q\). Logic abstracts away from the interpretation of non-logical expressions. Some premises logically entail a conclusion iff there’s no conceivable scenario in which the premises are true and conclusion false, on any interpretation of the non-logical expressions.

Here we need a distinction between “logical” and “non-logical” expressions. This is best seen as a matter of choice. In epistemic logic, for example, a regimented version of ’it is known that’ counts as logical. Since propositional logic is the logic of the Boolean connectives, ‘\(\neg \)’ and ‘\(\to \)’ here count as logical; the sentence letters are non-logical.

We now have this preliminary account of logical entailment:

Some premises \(\Gamma \) logically entail a sentence \(A\) iff every scenario and interpretation of the sentence letters that makes the sentences in \(\Gamma \) true also makes \(A\) true.

We can render this simpler and more precise. Think of what you need to know about a pair of a scenario \(S\) and an interpretation \(I\) of the sentence letters in order to determine whether an arbitrary \(\mathfrak {L}_0\)-sentence – say, \(\neg p\) – is true. I could tell you that \(p\) means that snow is purple, and that the scenario is one in which snow is red. You could then figure out that \(\neg p\) is true (relative to \(S\) and \(I\)), using the interpretation rule for negation and the information I gave you. But you don’t need all that information. It would be enough if I merely told you that \(p\) means something that isn’t true in \(S\). By the interpretation rule for negation, you could infer that \(\neg p\) is true in \(S\) under \(I\). Generalizing, all the information we need about a pair of a scenario \(S\) and an interpretation \(I\) to determine whether an arbitrary \(\mathfrak {L}_{0}\)-sentence is true in \(S\) under \(I\) is which sentence letters are true and which are false in \(S\) under \(I\). This means that instead of quantifying over scenarios and interpretations, we can simply quantify over assignments of truth-values to the sentence letters. Such assignments are often called ‘interpretations’, but I find this misleading. We’ll call them ‘models’.

That is, a model is a function \(\sigma \) that assigns to each sentence letter \(p\) one of the two truth values, which I’ll label ‘\(T\)’ and ‘\(F\)’. We use standard function notation here, using ‘\(\sigma (p) = T\)’ to express that \(\sigma \) assigns the value \(T\) to \(p\) and ‘\(\sigma (p) = F\)’ to express that \(\sigma \) assigns \(F\) to \(p\).

Next, we specify how an assignment of truth-values to the sentence letters determines an assignment of truth-values to all sentences of \(\mathfrak {L}_0\), in accordance with our above interpretation rules for ’\(\neg \)’ and ’\(\to \)’. We write ‘\(\sigma \Vdash A\)’ (read: “\(\sigma \) satisfies A”) to mean that \(A\) is true in the model \(\sigma \), and ‘\(\sigma \not \Vdash A\)’ to mean that \(A\) is not true in \(\sigma \). The satisfaction relation \(\Vdash \) is defined as follows:

For example, if \(\sigma (p) = T\) and \(\sigma (q) = F\), then \(\sigma \Vdash p \to (q \to \neg q)\), as you can confirm by working through definition 1.5.

We can now define logical entailment, as already announced:

We allow \(\Gamma \) to be infinite, and to be empty. If something is (logically) entailed by the empty set of premises, it is called (logically) valid. Since our topic is logic, I’ll drop ‘logically’ when talking about validity and entailment from now on.

1.4Soundness and completeness

We have explored two perspectives on logic. The first was proof-theoretic: we studied proofs and deductions, defined as arrangements of symbols conforming to certain rules, without any extrinsic concern for what the symbols might mean. We then turned to a model-theoretic perspective, defining notions of validity and entailment in purely semantic terms.

Ideally, we’d like the two perspectives to harmonize: a sentence should be provable iff it is valid. More generally, we should have \(\Gamma \vdash _{0} A\) iff \(\Gamma \vDash A\). In this section, we will show that this is indeed the case.

We have two directions to check. We first show that if \(\Gamma \vdash _{0} A\) then \(\Gamma \vDash A\). This shows that the propositional calculus, and all the calculi equivalent to it, are sound with respect to the model-theoretic conception of entailment: anything that can be deduced from some premises in the calculus is entailed by the premises.

Afterwards, we’ll show the converse, that if \(\Gamma \vDash A\) then \(\Gamma \vdash _{0} A\). This shows that the calculus is complete: whenever something is entailed by some premises, it can be deduced from the premises.

The soundness proof is straightforward.

Completeness is harder. The first completeness proof for a propositional calculus was given by Paul Bernays in 1918. We’re going to use a different technique, due to Leon Henkin (1949), that works for a wide range of logics. We’ll use it again in chapter 3 to prove completeness for first-order logic.

Before we start, we need to define two key concepts. Let \(\Gamma \) be a set of \(\mathfrak {L}_0\)-sentences. We’ll say that \(\Gamma \) is consistent if one can’t deduce a contradiction from it: there is no sentence \(A\) such that \(\Gamma \vdash _{0} A\) and \(\Gamma \vdash _{0} \neg A\); equivalently, by exercise 1.8: \(\Gamma \not \vdash _{0} \bot \). We say that \(\Gamma \) is satisfiable if there is some model that satisfies every sentence in \(\Gamma \).

The following lemmas allow us to reformulate completeness in terms of consistency and satisfiability.

Now, completeness requires that whenever \(\Gamma \vDash A\) then \(\Gamma \vdash _{0} A\). Equivalently, by contraposition: Whenever \(\Gamma \not \vdash _{0} A\) then \(\Gamma \not \vDash A\). By lemma 1.2, \(\Gamma \not \vdash _{0} A\) iff \(\Gamma \cup \{\neg A\}\) is consistent. By lemma 1.1, \(\Gamma \not \vDash A\) iff \(\Gamma \cup \{\neg A\}\) is satisfiable. So what remains to be shown to establish completeness is this: Every consistent set of sentences is satisfiable.

We are going to prove this in two steps. First, we show that every consistent set can be extended to a maximal consistent set. A set is maximal consistent if it is consistent and contains either \(A\) or \(\neg A\), for each \(\mathfrak {L}_0\)-sentence \(A\). Then we show that every maximal consistent set is satisfied by a model that makes true all and only the sentence letters in the set.

En route to the first step, we start with an easy observation.

Now the first step:

For the second step, we also need a preliminary observation:

Here comes step 2.

Let’s put the pieces together: