Propositional Logic: Deductive Systems

Abstract

The concept of deducing theorems from a set of axioms and rules of inference is very old and is familiar to every high-school student who has studied Euclidean geometry. Modern mathematics is expressed in a style of reasoning that is not far removed from the reasoning used by Greek mathematicians. This style can be characterized as ‘formalized informal reasoning’, meaning that while the proofs are expressed in natural language rather than in a formal system, there are conventions among mathematicians as to the forms of reasoning that are allowed. The deductive systems studied in this chapter were developed in an attempt to formalize mathematical reasoning.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

The concept of deducing theorems from a set of axioms and rules of inference is very old and is familiar to every high-school student who has studied Euclidean geometry. Modern mathematics is expressed in a style of reasoning that is not far removed from the reasoning used by Greek mathematicians. This style can be characterized as ‘formalized informal reasoning’, meaning that while the proofs are expressed in natural language rather than in a formal system, there are conventions among mathematicians as to the forms of reasoning that are allowed. The deductive systems studied in this chapter were developed in an attempt to formalize mathematical reasoning.

We present two deductive systems for propositional logic. The second one $H$ will be familiar because it is a formalization of step-by-step proofs in mathematics: It contains a set of three axioms and one rule of inference; proofs are constructed as a sequence of formulas, each of which is either an axiom (or a formula that has been previously proved) or a derivation of a formula from previous formulas in the sequence using the rule of inference. The system $G$ will be less familiar because it has one axiom and many rules of inference, but we present it first because it is almost trivial to prove the soundness and completeness of $G$ from its relationship with semantic tableaux. The proof of the soundness and completeness of $H$ is then relatively easy to show by using $G$. The chapter concludes with three short sections: the definition of an important property called consistency, a generalization to infinite sets of formulas, and a survey of other deductive systems for propositional logic.

3.1 Why Deductive Proofs?

Let U={A ₁,…,A _n }. Theorem 2.50 showed that U⊨A if and only if ⊨A ₁∧⋯∧A _n →A. Therefore, if U is a set of axioms, we can use the completeness of the method of semantic tableaux to determine if A follows from U (see Sect. 2.5.4 for precise definitions). Why would we want to go through the trouble of searching for a mathematical proof when we can easily compute if a formula is valid?

There are several problems with a purely semantical approach:

• The set of axioms may be infinite. For example, the axiom of induction in arithmetic is really an infinite set of axioms, one for each property to be proved. For semantic tableaux in propositional logic, the only formulas that appear in the tableaux are subformulas of the formula being checked or their negations, and there are only a finite number of such formulas.

• Very few logics have decision procedures like propositional logic.

• A decision procedure may not give insight into the relationship between the axioms and the theorem. For example, in proofs of theorems about prime numbers, we would want to know exactly where primality is used (Velleman, 2006, Sect. 3.7). This understanding can also help us propose other formulas that might be theorems.

• A decision procedure produces a ‘yes/no’ answer, so it is difficult to recognize intermediate results (lemmas). Clearly, the millions of mathematical theorems in existence could not have been inferred directly from axioms.

Definition 3.1

A deductive system is a set of formulas called axioms and a set of rules of inference. A proof in a deductive system is a sequence of formulas S={A ₁,…,A _n } such that each formula A _i is either an axiom or it can be inferred from previous formulas of the sequence $A_{j_{1}}, \ldots, A_{j_{k}}$, where j ₁<⋯<j _k <i, using a rule of inference. For A _n , the last formula in the sequence, we say that A _n is a theorem, the sequence S is a proof of A _n , and A _n is provable, denoted ⊢A _n . If ⊢A, then A may be used like an axiom in a subsequent proof. ■

The deductive approach can overcome the problems described above:

• There may be an infinite number of axioms, but only a finite number will appear in any proof.

• Although a proof is not a decision procedure, it can be mechanically checked; that is, given a sequence of formulas, an syntax-based algorithm can easily check whether the sequence is a proof as defined above.

• The proof of a formula clearly shows which axioms, theorems and rules are used and for what purposes.

• Once a theorem has been proved, it can be used in proofs like an axiom.

Deductive proofs are not generated by decision procedures because the formulas that appear in a proof are not limited to subformulas of the theorem and because there is no algorithm telling us how to generate the next formula in the sequence forming a proof. Nevertheless, algorithms and heuristics can be used to build software systems called automatic theorem provers which search for proofs. In Chap. 4, we will study a deductive system that has been successfully used in automatic theorem provers. Another promising approach is to use a proof assistant which performs administrative tasks such as proof checking, bookkeeping and cataloging previously proved theorems, but a person guides the search by suggesting lemmas that are likely to lead to a proof.

3.2 Gentzen System $G$

The first deductive system that we study is based on a system proposed by Gerhard Gentzen in the 1930s. The system itself will seem unfamiliar because it has one type of axiom and many rules of inference, unlike familiar mathematical theories which have multiple axioms and only a few rules of inference. Furthermore, deductions in the system can be naturally represented as trees rather in the linear format characteristic of mathematical proofs. However, it is this property that makes it easy to relate Gentzen systems to semantic tableaux.

Definition 3.2

(Gentzen system $G$)

An axiom of $G$ is a set of literals U containing a complementary pair. Rule of inference are used to infer a set of formulas U from one or two other sets of formulas U ₁ and U ₂; there are two types of rules, defined with reference to Fig. 3.1:

• Let {α ₁,α ₂}⊆U ₁ and let $U_{1}' = U_{1} - \{\alpha_{1}, \alpha_{2}\}$. Then $U=U_{1}'\cup\{\alpha\}$ can be inferred.

