Tutorial 4: Number Theory 1

12/28/13

Tutorial 4: Number Theory 1

Formal Number Theory is the formalization of ordinary elementary arithmetic. It deals with addition (+), multiplication (here, .), it has a constant (0), and the successor function ('). And it uses Identity. The successor function takes 0 to 0' (ie 1), then 0'' is 2. And so on. In many formal systems, 1 is defined as 0' and 2 as 1' (or 0'') and so on. Our system allows in the numerals 0,1,2,3 as constants (but not 4,5,6 etc.-- we need only enough numerals for illustration), then any definitions have to be explicitly introduced. Then the formal theory proves a number of theorems like

x'=x+1.

The end result is that number theory can be done within predicate logic.

Of particular interest, intellectually, is the use of an axiom schema (that of induction).

Axioms or First Principles need to be decidable. That is, there should be a mechanical way of answering yes/no to the question of whether a particular formula is an axiom. Often axiom systems have only a finite number of axioms (say 5 or 6 of them) and these are decidable by virtue of the fact that we only have to look through them to see whether a presented formula is among them (and thus is or is not an axiom). But it is possible for an axiom system to have an infinite number of axioms. Obviously we cannot complete looking through these individually. But if the infinite among them all fit a certain pattern, we can see whether or not a presented formula fits the pattern (and thus is or is not an axiom). So, purely as an illustration, some theory might have an axiom schema (or pattern) to the effect that

any formula with form φ[x] is an axiom, where φ[x] here means any well formed formula with at least one occurrence of the free variable x.

with this example, the formulas Fx,Gx,Hx, etc are all axioms (infinitely many of them). We can decide which formulas are axioms (even, here, with infinitely many axioms).

The induction axiom schema, permitting infinitely many axioms, will be similar to this.

In sum

Formal Number Theory has five proper symbols {=,',+, .,0} and six proper axioms

(∀x)(∀y)(x'=y'⊃x=y),
(∀x)~(x'=0),
(∀x)(x+0=x),
(∀x)(∀y)(x+y'=(x+y)'),
(∀x)(x.0=0),
(∀x)(∀y)(x.y'=x.y+x)

And the axiom (metalanguage) schema of induction. If φ[x] is any formula in the object language with free variable x then

(φ[0]∧(∀x)(φ[x]⊃φ[x'])) ⊃ (∀x)φ[x]

is an axiom.

What the schema says in English, roughly, is

If (φ[0]∧(∀x)(φ[x]⊃φ[x'])) then (∀x)φ[x]
which is
If φ[0]and(∀x)(φ[x]⊃φ[x'])) then (∀x)φ[x]
which is
If you have a formula φ[x], with free variable x, proved for the case of 0 substituted for that x and(∀x)(φ[x]⊃φ[x'])) then (∀x)φ[x]
which is
If you have a formula φ[x], with free variable x, proved for the case of 0 substituted for that x and you have for all x (φ[x]⊃φ[x'])) then (∀x)φ[x]
which is
If you have a formula φ[x], with free variable x, proved for the case of 0 substituted for that x and you have for all x (if φ[x]then φ[x'])) then (∀x)φ[x]
which is
If you have a formula φ[x], with free variable x, proved for the case of 0 substituted for that x and you have for all x (if φ[with x for x] then φ[with x'for x])) then (∀x)φ[x]
which is
If you have a formula φ[x], with free variable x, proved for the case of 0 substituted for that x and you have for all x (if φ[with x for x]then φ[with x'for x])) then you can have All x φ[x for x]

 

Derive the following theorems (solutions are provided at the end of this Journal)

 

---

 

Exercise to accompany Number Theory I.

Exercise 1(of 3)

 

 

Derive the following. (These first 3 you probably will have done before under the heading of Identity.)

Theorem 1 (*the axioms of formal arithmetic are not needed for this*)

∴(∀x)(x=x)

Theorem 2 (*the axioms of formal arithmetic are not needed for this*)

∴(∀x)(∀y)((x=y) ⊃(y=x))

Theorem 3 (*the axioms of formal arithmetic are not needed for this*)

∴(∀x)(∀y)(∀z)(((x=y)∧(y=z)) ⊃(x=z))

From here on we will not bother to Universally quantify the theorem by forming the closure-- there are no free variables in the axioms so that can always be done, we will just state the theorems in their free variable form.

Theorem 4 (*the axioms of formal arithmetic are not needed for this*)

∴x=y⊃(x+z)=(y+z)

Exercise 2(of 3)

Theorem 5

(∀x)(∀y)(x'=y'⊃x=y),
(∀x)~(x'=0),
(∀x)(x+0=x),
(∀x)(∀y)(x+y'=(x+y)'),
(∀x)(x.0=0),
(∀x)(∀y)(x.y'=x.y+x)
∴
(x+0'=x')

From now on the Schema of Induction will start to creep in. The use of earlier theorems is also permitted (even the closures if you wish)-- use the Rule T (rule of Theorem) and annotate the line correctly.

Theorem 6

(∀x)(∀y)(x'=y'⊃x=y),
(∀x)~(x'=0),
(∀x)(x+0=x),
(∀x)(∀y)(x+y'=(x+y)'),
(∀x)(x.0=0),
(∀x)(∀y)(x.y'=x.y+x)
∴
x=0+x

Theorem 7

(∀x)(∀y)(x'=y'⊃x=y),
(∀x)~(x'=0),
(∀x)(x+0=x),
(∀x)(∀y)(x+y'=(x+y)'),
(∀x)(x.0=0),
(∀x)(∀y)(x.y'=x.y+x)
∴
x'+y=(x+y)'

Exercise 3(of 3)

 

Theorem 8

(∀x)(∀y)(x'=y'⊃x=y),
(∀x)~(x'=0),
(∀x)(x+0=x),
(∀x)(∀y)(x+y'=(x+y)'),
(∀x)(x.0=0),
(∀x)(∀y)(x.y'=x.y+x)
∴
x+y=y+x

Theorem 9

(∀x)(∀y)(x'=y'⊃x=y),
(∀x)~(x'=0),
(∀x)(x+0=x),
(∀x)(∀y)(x+y'=(x+y)'),
(∀x)(x.0=0),
(∀x)(∀y)(x.y'=x.y+x)
∴
(x+y)+z=x+(y+z)

Theorem 10

(∀x)(∀y)(x'=y'⊃x=y),
(∀x)~(x'=0),
(∀x)(x+0=x),
(∀x)(∀y)(x+y'=(x+y)'),
(∀x)(x.0=0),
(∀x)(∀y)(x.y'=x.y+x)
∴
0.x=0

---