Goedel's Theorem

One of the benefits of Herbrand logic is that some theories that do not have finite axiomatizations, or even recursively enumerable axiomatizations, in first-order logic are finitely axiomatizable in Herbrand logic. In particular, the theory of natural arithmetic is finitely axiomatizable.

Herbrand logic is therefore more expressive than FOL. In FOL, we can encode Diophantine equations (see Proof and Model theory), but because it is semi-decidable, we are ensured that there is no r.e. axiomatization of the negation of an arbitrary diophantine since otherwise FOL would decide Diophantines, which clearly it can't. But, in Herbrand logic, we can encode both the Diophantine and its negation; obviously, the downside is that we lose semi-decidability of entailment.

Recall that the theory of natural arithmetic is just the model A = <N, <, +, * >. Its universe is the natural numbers, < is an infinite table that defines the total ordering on the naturals; + and * are the usual functions that map two natural numbers onto their sum and product, respectively.

Goedel's first incompleteness proof shows that with multiplication, addition, and an ordering on integers, it is possible to encode the true sentence "this sentence is unprovable". That is, this sentence is satisfied in A. One consequence of this result is that in every complete logic, arithmetic has no recursively enumerable axiomatization.

For the purpose of contradiction, suppose there were a recursively enumerable axiomatization of arithmetic in a complete logic. Then by completeness of the logic there must be a proof of every true sentence from that axiomatization. That contradicts the truth of the sentence "this sentence is unprovable". Hence there can be no such recursively enumerable axiomatization.

In an incomplete logic that proof no longer works. Because Goedel's proof relies on representing proofs as integers, infinite proofs cannot be represented by Goedel's encoding. In that case Goedel's statement might be more accurately translated as "this statement is not finitely provable". Or because the logic is incomplete, there is no finite proof system that will prove all entailed sentences, which means that any proof system encoded using Goedel's methodology is incomplete. Certainly then there would definitely be sentences true that are not provable.

To summarize, the existence of a finite axiomatization of arithmetic in an incomplete logic is consistent with Goedel's first incompleteness result. Herbrand logic appears to admit such a finite axiomatization.

What follows is an outline for how to finitely axiomatize arithmetic over the natural numbers in Herbrand logic.

Let the vocabulary be {0, s, <, Add, Mult}. First we exhibit axioms that are strong enough to capture arithmetic over the natural numbers. Then we argue that these axioms are consistent.

Theorem (Axioms for <): Let A be the model of arithmetic <N,<,+,*>, where N = {0, s(0), ...}. Let Δ be the following set of sentences.

1. x < s(x)
2. x < s(y) ⇐ x < y
3. ¬ x < x
4. ¬ s(x) < y ⇐ ¬ x < y

Theorem (Axioms for +): Let A be the model of arithmetic <N,<,+,*>, where N = {0, s(0), ...}. Let Δ be the following set of sentences.

1. Add(x,y,z) ∧ Add(x,y,w) ⇒ z=w
2. Add(s(x), y, s(z)) ⇐ Add(x, y, z)
3. Add(0, x, x)
4. Add(x, s(y), s(z)) ⇐ Add(x, y, z)

Theorem (Axioms for *): Let A be the model of arithmetic <N,<,+,*>, where N = {0, s(0), ...}. Let Δ be the following set of sentences.

0. Axioms of addition from above.
1. Mult(x,y,z) ∧ Mult(x,y,w) ⇒ z=w
2. Mult(s(x), y, w) ⇐ Mult(x,y,z) ∧ Add(z, y, w)
3. Mult(x,y,z) ⇐ Mult(y,x,z)
4. Mult(0,y,0)

The above three theorems ensure the axioms given entail the theory of arithmetic; it is left to show that the axioms are consistent. The difficulty with showing the axioms are consistent is that we would need to demonstrate the model that satisfies them, which is infinite and therefore cannot be demonstrated. We might instead try appealing to syntactic characteristics of the sentences. In first-order logic, for instance, a set of disjunction-free, quantifier-free implications where every literal is positive (a Horn clause) is always satisfied by the model where everything is true. In this example, however, we see that the model where ∀xyz.Add(x,y,z) is satisfied is explicitly disallowed by the axiom that says Add(x,y,z) ∧ Add(x,y,w) ⇒ z=w. In Herbrand logic, a set of Horn clauses that mention = is not necessarily satisfied by the model where all the ground atoms are true, as evidenced here.

Rather than presenting a proof that demonstrates the above axioms are consistent and therefore integer arithmetic is consistent (one of the very questions logic was invented to investigate), here we argue that if the rules of algebra taught in high school are consistent, so are the axioms above.

x < s(x)

obviously x < x+1 is true

x < s(y) ⇐ x < y

x < y (add 1 to y since x is already smaller than y) x < y+1

¬ x < x

obviously x is never less than itself

¬ s(x) < y ⇐ ¬ x < y

(rewrite with >=) x >= y (add 1 to x since x is already larger than y) x+1 >= y

Add(x,y,z) ∧ Add(x,y,w) ⇒ z=w

functionality of addition: x+y=z and x+y=w means z=w

Add(s(x), y, s(z)) ⇐ Add(x, y, z)

x + y = z (add 1 to both sides) x + y + 1 = z + 1 (grouping) (x+1) + y = (z+1)

Add(0, x, x)

0 + x = x

Add(x, s(y), s(z)) ⇐ Add(x, y, z)

x + y = z (add 1 to both sides) x + y + 1 = z + 1 (group) x + (y+1) = (z+1)

Mult(x,y,z) ∧ Mult(x,y,w) ⇒ z=w

x*y = z and x*y = w ensures z=w

Mult(s(x), y, w) ⇐ Mult(x,y,z) ∧ Add(z, y, w)

x*y=z and z+y=w (substitute x+y for z in second equation) x*y+y=w (factor out the y) (x+1) * y = w

Mult(x,y,z) ⇐ Mult(y,x,z)

y * x = z (symmetry of *) x * y = z

Mult(0,y,0)

0 * y = 0