• Let {β ₁}⊆U ₁, {β ₂}⊆U ₂ and let $U_{1}' = U_{1} - \{\beta_{1}\}$, $U_{2}' = U_{2} - \{\beta_{2}\}$. Then $U=U_{1}'\cup U_{2}'\cup\{\beta\}$ can be inferred.

The set or sets of formulas U ₁,U ₂ are the premises and set of formulas U that is inferred is the conclusion. A set of formulas U that is an axiom or a conclusion is said to be proved, denoted ⊢U. The following notation is used for rules of inference:

$$ \frac{\vdash U_{1}'\cup \{\alpha_{1},\alpha_{2}\}}{\vdash U_{1}'\cup\{\alpha\}} \qquad \frac{\vdash U_{1}'\cup\{\beta_{1}\}\hspace{4em}\vdash U_{2}'\cup\{\beta_{2}\}}{\vdash U_{1}'\cup U_{2}'\cup\{\beta\}}. $$

Braces can be omitted with the understanding that a sequence of formulas is to be interpreted as a set (with no duplicates).  ■

Fig. 3.1

Classification of α- and β-formulas

Example 3.3

The following set of formulas is an axiom because it contains the complementary pair $\{r,\:\neg \,r\}$:

$$\vdash p \wedge q, q, r, \neg \,r, q \vee \neg \,r.$$

The disjunction rule for A ₁=q,A ₂=¬ r can be used to deduce:

$$\frac{\vdash p \wedge q, q, r, \neg \,r, q \vee \neg \,r}{\vdash p \wedge q, r, q \vee \neg \,r, q \vee \neg \,r}.$$

Removing the duplicate formula q∨¬ r gives:

$$\frac{\vdash p \wedge q, q, r, \neg \,r, q \vee \neg \,r}{\vdash p \wedge q,r, q \vee \neg \,r}.$$

Note that the premises {q,¬ r} are no longer elements of the conclusion. ■

A proof can be written as a sequence of sets of formulas, which are numbered for convenient reference. On the right of each line is its justification: either the set of formulas is an axiom, or it is the conclusion of a rule of inference applied to a set or sets of formulas earlier in the sequence. A rule of inference is identified by the rule used for the α- or β-formula on the principal operator of the conclusion and by the number or numbers of the lines containing the premises.

Example 3.4

Prove ⊢(p∨q)→(q∨p) in $G$.

Proof

 ■

Example 3.5

Prove $\vdash p\vee (q\wedge r)\:\mathbin {\rightarrow }\: (p\vee q)\wedge (p\vee r)$ in $G$.

Proof

 ■

3.2.1 The Relationship Between $G$ and Semantic Tableaux

It might seem that we have been rather clever to arrange all the inferences in these proofs so that everything comes out exactly right in the end. In fact, no cleverness was required. Let us rearrange the Gentzen proof into a tree format rather than a linear sequence of sets of formulas. Let the axioms be the leaves of the tree, and let the inference rules define the interior nodes. The root at the bottom will be labeled with the formula that is proved.

The proof from Example 3.4 is displayed in tree form on the left below:

If this looks familiar, it should. The semantic tableau on the right results from turning the derivation in $G$ upside down and replacing each formula in the labels on the nodes by its complement (Definition 2.57).

A set of formulas labeling a node in a semantic tableau is an implicit conjunction, that is, all the formulas in the set must evaluate to true for the set to be true. By taking complements, a set of formulas labeling a node in a derivation in $G$ is an implicit disjunction.

An axiom in $G$ is valid: Since it contains a complementary pair of literals, as a disjunction it is:

$$ \cdots \vee p \vee \cdots \vee \neg \,p \vee \cdots , $$

which is valid.

Consider a rule applied to obtain an α-formula, for example, A ₁∨A ₂; when the rule is written using disjunctions it becomes:

$$ \frac{\vdash \bigvee U_{1}' \vee A_{1} \vee A_{2}}{\vdash \bigvee U_{1}' \vee (A_{1} \vee A_{2})}, $$

and this is a valid inference in propositional logic that follows immediately from associativity.

Similarly, when a rule is applied to obtain a β-formula, we have:

$$ \frac{\vdash \bigvee U_{1}' \vee B_{1} \hspace{4em} \bigvee U_{2}' \vee B_{2}}{\vdash \bigvee U_{1}' \vee \bigvee U_{2}' \vee (B_{1} \wedge B_{2})}, $$

which follows by the distribution of disjunction over conjunction. This inference simply says that if we can prove both B ₁ and B ₂ then we can prove B ₁∧B ₂.

The relationship between semantic tableaux and Gentzen systems is formalized in the following theorem.

Theorem 3.6

Let A be a formula in propositional logic. Then ⊢A in $G$ if and only if there is a closed semantic tableau for ¬ A.

This follows immediately from a more general theorem on sets of formulas.

Theorem 3.7

Let U be a set of formulas and let $\bar{U}$ be the set of complements of formulas in U. Then ⊢U in $G$ if and only if there is a closed semantic tableau for  $\bar{U}$.

Proof

Let $T$ be a closed semantic tableau for $\bar{U}$. We prove ⊢U by induction on h, the height of $T$. The other direction is left as an exercise.

If h=0, then $T$ consists of a single node labeled by $\bar{U}$. By assumption, $G$ is closed, so it contains a complementary pair of literals {p,¬ p}, that is, $\bar{U}=\bar{U}' \cup \{p,\neg \,p\}$. Obviously, U=U′∪{¬ p,p} is an axiom in $G$, hence ⊢U.

