
Re: A finite set of all naturals
Posted:
Aug 12, 2013 7:04 AM


fom <fomJUNK@nyms.net> writes: <snip> > Here is the proof he provides when pressed to produce: > > https://groups.google.com/d/msg/comp.ai.philosophy/AVnJgA5ZIk0/fk1sQQNSYVgJ
I could not resist taking just a little peek... That post claims to be "written in the language of arithmetic L(PA)" but it contains this definition early on:
Def03a: even1(x) <> Ey[x=y+y] Def03b: even2(x) <> Ey[x=2*y] Def03c: even(x) <> (even1(x) \/ even2(x))
Does this mean that Ax[even1(x)=even2(x)] is not a theorem of the system being used, or does it mean that the author is inclined to use overly complex definitions? Either way, I didn't find it an encouraging start.
Maybe I don't understand the notation, because just a few lines further on I see:
Def05c: aGC(x) <> (even(x) /\ (SS0<x)) > Ap1p2[prime(p1) /\ prime(p2) /\ (p1+p2<x \/ x<p1+p2)]
but isn't Ap1p2[prime(p1) /\ prime(p2) /\ (p1+p2<x \/ x<p1+p2)] simply false?
<snip>  Ben.

