0.1. Notes on Arithmetic

Peano Arithmetic is a formal theory, kind of “applied logic”, that talks about the behaviour of our familiar objects—the natural numbers 0, 1, 2, …—and the operations and relations on them formally. That is, purely syntactically, without mixing “expectations” with what has been actually assumed (axioms).

Of course, expectations lead us to the appropriate choice of axioms, but once the choice has been effected, the expectations are put aside, and give way to formal proving.

This “formal proving” is supposed to help us discover true statements about the “real” objects that our axiomatic system simulates. Soundness of all first order theories, and the fact that the “natural interpretation” of our axioms is valid over ℕ, guarantee that we will never prove any invalid formulas.

A celebrated theorem by Gödel, however, says that we cannot prove all true statements about the natural numbers, no matter how we axiomatize their behaviour in a “practical system”.^{∗}

The nonlogical symbols are the following

1. “0” When interpreted naturally, it means “zero”.

2. “S” When interpreted naturally, it means “+1”, the successor function of one variable (i.e., S(x) or more simply Sx is interpreted as x + 1).

3. “+” When interpreted naturally, it means “+”, the “plus” function of two variables (i.e., the formal x + y is interpreted as the “real” or informal x + y).

4. “·” When interpreted naturally, it means “·”, the “times” function of two variables (i.e., the formal x·y is interpreted as the “real” or informal x·y).

5. “<” When interpreted naturally, it means “<”, the “less than” relation of two variables (i.e., the formal x < y is interpreted as the “real” or informal x < y).

What about “1”, “2”? What about ≤ and other things? Like exponentiation, etc? All these “other” things can be introduced definitionally. For example we can write S0 and SS0 as the formal counterparts of the real (i.e., whatever we, philosophically, think are really the numbers) 1 and 2 respectively. Formal abbreviations for S0 and SS0 are ˜1 and ˜2 respectively. Similarly, we write (formally) ñ as short for

\overbrace{S … S}^{n copies} 0

∗A system of axioms is “practical” if we can tell in a finite number of steps whether a formula is an axiom or not. For example, our logical axioms Ax1–Ax6 are “practical”. Even though Ax1 contains infinitely many formulas, we can certainly test in a finite number of steps whether or not a formula is a partial generalization of a tautology.

Note that due to a theorem of Church we cannot take all formulas that are valid in ℕ as axioms, for this system, he proved, is not practical.

Of course this interprets naturally as the “real” natural number “n”.

We are not going to use this rigid notation in Ch.12. Only at the beginning, briefly, so you can get a flavour of what formal arithmetic is really like. After that we will revert to the “quasi-formal-quasi-sloppy” text style (sigh …)

The axioms of Peano Arithmetic (PA) are the universal closures^{†} of the following:

(S)1. ¬0 = Sx

(S)2. Sx = Sy ⇒ x = y (“1-1ness of S”)

(+)1. x + 0 = x

(+)2. x + Sy = S(x + y)

(·)1. x · 0 = 0

(·)2. x · Sy = x · y + x

(<)1. ¬x < 0

(<)2. x < Sy ≡ x < y ∨ x = y

(<)3. x < y ∨ x = y ∨ y < x

And the Induction Schema, one axiom for each formula A:

(Ind)  A[x := 0] ∧ (∀x)(A ⇒ A[x := Sx]) ⇒ A

The totality of the above axioms (i.e., the universal closures of what I have just listed) are going to be denoted by “PA”.

If we keep all except (Ind) we have “Robinson’s Arithmetic”, in short, “ROB”.

Writing A[x] to indicate our interest in the free variable x of A^{‡} we rewrite (Ind) as follows:

(Ind′)  A[0] ∧ (∀x)(A[x] ⇒ A[Sx]) ⇒ A[x]

This yields, by modus ponens the derived rule of PA:

A[0] ∧ (∀x)(A[x] ⇒ A[Sx]) ⊢ A[x]

†If A is a formula, its universal closure is obtained by adding (∀x) in front of A for each free variable of A. The order of the various (∀x) is immaterial, since ⊢ (∀x)(∀y)A ≡ (∀y)(∀x)A.

