On 12/08/2013 8:23 AM, Ben Bacarisse wrote: > Peter Percival <firstname.lastname@example.org> 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,
It actually doesn't mean that; "even1", "even1", "even" are what Shoenfield termed as "defined symbols": they are eliminated-able by the actual language symbols [of L(PA)]. So there's _nothing wrong_ with those 3 definitions.
>>> or does it mean that the author is inclined to use overly >>> complex definitions?
Not "inclined" at all. In fact it was _deliberately_ on my part to define the even function (or the like) in this overly complex manner, _for a good reason_ : it highlighted the expression-duality of even numbers, in that they can be expressed _either_ inductively (Def-03a) or non-inductively (Def-03b).
This inductive and non-inductive expression duality was used in other definitions (Def-07a and Def-07a, for "There are infinitely many examples of property P"), and plays a key role in my proof about certain structure theoretical truth-impossibility. The other posters (fom, e.g.) didn't recognize that but, to answer your question, it was _NOT_ an accidence the these kind of definitions were done that complex way.
>>> 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.
Yes it was an overlook on my part then (the same with my definition of primes), but that would take only a simple fix (which I indicated before somewhere it will be done in the next formal presentation.
No consequence to my overall proof though. > > 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. >
-- ----------------------------------------------------- There is no remainder in the mathematics of infinity.