Analysis of the Axiomatic Method

From the previous section, one might conclude that if we were to extend our formal system L to system with more and more theorems, the more likely it will be that there will be some well-formed formula A such that both A and ~A are theorem. Obviously, such a situation will be undesirable. In fact this is considered to be a fundamental and critical question: does the system imply any contradictory theorems? If it does, clearly something is very wrong, and it is useless to inquire into other questions such as independence of the axioms in the system until this defect has been eliminated.

From the logical point of view we can make the following definition of consistency:

An axiom system L is called consistent if contradictory statements are not implied by L.

Putting the same thing is a different way, we say that an extension of formal system L is consistent if for no well-formed formula A are both A and ~A theorems of the extension.

Seemingly, everything looks good. But this definition give rise to certain questions and criticisms. To begin with, given an axiom system L, how, in the hell, are we going to tell whether it is consistent or not? Conceivably we might prove two theorems from L which contradict one another, and hence conclude that L is not consistent. But, supposing that this does not happen, are we going to conclude that L is consistent? How can we tell that, if we continued stating and proving theorems, we might not ultimately arrive at contradictory statements and hence inconsistency?

Lemma. Proposition 2.17

Formal system L is consistent.

Proof.

Suppose not. [We take the negation of the proposition and suppose it to be true.] That, is assume, to the contrary that there is a well-formed formula A such that A and ~A. Then by the Soundness theorem, both A and ~A are tautologies. This is impossible [since if A is a tautology, then ~A is a contradiction and if ~A is a tautology, then A is a contradiction.]

This contradictions the supposition that A and ~A are theorems. [Hence, the supposition is false and the proposition is true.] Therefore, L must be consistent.

This completes the proof.

Lemma. Proposition 2.18

An extension of the formal system L^* of L is consistent if, and only if, there is a well-formed formula which is not a theorem of L^*.

Proof.

Now we will describe one circumstance in which a consistent extension can be obtained.

Lemma. Proposition 2.19

Let L^*  be a consistent extension of L and let A be a well-formed formula of L which is not a theorem of L^* . Then L^** is also consistent, where L^** is the extension of L obtained from L^** by including ~A as an additional axiom.

Proof. L^*  L^**

Let A be a well-formed formula of L which is not a theorem of L^*. Suppose Not. [We take the negation of the proposition and suppose it to be true.] That is, assume to the contrary that L^** is not consistent. Then, for some well-formed formula, B, in the system L^** and we have

  _L** B    and    _L** (~B)

[Why? Because L^** is not consistent by supposition. So, by definition of consistency both B and ~B are theorems of the extension.]

Now it follows [just as in the proof of Proposition 2.18] that

 _L** A

But L^** differ from L^* only in having ~A as an addition axiom, so

 _L** A

is equivalent to

~A _L* A

[Note that a proof in L^** is just a deduction from ~A in L^*.]

So, by the Deduction Theorem, we have

 _L* ((~A) → A) _____________________(1)

But _L (((~A) → A) → A) by Lemma [See example].

Hence, in system L^**, we have

 _L* (((~A) → A) → A) _____________________(2)

Now by applying modus ponens to expression (1) and expression (2), we get

 _L* A

But this contradicts the supposition that A is not a theorem of L^*. [Thus, the supposition is false and the proposition is true.] Hence, L^* must be consistent.

This completes the proof.

There is obviously a limit somewhere to the well-formed formulas which we can include as additional axioms in an extension of L while maintaining consistency. Attaining this limit is the object of the next proposition, but first let us describe the situation in a definition.

Definition: An extension of L is complete if for each well-formed formula A, either A or ~A is a theorem of the extension.

Lemma. Proposition 2.21

Let L^* be a consistent extension of L. Then there is a consistent complete extension of L^*.

Proof.

--------------------------------------------------------------------------

It is our purpose to show that a well-formed formula is theorem if, and only if, it is a tautology.

The Soundness Theorem: Every theorem of formal system L is a tautology.

Proof.

The proof is by induction on the number of well-formed formulas, n, in a sequence of well-formed formulas that constitutes a proof of A. Let A be a theorem.

For base step, suppose that the proof of A has only one well-formed formula in it. Then, A must be an axiom. All axioms are tautology. The verification of this is by constructing truth tables.

For inductive step, suppose that the proof of A contains n well-formed formulas where n > 1, and suppose as induction hypothesis that all theorems of L which have proofs in fewer than n steps are tautologies. Then, we have one of two possibilities:

Hence, by the principle of induction, every theorem of formal system L is a tautology.

This completes the proof.

To prove the converse of this, we need two new ideas: extensions of L and consistency.