Basics of Mathematical Logic

In section 6.2 of the text we see a brief introduction to Mathematical Logic and the impact that the Theory of Computation has had on that subject.

To begin our discussion, let's look at the basic building blocks of Mathematical Logic.

A formula is composed of variables, relations, logical operators, and quantifiers.

In formulas, variables take values from a specified universe. Some examples of universes include the positive integers and the real numbers.

A relation is a boolean function of one or more parameters. A typical example is the relation +(x,y,z), which evaluates to true if and only if x + y = z.

The quantifiers allowed in a formula include the existential quantifier ∃ and the universal quantifier ∀.

Here are some examples of formulas. The first example is a statement about the existence of 0:

∃ z ∀x +(x,z,x)

The second example is a statement about the existence of additive inverses.

∃ z ((∀x +(x,z,x)) ∧ (∀s ∃t +(s,t,z)))

An unquantified variable in a formula is a called a free variable. A formula with no free variables is called a sentence.

A somewhat more abstract kind of formula is one in which the relations are not explicitly specified. For example, we can rewrite the last example more generically by replacing the concrete relation + with a placeholder relation, R1:

∃ z ((∀x R1(x,z,x)) ∧ (∀s ∃t R1(s,t,z)))

To fully evaluate a sentence, we have to specify both the precise relations used and a universe for the variables. We do this by specifying a model. A given sentence may be true in one model, and false in another. For example, the last sentence is true in the model (ℤ,+), but false in the model (ℕ,+).

The set of all sentences that are true in a particular model is the theory of that model.

Deciding sentences

Given a sentence in some model, an important question is whether or not the sentence is true. A theory is decidable if there exists some computational process that can determine in a finite time whether or not a given sentence is true.

In section 6.2 the author presents a proof that the theory of the model M = (ℕ,+) is decidable.

Alonzo Church showed that the theory of the model M = (ℕ,+,×) is undecidable. One way to show this result is to use a reduction from ATM. Suppose we had a decider for this theory. Given any Turing machine M and input w we can construct the sentence

∃ x φM,w

where φM,w is an elaborate formula that says that x encodes a computation trace in which M accepts w. We would then be able to run the decider for our model on this sentence: if the sentence is true we have a proof that M accepts w, and we can use that knowledge to decide ATM.

A key idea driving the construction of the formula φM,w is the observation that if we have access to the operations of addition and multiplication we can decompose a large integer x into its component digits. In so doing, we can break the computation trace down into its component symbols and then check whether or not the resulting sequence of symbols represents a valid accepting computation for w running on M.

Proving things

Once we learn that certain theories are undecidable, we can fall back to an alternative strategy. We instead set up a system of proof and use it to manufacture a collection of statements that are provably true.

Proof is one of the central concepts in mathematics. In the framework we are setting up, a system of proof has several key ingredients.

  1. The system of proof operates within the context of a particular model.
  2. A proof is a systematic procedure for combining true sentences via standard logical operations to generate new sentences.
  3. In a system of proof an initial set of sentences that are assumed to be true is a set of axioms.

Proof systems have two key properties. A system of proof is sound if every statement that can be proven is true. A system of proof is complete if every true statement can be proved.

Unfortunately, Kurt Gödel showed that any system of proof is either sound or complete, but no system of proof can be both. In his famous incompleteness theorem he showed that any sound system of proof will be incomplete.

Here are some results leading up to a proof of the incompleteness theorem. The first step is to imagine a mechanical process for proof checking.

Theorem The language PROVABLE = { φ | φ has a proof } is Turing recognizable.

Proof Here is a recognizer for PROVABLE. The recognizer makes use on an enumerator E that enumerates the language of all possible strings.

On input φ:

  1. Run the enumerator E. For each string s that E prints, do the following:
    1. Check to see whether or not s is a valid proof of φ. If it is, stop and accept.

Since we showed earlier that the theory of the model M = (ℕ,+,×) is undecidable, we now can prove by contradiction that any proof system for this theory must be incomplete. We do this by constructing a decider for the theory:

On input φ:

  1. Run two copies of the recognizer for PROVABLE on φ and on ¬φ in parallel one step at a time until one of the two copies accepts.
  2. If the recognizer for PROVABLE accepts φ, stop and accept.
  3. If the recognizer for PROVABLE accepts ¬φ, stop and reject.

We know already that the theory of the model M = (ℕ,+,×) is undecidable, so this decider can't possibly work. The only way out of this to consider the possibility that the proof system is incomplete; that is, there exist true statements that can not be proved in our proof system. Allowing for incompleteness would allow step 1 above to run forever, which would cause our machine to not be a decider.

Finally, here is an alternative proof of incompleteness which makes use of the recursion theorem.

The proof makes use of the following Turing machine, S:

On input x:

  1. Use the recursion theorem to obtain <S>.
  2. Construct the sentence ψ = ¬∃c φS,0. This sentence says "It is not true that there is an accepting computation trace for S running on the input 0."
  3. Run the recognizer for provable statements on the sentence ψ. If it accepts, stop and accept.

There are two possibilities here. The first is that the sentence ψ we constructed has a proof. If it has a proof, it must be true. If the sentence is true, we have a contradiction because the sentence says that S does not accept 0, which contradicts the behavior of S itself. The second possibility is that ψ does not have a proof. If that is the case, there is no way that S will accept 0, and the sentence ψ must be true. This proves the existence of an unprovable true statement.