‡Recall that x need not be actually free. Compare: We write in Calculus “f(x)” to indicate a function’s dependence of x. Maybe we can later prove that f′(x)—the derivative—equals 0 on an open interval (a, b). Then f(x) is constant on (a, b), i.e., it does not depend on x after all. This does not stop us from writing “f(x)” nevertheless.

Notes on Induction\begin{matrix}c \\ ◯ \end{matrix} by George Tourlakis

or, separating the premises^{§}

(Ind′′)  A[0], (∀x)(A[x] ⇒ A[Sx]) ⊢ A[x]

The above is pretty close to the “practical” induction “protocol”. A few more simplifications and we get to that: Note what (Ind′′) offers us:

To prove

PA ⊢ A[x]  (1)

or, equivalently,

PA ⊢ (∀x)A[x]  (2)

since PA consists of closed formulas, it suffices to do instead

(a) PA ⊢ A[0]

and

(b) PA ⊢ (∀x)(A[x] ⇒ A[Sx])

However, to do (b) we only need do \underline{simply}

PA ⊢ A[x] ⇒ A[Sx]

We then get (b) by generalization! We can get away with this because our “Γ ” here is PA, and we have ensured that it has no free variables. Thus, our “practical induction protocol” is the following RULE:

(Ind-rule)  A[0], A[x] ⇒ A[Sx] ⊢ A[x]

which is implemented (used) in practice, via the Deduction theorem, as follows:

(I) PA ⊢ A[0]. This is the Basis.

and

(II) Add A[x] to PA as a new axiom (“auxiliary” or “temporary axiom”). This is the Induction Hypothesis, or “I.H.”

(III) The “GoTo step” (goto “Sx”, or goto “x + 1”): Do

PA, A[x] ⊢ A[Sx]

Jargon When we prove PA ⊢ (∀x)A[x] by induction, or—as we often omit the “(∀x)”—PA ⊢ A[x], we say that \underline{we do induction on x}.

Let us sample a couple of applications that do not murky the waters by assuming things we never assumed (such as summations, for example).

§Legitimate by the tautological implications P ∧Q ⊧_{taut} P, P ∧Q ⊧_{taut} Q and P, Q ⊧_{taut} P ∧ Q.

Notes on Induction\begin{matrix}c \\ ◯ \end{matrix} by George Tourlakis

0.1.1 Example. We prove PA ⊢ 0 ≤ x by induction on x.

First off, “≤” is a defined symbol introduced by

x ≤ y stands for x < y ∨ x = y

As we know from class such “stands for” definitions give rise to tautologies

x ≤ y ≡ x < y ∨ x = y

Onto our task. A[x] is 0 ≤ x.

Basis. I want PA ⊢ 0 ≤ 0.

0 ≤ 0

≡ ⟨Definition of ≤⟩ 0 < 0 ∧ 0 = 0

The last formula is an absolute theorem^{†} (PA not used), hence so is 0 ≤ 0. Add to PA the assumption A[x] (I.H.) Goto step (prove A[Sx]).

0 ≤ Sx

≡ ⟨Definition of ≤⟩ 0 < Sx ∨ 0 = Sx

≡ ⟨Leib. plus axiom “(<)2.”⟩ 0 < x ∨ 0 = x ∨ 0 = Sx

≡ ⟨Leib. plus def. of ≤⟩ 0 ≤ x ∨ 0 = Sx

The last line is a tautological consequence of I.H., so we are done. □

0.1.2 Example. We prove PA ⊢ x < y ∧ y < z ⇒ x < z by induction on z. That is, the formula “x < y ∧ y < z ⇒ x < z” is our “A[z]”. Basis. I want PA ⊢ x < y ∧ y < 0 ⇒ x < 0. This is a tautological

consequence of ¬y < 0 (axiom (<)1.)

Add to PA the assumption A[z] (I.H.)

†Specialization of axiom (∀z)(z = z), followed by tautological implication.

Notes on Induction\begin{matrix}c \\ ◯ \end{matrix} by George Tourlakis

Goto step (prove A[Sz]).

x < y ∧ y < Sz ⇒ x < Sz

≡ ⟨Leib. plus axiom (<)2.⟩

