Peter Percival <email@example.com> writes:
> Ben Bacarisse wrote: >> 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: >> >> Def-03a: even1(x) <-> Ey[x=y+y] >> Def-03b: even2(x) <-> Ey[x=2*y] >> Def-03c: 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: >> >> Def-05c: 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> > > Yes, since not every natural number is a prime, and a conjunct claims > otherwise, the whole is false. Perhaps > > Ap1p2[[prime(p1) /\ prime(p2)] -> (p1+p2<x \/ x<p1+p2)] > > was meant.
That was my guess too, but the reader shouldn't have to guess. For one thing, other errors, they may not be so obvious.
Since the post is more than a year old, these sort of issues may have been corrected, but it's a shame there is no TeX-formatted version (as you suggested) for easy reading. The journal will definitely want one.