| |||
---|---|---|---|

78.3 | 117 | ||

78.4 | 122 | ||

78.5 | 90 | ||

78.6 | 107 | ||

¬zP0 | 108 | ||

Induction 1 | 123 | ||

The basic fact about the weak ancestral | 134,136 | ||

The lemma | 141 | ||

Induction 2 | 144 | ||

(5′) | 145 | ||

(4′) | α149 | ||

(1′) | 150 | ||

Induction 3 | 152 | ||

(2) | 154 | ||

(0′) | 155 |

**APPENDIX 2. INTERPRETING FREGE ARITHMETIC**

IN SECOND-ORDER ARITHMETIC

IN SECOND-ORDER ARITHMETIC

The language (of second-order arithmetic) contains variables x, y, z, . . . over natural numbers; variables α, β, γ, . . . over sets of numbers; and variables ρ, Ϛ, . . . . over binary relations of numbers. (We do not need variables over n-place relations for n>2.) Its non-logical symbols are 0, s, +, ×, >. Terms t are built up out of 0, s, +, × as usual; the atomic formulas are t=t′, t>t′, αt, ρtt′; formulas are then built up as usual.

The axioms of second-order arithmetic are induction: (α0 ∧ ∀x(αx → αsx) → αx) [a single formula]; the recursion axioms for successor, plus and times and the definition of less-than:

0≠sx, sx=sy → x=y, x+0 = x, x+sy = s(x+y), x×0 = 0,

x×sy = (x×y)+x, x

and the comprehension axioms (which are axioms of standard second-order logic):

∃α∀x(αx ↔ A), ∃ρ∀x∀y(ρxy ↔ B), A a formula in which α is not free and B a formula in which p is not free.

Since we have + and ×, we could have dispensed with binary relation variables; and since we have binary relation variables, we could have dispensed with + and × and set variables:

J, = λxyιz(x^{2} +2xy+y^{2} +3x+y = 2z), is an onto pairing function.

Thus if we have + and ×, we have J, and so we can replace ρtt′ by αJ (t,t′). And we can define x+y = z and x×y = z from 0 and s using binary relation variables: x+y = z

-424-