x < y ∧ (y < z ∨ y = z) ⇒ x < Sz

≡ ⟨Leib. plus tautology⟩

(x < y ∧ y < z) ∨ (x < y ∧ y = z) ⇒ x < Sz

≡ ⟨tautology⟩

(x < y ∧ y < z ⇒ x < Sz) ∧ (x < y ∧ y = z ⇒ x < Sz)

The last line is a theorem by I.H. and axiom (<)2, so we are done.

You believe this? Here:

(1) x < y ∧ y < z ⇒ x < z (The I.H.)

(2) x < z ⇒ x < z ∨ x = z (tautology)

(3) x < z ⇒ x < Sz (taut. impl. from (2) plus axiom (<)2.)

(4) x < y ∧ y < z ⇒ x < Sz ((1) plus (3) plus taut. impl.) This justifies the left conjunct. For the right conjunct, Ax6 tautologically yields ⊢ x < y ∧ y = z ⇒ x < z.

Now use (3) above to get x < y ∧ y = z ⇒ x < Sz by taut. implication. □

0.1.3 Example. (“Strong” or “course-of-values” induction)

We now \underline{derive} a useful induction principle (the one proposed up in front in GS) that goes by any of the above names. Its I.H. is “strong” and uses the “entire course of values (history)” of the induction variable. Naïvely, to prove P (n) (n of “type” ℕ) you assume (I.H.) the claim for all k < n. Helped by this you prove P (n). You then proclaim that you have proved P (n) for all n ∈ ℕ. Here is the formal reason why this technique is “correct”:

For every formula A[x],

PA ⊢ (∀x)((∀z < x)A[z] ⇒ A[x]) ⇒ (∀x)A[x]  (CV I)

We have used the “bounded quantification” abbreviation above that is very common in the literature: We wrote “(∀z < x)A[z]” for “(∀z)(z < x ⇒ A[z])”.

To prove (CV I) (for any given formula A) we will employ the Deduction theorem to eliminate the rightmost ⇒.

Thus, we \underline{add (∀x)((∀z < x)A[z] ⇒ A[x]) to PA.}  (0)

Next, we \underline{name} the formula

(∀z < x)A[z]  (1)

by the short name B[x].

Plan: Prove PA ⊢ (∀x)B[x]. We use induction on x.

Basis. Do PA ⊢ B[0]. By (1), do

PA ⊢ (∀z)(z < 0 ⇒ A[z])

We calculate this here:

(∀z)(z < 0 ⇒ A[z]) ≡ ⟨axiom (<)1., redundant true, and sWLUS⟩

(∀z)(false ⇒ A[z])

The last formula is in Ax1.

With the basis out of the way, \underline{add to PA the assumption B[x].} (I.H.)

For future use: (0) above, via specialization, yields

B[x] ⇒ A[x]  (2)

Goto step. (Prove B[Sx])

(∀z)(z < Sx ⇒ A[z])

≡ ⟨axiom (<)2. and sWLUS⟩ (∀z)(z < x ∨ z = x ⇒ A[z]) ≡ ⟨WLUS and obvious tautology⟩

(∀z)((z < x ⇒ A[z]) ∧ (z = x ⇒ A[z]))

≡ ⟨distr. ∀ over ∧⟩

(∀z)(z < x ⇒ A[z]) ∧ (∀z)(z = x ⇒ A[z]) ≡ ⟨Leib. plus 1-point-rule⟩

B[x] ∧ A[x]

The last line is a theorem, because B[x] is (I.H.), and hence so is A[x] by (2) and MP.

We now have that PA \underline{along with our first underlined assumption} (the one just above (1)) proves

(∀x)B[x]

By ∀-monotonicity and (2),

(∀x)A[x]

By the Deduction theorem we are done! □

0.1.4 Example. (Practicalities of (CV I)) We employ “strong” induction like this: To prove PA ⊢ (∀x)A[x] just do the following two things.

1. Assume (∀z)(z < x ⇒ A[z]). This is the I.H. We also say it informally: “Assume that, for all z < x, A[z] holds”.

2. Prove, using PA \underline{and} the I.H., A[x]. This is the Goto step.

Indeed, steps 1. and 2. yield