If h>0, then some tableau rule was used on an α- or β-formula at the root of $T$ on a formula $\bar{\phi}\in \bar{U}$, that is, $\bar{U}=\bar{U}' \cup \{\bar{\phi}\}$. The proof proceeds by cases, where you must be careful to distinguish between applications of the tableau rules and applications of the Gentzen rules of the same name.

Case 1: :

$\bar{\phi}$ is an α-formula (such as) ¬ (A ₁∨A ₂). The tableau rule created a child node labeled by the set of formulas $\bar{U}' \cup \{\neg \,A_{1},\neg \,A_{2}\}$. By assumption, the subtree rooted at this node is a closed tableau, so by the inductive hypothesis, ⊢U′∪{A ₁,A ₂}. Using the appropriate rule of inference from $G$, we obtain ⊢U′∪{A ₁∨A ₂}, that is, ⊢U′∪{ϕ}, which is ⊢U.

Case 2: :

$\bar{\phi}$ is a β-formula (such as) ¬ (B ₁∧B ₂). The tableau rule created two child nodes labeled by the sets of formulas $\bar{U}' \cup \{\neg \,B_{1}\}$ and $\bar{U}' \cup \{\neg \,B_{2}\}$. By assumption, the subtrees rooted at this node are closed, so by the inductive hypothesis ⊢U′∪{B ₁} and ⊢U′∪{B ₂}. Using the appropriate rule of inference from $G$, we obtain ⊢U′∪{B ₁∧B ₂}, that is, ⊢U′∪{ϕ}, which is ⊢U. ■

Theorem 3.8

(Soundness and completeness of $G$)

⊨A if and only if ⊢A in $G$.

Proof

A is valid iff ¬ A is unsatisfiable iff there is a closed semantic tableau for ¬ A iff there is a proof of A in $G$. ■

The proof is very simple because we did all the hard work in the proof of the soundness and completeness of tableaux.

The Gentzen system $G$ described in this section is not very useful; other versions (surveyed in Sect. 3.9) are more convenient for proving theorems and are closer to Gentzen’s original formulation. We introduced $G$ as a theoretical stepping stone to Hilbert systems which we now describe.

3.3 Hilbert System $H$

In Gentzen systems there is one axiom and many rules of inference, while in a Hilbert system there are several axioms but only one rule of inference. In this section, we define the deductive system $H$ and use it to prove many theorems. Actually, only one theorem (Theorem 3.10) will be proved directly from the axioms and the rule of inference; practical use of the system depends on the use of derived rules, especially the deduction rule.

Notation:

Capital letters A,B,C,… represent arbitrary formulas in propositional logic. For example, the notation ⊢A→A means: for any formula A of propositional logic, the formula A→A can be proved.

Definition 3.9

(Deductive system $H$)

The axioms of $H$ are:

$$ \begin{array}{*{20}l} {\boldsymbol{{\rm Axiom}\,1}} & { \vdash (A \to (B \to A)),} \\ {\boldsymbol{{\rm Axiom}\,2}} & { \vdash (A \to (B \to C)) \to ((A \to B) \to (A \to C)),} \\ {\boldsymbol{{\rm Axiom}\,3}} & { \vdash (\neg \,B \to \neg \,A) \to (A \to B).} \\ \end{array} $$

The rule of inference is modus ponens (MP for short):

$$ \frac{\vdash A\hspace{5em}\vdash A\mathbin {\rightarrow }B}{\vdash B}. $$

In words: the formula B can be inferred from A and A→B.

The terminology used for $G$—premises, conclusion, theorem, proved— carries over to $H$, as does the symbol ⊢ meaning that a formula is proved. ■

Theorem 3.10

⊢A→A.

Proof

 ■

When an axiom is given as the justification, identify which formulas are substituted for the formulas A,B,C in the definition of the axioms above.

3.3.1 Axiom Schemes and Theorem Schemes *

As we noted above, a capital letter can be replaced by any formula of propositional logic, so, strictly speaking, ⊢A→(B→A) is not an axiom, and similarly, ⊢A→A is not a theorem. A more precise terminology would be to say that ⊢A→(B→A) is an axiom scheme that is a shorthand for an infinite number of axioms obtained by replacing the ‘variables’ A and B with actual formulas, for example:

$$ \overbrace{((p \vee \neg \,q) \mathbin {\leftrightarrow }r)}^{A} \;\;\mathbin {\rightarrow }\;\; (\;\;\;\overbrace{\neg \,(q \wedge \neg \,r)}^{B} \;\; \mathbin {\rightarrow }\;\; \overbrace{((p \vee \neg \,q) \mathbin {\leftrightarrow }r)}^{A} \;\;\;). $$

Similarly, ⊢A→A is a theorem scheme that is a shorthand for an infinite number of theorems that can be proved in $H$, including, for example:

$$ \vdash ((p \vee \neg \,q) \mathbin {\leftrightarrow }r) \mathbin {\rightarrow }((p \vee \neg \,q) \mathbin {\leftrightarrow }r). $$

We will not retain this precision in our presentation because it will always clear if a given formula is an instance of a particular axiom scheme or theorem scheme. For example, a formula ϕ is an instance of Axiom 1 if it is of the form:

where there are subtrees for the formulas represented by A and B. There is a simple and efficient algorithm that checks if ϕ is of this form and if the two subtrees A are identical.

3.3.2 The Deduction Rule

