Search All of the Math Forum:

Views expressed in these public forums are not endorsed by NCTM or The Math Forum.

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

Topic: A finite set of all naturals
Replies: 32   Last Post: Aug 15, 2013 4:07 PM

 Messages: [ Previous | Next ]
 fom Posts: 1,968 Registered: 12/4/12
Re: A finite set of all naturals
Posted: Aug 12, 2013 8:17 PM

On 8/12/2013 6:04 AM, Ben Bacarisse wrote:
> fom <fomJUNK@nyms.net> writes:
> <snip>

>> Here is the proof he provides when pressed to produce:
>>

>
> I could not resist taking just a little peek...

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,

Ap1[prime(p1) -> Ap2[prime(p2) -> [(p1+p2<x \/ x<p1+p2)]

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

aGC(0)

aGC(1)

aGC(2)

hold.

Suppose the antecedent fails because ~even(x) holds. Then,
presumably odd(x) holds (although I have not proved this
from Nam's definitions).

Consider prime pairs. One has, for example,

2 + 3 = 5

So

(2+3<5 \/ 5<2+3)

does not hold. Since 3 is prime,

prime(3)

holds. so

prime(3) -> (2+3<5 \/ 5<2+3)

does not hold and

Ap2[prime(p2) -> (2+p2<5 \/ 5<2+p2)]

does not hold. Similarly,

Ap1[prime(p1) -> Ap2[prime(p2) -> (p1+p2<5 \/ 5<p1+p2)]

does not hold. So, since both the antecedent and the
consequent fail, the conditional holds. Therefore, for
the example,

aGC(5)

holds.

Since the given analysis should apply to every prime pair,
one should have

aGC(x) = {0, 1, 2} union {x | prime(x) /\ Ey[prime(y) /\ x=y+2]} union
{x | (even(x) /\ (SS0<x)) /\ Ap1[prime(p1) -> Ap2[prime(p2) -> [(p1+p2<x
\/ x<p1+p2)]}

Given my recent lack of practice, I have probably made a mistake
here.

But, the important thing is how one must remember that one must
interpret Nam's incorrect definitions so that they make sense
with respect to his claims.

Suppose you actually consider his definition as given.

Then since, as you observed,

Ap1p2[prime(p1) /\ prime(p2) /\ (p1+p2<x \/ x<p1+p2)]

cannot hold, the conditional is true whenever

(even(x) /\ (SS0<x))

does not hold. Hence,

aGC(x) = {0, 1, 2} union {x | odd(x)}

Once again, perhaps I have made some mistake.

Yet, since you have motivated me to actually make sense
of his definition of aGC(x) to the best of my ability,
the question is whether or not I can resist seeing how
he actually uses it.

chuckle

Date Subject Author
8/12/13 Ben Bacarisse
8/12/13 Peter Percival
8/12/13 fom
8/12/13 Ben Bacarisse
8/12/13 namducnguyen
8/12/13 namducnguyen
8/12/13 antani
8/12/13 namducnguyen
8/13/13 Marshall
8/13/13 quasi
8/13/13 namducnguyen
8/13/13 quasi
8/13/13 namducnguyen
8/13/13 namducnguyen
8/13/13 quasi
8/13/13 namducnguyen
8/14/13 quasi
8/14/13 namducnguyen
8/14/13 quasi
8/14/13 namducnguyen
8/15/13 namducnguyen
8/15/13 Virgil
8/15/13 namducnguyen
8/15/13 antani
8/13/13 antani
8/13/13 Peter Percival
8/13/13 Ben Bacarisse
8/13/13 namducnguyen
8/14/13 Peter Percival
8/14/13 Shmuel (Seymour J.) Metz