This is a file in the archives of the Stanford Encyclopedia of Philosophy. |
HerOn(Q,The proof of this claim appeals to the following Lemma (cf. Gg I, Theorem 149):)
Lemma on Predecessor+:Intuitively, the Lemma on Predecessor+ tells us that if y precedes a number x, then #[
x & Precedes(y,x)
![]()
#[z Precedes+(z,y)] = #[
z Precedes+(z,x) & z
x]
Now to show HerOn(Q,), we have to
show:
If we replace Q with its definition and simplify the result byn
m[Precedes(n,m)
(Qn
Qm)]
(Intuitively, we have to show that if n precedes m, then if n precedes the number of numbers less than or equal to n, then m precedes the number of numbers less than or equal to m.) So, letting n and m be arbitrary, we assume both:n
m(Precedes(n,m)
![]()
Precedes(n,#[z Precedes+(z,n)])
Precedes(m,#[
z Precedes+(z,m)])
(A) Precedes(n,m)to show:
(B) Precedes(n,#[z Precedes+(z,n)])
Precedes(m,#[By the definition of Predecessor, we have to show that there is a concept F and object x such that:z Precedes+(z,m)])
(1) FxWe can demonstrate that there is an F and x for which (1), (2) and (3) hold if we pick F to be [
(2) #[z Precedes+(z,m)] = #F
(3) m = #[u Fu & u
x]
To show that (1) holds, we have to show:
[But we know, from the definition of Precedes+, that Precedes+(m,m). So by abstraction usingz Precedes+(z,m)]m
To show that (2) holds, we need do no work, since our choice of F requires us to show:
#[which we know by the logic of identity.z Precedes+(z,m)] = #[
z Precedes+(z,m)],
To show (3) holds, we need to show:
(C) m = #[[Note that theu Precedes+(u,m) & u
m]
[In what follows, we use the simplified version of thisu [
z Precedes+(z,m)]u & u
m]
Now in virtue of (A), (B) and the functionality of Predecessor (the
proof of which was left as an exercise in the subsection No Two
Numbers Have the Same Successor in §5), we know m =
#[z
Precedes+(z,n)]. So, substituting
for m in (C), we have to show:
#[But we can demonstrate this by appealing to the Lemma on Predecessor+ mentioned at the outset. We may instantiate the variables x and y in this Lemma to m and n, respectively, yielding:z Precedes+(z,n)] = #[
u Precedes+(u,m) & u
m]
Since the consequence is what we had to show, we are done, for the conjuncts of the antecedent are things we assumed to be true at the beginning of our conditional proof.m & Precedes(n,m)
![]()
#[z Precedes+(z,n)] = #[
z Precedes+(z,m) & z
m]
Return to Frege's Logic, Theorem, and Foundations for Arithmetic
Edward N. Zalta zalta@stanford.edu |