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
-- Nam Nguyen in sci.logic in the thread 'Q on incompleteness proof' on 16/07/2013 at 02:16: "there can be such a group where informally it's impossible to know the truth value of the abelian expression Axy[x + y = y + x]".