PA ⊢ (∀z)(z < x ⇒ A[z]) ⇒ A[x]

by Deduction theorem. Since all the axioms of PA are closed, generalization is allowed and gives

PA ⊢ (∀x)((∀z)(z < x ⇒ A[z]) ⇒ A[x])  (3)

Since (CV I) is a PA theorem by our work in Example 0.1.3, PA ⊢ (∀x)A[x] by (3) and modus ponens. □

0.1.5 Example. (Hey! What about the basis?) The basis in (CV I) is part of the Goto step. Here’s why: There is one case where the “Goto step” is not helped by the I.H. in 1. of the above example (0.1.4). That is when PA can \underline{prove} the I.H. In that case we prove A[x] \underline{just from PA} for our “assumption” (I.H.) is a PA-theorem anyway—that is, it is not an additional assumption. So, when does this happen? That is if x = 0: Then z < 0 ⇒ A[z] equivales to true in PA, since z < 0 equivales to false in PA by the first <-axiom. Thus we have to prove A[0] from scratch.

In plain English (informally), since there is no z to the left of 0 in ℕ, there is no hypothesis “for all z < 0, A[z] holds” to use when proving A[0]. The moral is: “You cannot escape from the Basis”. □

Both simple induction and CVI can be used to prove statements such as (∀n ≥

n_{0})A[n], where n_{0} is a fixed positive number.

The two recipes are respectively:

(1) Simple: Do

(i) Verify A[n_{0}] (Basis)

(ii) Assume A[n] (for n ≥ n_{0})—this is the I.H.

(iii) Prove that A[n + 1] (for n + 1 ≥ n_{0})—this is the “goto step”.

(2) CVI: Do

(a) Assume that A[m] holds for all m such that n > m ≥ n_{0}—this is the I.H.

(b) Prove that A[n] holds, ensuring that your argument is good for any n ≥ n_{0}— this is the “goto step”.

Note that doing (b) above you have to directly verify A[n_{0}] because the I.H. is true and thus it does not help when you want to prove true ⇒ A[n_{0}].^{¶} We say that \underline{n = n_{0} is the boundary case}.

0.1.6 Example. Here we show the CVI in action. However, we retreat to informal mathematics, where we assume a lot. In particular we assume that we know what a prime is and that a factor of a factor of n ∈ ℕ is a factor of n.^{∥} Moreover, we will carry out the proof informally.

We want to prove:

Every n ≥ 2 has a prime factor  (1)

Following the recipe (a)–(b) above 1) I.H. Assume that if 2 ≤ m < n then m has a prime divisor.

2) Now prove that n ≥ 2 has a prime divisor.

There are two cases:

Case I. (The boundary case) If n = 2, then we are done: 2 has a prime factor, itself, since 2 = 2 · 1.

Case II. n > 2. Well, if n is prime we are done—just write n = n · 1. If on the other hand it is composite, then n = a · b where a > 1 and b > 1. But a > 1 says a ≥ 2. Thus n > a ≥ 2 and the I.H. applies to a. That is, a has a prime factor. But any prime factor of a is a prime factor of n. Done.

□

¶The hypothesis is “for all m such that n_{0} > m ≥ n_{0}, A[n_{0}] holds” or, in symbols, n_{0} > m ≥ n_{0} ⇒ A[n_{0}]. But n_{0} > m ≥ n_{0} equivales to false.

∥Well, OK: We are in ℕ. A factor or divisor of n is an m such that (∃x)n = m·x, where “We are in ℕ” means that whenever you write “(∃x) …” or “(∀x) …” you mean “(∃x ∈ ℕ) …” and “(∀x ∈ ℕ) …” respectively. Note that if (∃y)m = d·y as well then (∃y)m = d·y∧(∃x)n = m·x, which is equivalent to (∃y)(∃x)(m = d · y ∧ n = m · x) (you believe this?), hence (Ax6 and ∃-monotonicity), (∃y)(∃x)(n = d · y · x), thus (∃z)n = d · z. d is a factor of n. Now, n is a prime if it is > 1 and all its factors are n and 1.

Notes on Induction\begin{matrix}c \\ ◯ \end{matrix} by George Tourlakis