The proof of Theorem 3.10 is rather complicated for such a trivial formula. In order to formalize the powerful methods of inference used in mathematics, we introduce new rules of inference called derived rules. The most important derived rule is the deduction rule. Suppose that you want to prove A→B. Assume that A has already been proved and use it in the proof of B. This is not a proof of B unless A is an axiom or theorem that has been previously proved, in which case it can be used directly in the proof. However, we claim that the proof can be mechanically transformed into a proof of A→B.

Example 3.11

The deduction rule is used frequently in mathematics. Suppose that you want to prove that the sum of any two odd integer numbers is even, expressed formally as:

$$\mathit{odd}(x) \wedge \mathit{odd}(y) \mathbin {\rightarrow }\mathit{even}(x+y),$$

for every x and y. To prove this formula, let us assume the formula odd(x)∧odd(y) as if it were an additional axiom. We have available all the theorems we have already deduced about odd numbers, in particular, the theorem that any odd number can be expressed as 2k+1. Computing:

$$x+y=2k_{1}+1+2k_{2}+1=2(k_{1}+k_{2}+1),$$

we obtain that x+y is a multiple of 2, that is, even(x+y). The theorem now follows from the deduction rule which discharges the assumption. ■

To express the deduction rule, we extend the definition of proof.

Definition 3.12

Let U be a set of formulas and A a formula. The notation U⊢A means that the formulas in U are assumptions in the proof of A. A proof is a sequence of lines U _i ⊢ϕ _i , such that for each i, U _i ⊆U, and ϕ _i is an axiom, a previously proved theorem, a member of U _i or can be derived by MP from previous lines U _i′⊢ϕ _i′,U _i″⊢ϕ _i″, where i′,i″<i. ■

Rule 3.13

(Deduction rule)

$$\frac{U\cup\{A\}\vdash B}{U\vdash A\mathbin {\rightarrow }B}.$$

We must show that this derived rule is sound, that is, that the use of the derived rule does not increase the set of provable theorems in $H$. This is done by showing how to transform any proof using the rule into one that does not use the rule. Therefore, in principle, any proof that uses the derived rule could be transformed to one that uses only the three axioms and MP.

Theorem 3.14

(Deduction theorem)

The deduction rule is a sound derived rule.

Proof

We show by induction on the length n of the proof of U∪{A}⊢B how to obtain a proof of U⊢A→B that does not use the deduction rule.

For n=1, B is proved in one step, so B must be either an element of U∪{A} or an axiom of $H$ or a previously proved theorem:

• If B is A, then ⊢A→A by Theorem 3.10, so certainly U⊢A→A.

• Otherwise (B is an axiom or a previously proved theorem), here is a proof of U⊢A→B that does not use the deduction rule or the assumption A:

  

If n>1, the last step in the proof of U∪{A}⊢B is either a one-step inference of B or an inference of B using MP. In the first case, the result holds by the proof for n=1. Otherwise, MP was used, so there is a formula C and lines i,j<n in the proof such that line i in the proof is U∪{A}⊢C and line j is U∪{A}⊢C→B. By the inductive hypothesis, U⊢A→C and U⊢A→(C→B). A proof of U⊢A→B is given by:

  ■

3.4 Derived Rules in $H$

The general form of a derived rule will be one of:

$$ \frac{U\vdash \phi_1}{U\vdash \phi}, \qquad\frac{U\vdash \phi_1 \hspace{2em} U\vdash \phi_2}{U\vdash \phi}. $$

The first form is justified by proving the formula U⊢ϕ ₁→ϕ and the second by U⊢ϕ ₁→(ϕ ₂→ϕ); the formula U⊢ϕ that is the conclusion of the rule follows immediately by one or two applications of MP. For example, from Axiom 3 we immediately have the following rule:

Rule 3.15

(Contrapositive rule)

$$\frac{U\vdash \neg \,B \mathbin {\rightarrow }\neg \,A}{U\vdash A\mathbin {\rightarrow }B}.$$

The contrapositive is used extensively in mathematics. We showed the completeness of the method of semantic tableaux by proving: If a tableau is open, the formula is satisfiable, which is the contrapositive of the theorem that we wanted to prove: If a formula is unsatisfiable (not satisfiable), the tableau is closed (not open).

Theorem 3.16

⊢(A→B)→[(B→C)→(A→C)].

Proof

 ■

Rule 3.17

(Transitivity rule)

$$ \frac{{U \vdash A \to B\quad \quad \quad \quad U \vdash B \to C}}{{U \vdash A \to C}}. $$

The transitivity rule justifies the step-by-step development of a mathematical theorem ⊢A→C through a series of lemmas. The antecedent A of the theorem is used to prove a lemma ⊢A→B ₁ whose consequent is used to prove the next lemma ⊢B ₁→B ₂ and so on until the consequent of the theorem appears as ⊢B _n →C. Repeated use of the transitivity rule enables us to deduce ⊢A→C.

Theorem 3.18

⊢[A→(B→C)]→[B→(A→C)].

Proof

 ■

Rule 3.19

(Exchange of antecedent rule)

$$ \frac{{U \vdash A \to (B \to C)}}{{U \vdash B \to (A \to C)}}. $$

Exchanging the antecedent simply means that it doesn’t matter in which order we use the lemmas necessary in a proof.

Theorem 3.20

⊢¬ A→(A→B).

Proof

 ■

Theorem 3.21

⊢A→(¬ A→B).

Proof

 ■

These two theorems are of major theoretical importance. They say that if you can prove some formula A and its negation ¬ A, then you can prove any formula B! If you can prove any formula then there are no unprovable formulas so the concept of proof becomes meaningless.

Theorem 3.22

⊢¬ ¬ A→A.

Proof

 ■

Theorem 3.23

⊢A→¬ ¬ A.

