Please accept my apologies. You should have resisted.
> 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. >
After arriving at a similar emotional state, I went looking for the alleged proof and only looked for definitions relevant to its analysis...
> Maybe I don't understand the notation,
Does anyone? You are not alone.
But, I am not one to speak. My own statements seem to puzzle others.
> 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? >
Nam probably wanted restricted quantifications in this definition,
Then, the apparent intent would be that aGC(x) holds if every sum of primes is different from x.
So, suppose aGC(x) holds.
Then, if (even(x) /\ (SS0<x)), the apparent intent would be realized for x.
Suppose the antecedent fails because (SS0>=x). Then doesn't x<(p1+p2) hold for all (correctly) defined primes? The antecedent fails, but the consequent does not. So, the conditional would appear to hold. If I am correct in this, then
Suppose the antecedent fails because ~even(x) holds. Then, presumably odd(x) holds (although I have not proved this from Nam's definitions).