Proof

 ■

Rule 3.24

(Double negation rule)

$$\frac{U\vdash \neg \,\neg \,A}{U\vdash A}, \qquad \frac{U\vdash A}{U\vdash \neg \,\neg \,A}.$$

Double negation is a very intuitive rule. We expect that ‘it is raining’ and ‘it is not true that it is not raining’ will have the same truth value, and that the second formula can be simplified to the first. Nevertheless, some logicians reject the rule because it is not constructive. Suppose that we can prove for some number n, ‘it is not true that n is prime’ which is the same as ‘it is not true that n is not composite’. This double negation could be reduced by the rule to ‘n is composite’, but we have not actually demonstrated any factors of n.

Theorem 3.25

⊢(A→B)→(¬ B→¬ A).

Proof

 ■

Rule 3.26

(Contrapositive rule)

$$\frac{U\vdash A \mathbin {\rightarrow }B}{U\vdash \neg \,B\mathbin {\rightarrow }\neg \,A}.$$

This is the other direction of the contrapositive rule shown earlier.

Recall from Sect. 2.3.3 the definition of the logical constants true as an abbreviation for p∨¬ p and false as an abbreviation for p∧¬ p. These can be expressed using implication and negation alone as p→p and ¬ (p→p).

Theorem 3.27

$$ \begin{array}{l} \vdash \mathit{true},\\ \vdash \neg \,\mathit{false}. \end{array} $$

Proof

⊢true is an instance of Theorem 3.10. ⊢¬ false, which is ⊢¬ ¬ (p→p), follows by double negation. ■

Theorem 3.28

⊢(¬ A→false)→A.

Proof

 ■

Rule 3.29

(Reductio ad absurdum)

$$\frac{U\vdash \neg \,A\mathbin {\rightarrow }\mathit{false}}{U\vdash A}.$$

Reductio ad absurdum is a very useful rule in mathematics: Assume the negation of what you wish to prove and show that it leads to a contradiction. This rule is also controversial because proving that ¬ A leads to a contradiction provides no reason that directly justifies A.

Here is an example of the use of this rule:

Theorem 3.30

⊢(A→¬ A)→¬ A.

Proof

 ■

We leave the proof of the following theorem as an exercise.

Theorem 3.31

⊢(¬ A→A)→A.

These two theorems may seem strange, but they can be understood on the semantic level. For the implication of Theorem 3.31 to be false, the antecedent ¬ A→A must be true and the consequent A false. But if A is false, then so is ¬ A→A≡A∨A, so the formula is true.

3.5 Theorems for Other Operators

So far we have worked with only negation and implication as operators. These two operators are adequate for defining all others (Sect. 2.4), so we can use these definitions to prove theorems using other operators. Recall that A∧B is defined as ¬ (A→¬ B), and A∨B is defined as ¬ A→B.

Theorem 3.32

⊢A→(B→(A∧B)).

Proof

 ■

Theorem 3.33

(Commutativity)

⊢A∨B↔B∨A.

Proof

The other direction is similar.  ■

The proofs of the following theorems are left as exercises.

Theorem 3.34

(Weakening)

• ⊢A→A∨B,

• ⊢B→A∨B,

• ⊢(A→B)→((C∨A)→(C∨B)).

Theorem 3.35

(Associativity)

• ⊢A∨(B∨C)↔(A∨B)∨C.

Theorem 3.36

(Distributivity)

• ⊢A∨(B∧C)↔(A∨B)∧(A∨C),

• ⊢A∧(B∨C)↔(A∧B)∨(A∧C).

3.6 Soundness and Completeness of $H$

We now prove the soundness and completeness of the Hilbert system $H$. As usual, soundness is easy to prove. Proving completeness will not be too difficult because we already know that the Gentzen system $G$ is complete so it is sufficient to show how to transform any proof in $G$ into a proof in $H$.

Theorem 3.37

The Hilbert system $H$ is sound: If ⊢A then ⊨A.

Proof

The proof is by structural induction. First we show that the axioms are valid, and then we show that MP preserves validity. Here are closed semantic tableaux for the negations of Axioms 1 and 3:

The construction of a tableau for the negation of Axiom 2 is left as an exercise.

Suppose that MP were not sound. There would be a set of formulas {A,A→B,B} such that A and A→B are valid, but B is not valid. Since B is not valid, there is an interpretation $I$ such that $\upsilon _I (B) = F$. Since A and A→B are valid, for any interpretation, in particular for $I$, $\upsilon _I (A) = \upsilon _I (A \to B) = T$. By definition of $\upsilon _I$ for implication, $\upsilon _I (B) = T$, contradicting $\upsilon _I (B) = F$. ■

There is no circularity in the final sentence of the proof: We are not using the syntactical proof rule MP, but, rather, the semantic definition of truth value in the presence of the implication operator.

Theorem 3.38

The Hilbert system $H$ is complete: If ⊨A then ⊢A.

By the completeness of the Gentzen system $G$ (Theorem 3.8), if ⊨A, then ⊢A in $G$. The proof of the theorem showed how to construct the proof of A by first constructing a semantic tableau for ¬ A; the tableau is guaranteed to close since A is valid. The completeness of $H$ is proved by showing how to transform a proof in $G$ into a proof in $H$. Note that all three steps can be carried out algorithmically: Given an arbitrary valid formula in propositional logic, a computer can generate its proof.

We need a more general result because a proof in $G$ is a sequence of sets of formulas, while a proof in $H$ is a sequence of formulas.

Theorem 3.39

If ⊢U in $G$, then ⊢⋁U in $H$.

The difficulty arises from the clash of the data structures used: U is a set while ⋁U is a single formula. To see why this is a problem, consider the base case of the induction. The set {¬ p,p} is an axiom in $G$ and we immediately have ⊢¬ p∨p in $H$ since this is simply ⊢p→p. But if the axiom in $G$ is {q,¬ p,r,p,s}, we can’t immediately conclude that ⊢q∨¬ p∨r∨p∨s in $H$.

Lemma 3.40

If U′⊆U and ⊢⋁U′ in $H$ then ⊢⋁U in $H$.

Proof

The proof is by induction using weakening, commutativity and associativity of disjunction (Theorems 3.34–3.35). We give the outline here and leave it as an exercise to fill in the details.

Suppose we have a proof of ⋁U′. By repeated application of Theorem 3.34, we can transform this into a proof of ⋁U″, where U″ is a permutation of the elements of U. By repeated applications of commutativity and associativity, we can move the elements of U″ to their proper places. ■

Example 3.41

Let U′={A,C}⊂{A,B,C}=U and suppose we have a proof of ⊢⋁U′=A∨C. This can be transformed into a proof of ⊢⋁U=A∨(B∨C) as follows, where Theorems 3.34–3.35 are used as derived rules:

   ■

Proof of Theorem 3.39

The proof is by induction on the structure of the proof in $G$. If U is an axiom, it contains a pair of complementary literals and ⊢¬ p∨p can be proved in $H$. By Lemma 3.40, this can be transformed into a proof of ⋁U.

Otherwise, the last step in the proof of U in $G$ is the application of a rule to an α- or β-formula. As usual, we will use disjunction and conjunction as representatives of α- and β-formulas.

Case 1: :

A rule in $G$ was applied to obtain an α-formula ⊢U ₁∪{A ₁∨A ₂} from ⊢U ₁∪{A ₁,A ₂}. By the inductive hypothesis, ⊢((⋁U ₁)∨A ₁)∨A ₂ in $H$ from which we infer ⊢⋁U ₁∨(A ₁∨A ₂) by associativity.

Case 2: :

A rule in $G$ was applied to obtain a β-formula ⊢U ₁∪U ₂∪{A ₁∧A ₂} from ⊢U ₁∪{A ₁} and ⊢U ₂∪{A ₂}. By the inductive hypothesis, ⊢(⋁U ₁)∨A ₁ and ⊢(⋁U ₂)∨A ₂ in $H$. We leave it to the reader to justify each step of the following deduction of ⊢⋁U ₁∨⋁U ₂∨(A ₁∧A ₂):

  ■

Proof of Theorem 3.38

If ⊨A then ⊢A in $G$ by Theorem 3.8. By the remark at the end of Definition 3.2, ⊢A is an abbreviation for ⊢{A}. By Theorem 3.39, ⊢⋁{A} in $H$. Since A is a single formula, ⊢A in $H$. ■

3.7 Consistency

What would mathematics be like if both 1+1=2 and ¬ (1+1=2)≡1+1≠2 could be proven? An inconsistent deductive system is useless, because all formulas are provable and the concept of proof becomes meaningless.

Definition 3.42

A set of formulas U is inconsistent iff for some formula A, both U⊢A and U⊢¬ A. U is consistent iff it is not inconsistent. A deductive system is inconsistent iff it contains an inconsistent set of formulas. ■

Theorem 3.43

U is inconsistent iff for all A, U⊢A.

Proof

Let A be an arbitrary formula. If U is inconsistent, for some formula B, U⊢B and U⊢¬ B. By Theorem 3.21, ⊢B→(¬ B→A). Using MP twice, U⊢A. The converse is trivial. ■

Corollary 3.44

U is consistent if and only if for some A, $U\not\vdash A$.

If a deductive system is sound, then ⊢A implies ⊨A, and, conversely, $\not\models A$ implies $\not\vdash A$. Therefore, if there is even a single falsifiable formula A in a sound system, the system must be consistent! Since $\not\models \mathit{false}$ (where false is an abbreviation for ¬ (p→p)), by the soundness of $H$, $\not\vdash \mathit{false}$. By Corollary 3.44, $H$ is consistent.

The following theorem is another way of characterizing inconsistency.

Theorem 3.45

U⊢A if and only if U∪{¬ A} is inconsistent.

Proof

If U⊢A, obviously U∪{¬ A}⊢A, since the extra assumption will not be used in the proof. U∪{¬ A}⊢¬ A because ¬ A is an assumption. By Definition 3.42, U∪{¬ A} is inconsistent.

Conversely, if U∪{¬ A} is inconsistent, then U∪{¬ A}⊢A by Theorem 3.43. By the deduction theorem, U⊢¬ A→A, and U⊢A follows by MP from ⊢(¬ A→A)→A (Theorem 3.31). ■

3.8 Strong Completeness and Compactness *

The construction of a semantic tableau can be generalized to an infinite set of formulas S={A ₁,A ₂,…}. The label of the root is {A ₁}. Whenever a rule is applied to a leaf of depth n, A _n+1 will be added to the label(s) of its child(ren) in addition to the α _i or β _i .

Theorem 3.46

A set of formulas S={A ₁,A ₂,…} is unsatisfiable if and only if a semantic tableau for S closes.

Proof

Here is an outline of the proof that is given in detail in Smullyan (1968, Chap. III).

If the tableau closes, there is only a finite subset S ₀⊂S of formulas on each closed branch, and S ₀ is unsatisfiable. By a generalization of Theorem 2.46 to an infinite set of formulas, it follows that S=S ₀∪(S−S ₀) is unsatisfiable.

Conversely, if the tableau is open, it can be shown that there must be an infinite branch containing all formulas in S, and the union of formulas in the labels of nodes on the branch forms a Hintikka set, from which a satisfying interpretation can be found. ■

The completeness of propositional logic now generalizes to:

Theorem 3.47

(Strong completeness)

Let U be a finite or countably infinite set of formulas and let A be a formula. If U⊨A then U⊢A.

The same construction proves the following important theorem.

Theorem 3.48

(Compactness)

Let S be a countably infinite set of formulas, and suppose that every finite subset of S is satisfiable. Then S is satisfiable.

Proof

Suppose that S were unsatisfiable. Then a semantic tableau for S must close. There are only a finite number of formulas labeling nodes on each closed branch. Each such set of formulas is a finite unsatisfiable subset of S, contracting the assumption that all finite subsets are satisfiable. ■

3.9 Variant Forms of the Deductive Systems *

$G$ and $H$, the deductive systems that we presented in detail, are two of many possible deductive systems for propositional logic. Different systems are obtained by changing the operators, the axioms or the representations of proofs. In propositional logic, all these systems are equivalent in the sense that they are sound and complete. In this section, we survey some of these variants.

3.9.1 Hilbert Systems

Hilbert systems almost invariably have MP as the only rule. They differ in the choice of primitive operators and axioms. For example, $H^\prime$ is an Hilbert system where Axiom 3 is replaced by:

$$ {\rm Axiom}\,3^\prime\quad - (\neg \,B \to \neg \,A) \to ((\neg \,B \to A) \to B). $$

Theorem 3.49

$H$ and $H^\prime$ are equivalent in the sense that a proof in one system can be transformed into a proof in the other.

Proof

We prove Axiom 3′ in $H$. It follows that any proof in $H^\prime$ can be transformed into a proof in $H$, by starting with this proof of the new axiom and using it as a previously proved theorem.

The use of the deduction theorem is legal because its proof in $H$ does not use Axiom 3, so the identical proof can be done in $H^\prime$.

We leave it as an exercise to prove Axiom 3 in $H^\prime$.  ■

Either conjunction or disjunction may replace implication as the binary operator in the formulation of a Hilbert system. Implication can then be defined by ¬ (A∧¬ B) or ¬ A∨B, respectively, and MP is still the only inference rule. For disjunction, a set of axioms is:

$$ \begin{array}{*{20}l} {{\rm Axiom}\,1} & { - A \vee A \to A,} \\ {{\rm Axiom}\,2} & { - A \to A \vee B,} \\ {{\rm Axiom}\,3} & { - A \vee B \to B \vee A,} \\ {{\rm Axiom}\,4} & { - (B \to C) \to (A \vee B \to A \vee C).} \\ \end{array} $$

The steps needed to show the equivalence of this system with $H$ are given in Mendelson (2009, Exercise 1.54).

Finally, Meredith’s axiom:

$$ \vdash\,(\{[(A\mathbin {\rightarrow }B)\mathbin {\rightarrow }(\neg \,C\mathbin {\rightarrow }\neg \,D)] \mathbin {\rightarrow }C\}\mathbin {\rightarrow }E) \mathbin {\rightarrow }[(E\mathbin {\rightarrow }A) \mathbin {\rightarrow }(D\mathbin {\rightarrow }A)], $$

together with MP as the rule of inference is a complete deductive system for propositional logic. Adventurous readers are invited to prove the axioms of $H$ from Meredith’s axiom following the 37-step plan given in Monk (1976, Exercise 8.50).

3.9.2 Gentzen Systems

$G$ was constructed in order to simplify the theoretical treatment by using a notation that is identical to that of semantic tableaux. We now present a deductive system similar to the one that Gentzen originally proposed; this system is taken from Smullyan (1968, Chap. XI).

Definition 3.50

If U and V are (possibly empty) sets of formulas, then U⇒V is a sequent. ■

Intuitively, a sequent represents ‘provable from’ in the sense that the formulas in U are assumptions for the set of formulas V that are to be proved. The symbol ⇒ is similar to the symbol ⊢ in Hilbert systems, except that ⇒ is part of the object language of the deductive system being formalized, while ⊢ is a metalanguage notation used to reason about deductive systems.

Definition 3.51

Axioms in the Gentzen sequent system $S$ are sequents of the form:

$$U \cup \{A\}\mathrel {\Rightarrow }V \cup \{A\}.$$

The rules of inference are shown in Fig. 3.2. ■

Fig. 3.2

Rules of inference for sequents

The semantics of the sequent system $S$ are defined as follows:

Definition 3.52

Let S=U⇒V be a sequent where U={U ₁,…,U _n } and V={V ₁,…,V _m }, and let $I$ be an interpretation for U∪V. Then $\upsilon _I (S) = T$ if and only if $\upsilon _I (U_1 ) = \cdots = \upsilon _I (U_n ) = T$ implies that for some i, $\upsilon _I (V_i ) = T$. ■

This definition relates sequents to formulas: Given an interpretation $I$ for U∪V, $\upsilon _I (U \Rightarrow V) = T$ if and only if $\upsilon _I ( \bigwedge U \to \bigvee V) = T$.

3.9.3 Natural Deduction

The advantage of working with sequents is that the deduction theorem is a rule of inference: introduction into the consequent of →. The convenience of Gentzen systems is apparent when proofs are presented in a format called natural deduction that emphasizes the role of assumptions.

Look at the proof of Theorem 3.30, for example. The assumptions are dragged along throughout the entire deduction, even though each is used only twice, once as an assumption and once in the deduction rule. The way we reason in mathematics is to set out the assumptions once when they are first needed and then to discharge them by using the deduction rule. A natural deduction proof of Theorem 3.30 is shown in Fig. 3.3.

Fig. 3.3

A natural deduction proof

The boxes indicate the scope of assumptions. Just as in programming where local variables in procedures can only be used within the procedure and disappear when the procedure is left, an assumption can only be used within the scope of its box, and once it is discharged by using it in a deduction, it is no longer available.

3.9.4 Subformula Property

Definition 3.53

A deductive system has the subformula property iff any formula appearing in a proof of A is either a subformula of A or the negation of a subformula of A. ■

The systems $G$ and $S$ have the subformula property while $H$ does not. For example, in the proof of the theorem of double negation ⊢¬ ¬ A→A, the formula ⊢¬ ¬ ¬ ¬ A→¬ ¬ A appeared even though it is obviously not a subformula of the theorem.

Gentzen proposed his deductive system in order to obtain a system with the subformula property. Then he defined the system $S^\prime$ by adding an additional rule of inference, the cut rule:

$$ \frac{{U,A \Rightarrow V\quad \quad \quad \quad U \Rightarrow V,A}}{{U \Rightarrow V}} $$

to the system $S$ and showed that proofs in $S^\prime$ can be mechanically transformed into proofs in $S$. See Smullyan (1968, Chap. XII) for a proof of the following theorem.

Theorem 3.54

(Gentzen’s Hauptsatz)

Any proof in $S^\prime$ can be transformed into a proof in $S$ not using the cut rule.

3.10 Summary

Deductive systems were developed to formalize mathematical reasoning. The structure of Hilbert systems such as $H$ imitates the style of mathematical theories: a small number of axioms, modus ponens as the sole rule of inference and proofs as linear sequences of formulas. The problem with Hilbert systems is that they offer no guidance on how to find a proof of a formula. Gentzen systems such as $G$ (and variants that use sequents or natural deduction) facilitate finding proofs because all formulas that appear are subformulas of the formula to be proved or their negations.

Both the deductive systems $G$ and $H$ are sound and complete. Completeness of $G$ follows directly from the completeness of the method of semantic tableaux as a decision procedure for satisfiability and validity in propositional logic. However, the method of semantic tableaux is not very efficient. Our task in the next chapters is to study more efficient algorithms for satisfiability and validity.

3.11 Further Reading

Our presentation is based upon Smullyan (1968) who showed how Gentzen systems are closely related to tableaux. The deductive system $H$ is from Mendelson (2009); he develops the theory of $H$ (and later its generalization to first-order logic) without recourse to tableaux. Huth and Ryan (2004) base their presentation of logic on natural deduction. Velleman (2006) will help you learn how to prove theorems in mathematics.

3.12 Exercises

3.1

Prove in $G$:

$$ \begin{array}{l} \vdash (A \mathbin {\rightarrow }B) \mathbin {\rightarrow }(\neg \,B \mathbin {\rightarrow }\neg \,A), \\[2pt] \vdash (A \mathbin {\rightarrow }B) \mathbin {\rightarrow }((\neg \,A \mathbin {\rightarrow }B) \mathbin {\rightarrow }B), \\[2pt] \vdash ((A\mathbin {\rightarrow }B) \mathbin {\rightarrow }A) \mathbin {\rightarrow }A. \end{array} $$

3.2

Prove that if ⊢U in $G$ then there is a closed semantic tableau for $\bar{U}$ (the forward direction of Theorem 3.7).

3.3

Prove the derived rule modus tollens:

$$ \frac{\vdash \neg \,B\hspace{5em}\vdash A\mathbin {\rightarrow }B}{\vdash \neg \,A}. $$

3.4

Give proofs in $G$ for each of the three axioms of $H$.

3.5

Prove ⊢(¬ A→A)→A (Theorem 3.31) in $H$.

3.6

Prove ⊢(A→B)∨(B→C) in $H$.

3.7

Prove ⊢((A→B)→A)→A in $H$.

3.8

Prove {¬ A}⊢(¬ B→A)→B in $H$.

3.9

Prove Theorem 3.34 in $H$:

• ⊢A→A∨B,

• ⊢B→A∨B,

• ⊢(A→B)→((C∨A)→(C∨B)).

3.10

Prove Theorem 3.35 in $H$:

• ⊢A∨(B∨C)↔(A∨B)∨C.

3.11

Prove Theorem 3.36 in $H$:

• ⊢A∨(B∧C)↔(A∨B)∧(A∨C),

• ⊢A∧(B∨C)↔(A∧B)∨(A∧C).

3.12

Prove that Axiom 2 of $H$ is valid by constructing a semantic tableau for its negation.

3.13

Complete the proof that if U′⊆U and ⊢⋁U′ then ⊢⋁U (Lemma 3.40).

3.14

Prove the last two formulas of Exercise 3.1 in $H$.

3.15

* Prove Axiom 3 of $H$ in $H^\prime$.

3.16

* Prove that the Gentzen sequent system $S$ is sound and complete.

3.17

* Prove that a set of formulas U is inconsistent if and only if there is a finite set of formulas {A ₁,…,A _n }⊆U such that ⊢¬ A ₁∨⋯∨¬ A _n .

3.18

A set of formulas U is maximally consistent iff every proper superset of U is not consistent. Let S be a countable, consistent set of formulas. Prove:

• 1. Every finite subset of S is satisfiable.

• 2. For every formula A, at least one of S∪{A}, S∪{¬ A} is consistent.

• 3. S can be extended to a maximally consistent set.