what to do about the Successor axiom once it reaches 999....9999#318; Correcting Math
in [Logic]
|
From: Nam Nguyen on 31 Jan 2010 17:52 Jesse F. Hughes wrote: > Nam Nguyen <namducnguyen(a)shaw.ca> writes: > >> Nam Nguyen wrote: >>> Nam Nguyen wrote: >>>> Here is my attempt: basically summation of x and y would be defined as >>>> the >>>> minimal _common_ upper bound of both x and y. >>>> >>>> Definition1: >>>> ============ >>>> >>>> Sum(x,y,z) <-> l.u.b(x,y,z) >>>> l.u.b(x,y,z) <-> cLim(x,y,z) /\ Az'[cLim(x,y,z') -> (z=z')] >>>> cLim(x,y,z) <-> lim(x,z) /\ lim(y,z) >>>> limt(x,y) <-> (x <= y) >>>> >>>> It looks less complicated than I feared, but would this seem a >>>> _reasonable_ >>>> definition? Thanks. >>> There are a typo and a desired simplification in my above. So the >>> following is >>> a slightly different rendition of the same idea: >>> >>> Sum(x,y,z) <-> cLim(x,y,z) /\ Az'[cLim(x,y,z') -> (z=z')] >>> cLim(x,y,z) <-> lim(x,z) /\ lim(y,z) >>> lim(x,y) <-> (x <= y) >>> >> Also I had: >> >> >> define as the minimal _common_ upper bound of both x and y. >> >> It should have been something like: >> >> "defined as _a kind_ of minimal common upper bound of both x and y." >> >> for better clarity on the English phrasing. > > > Yes, but in N with < defined as usual, the minimal common upper bound > of x and y is simply max{x,y}. > > (Note as well that your definitions above don't do what you want, > namely to specify that z is the max of x and y, as I pointed out in an > earlier post.) > First, I don't think we have to dwell too much on the English meanings of "cLim" and "lim": they're *just names*. Secondly, I already gave a clarification that involves "something like" and "as _a kind_ of", so I don't believe there's any harm to to the definition of Sum(x,y,z). (Notwidstanding the fact you had a intention for better clarity here). In other words, the most crucial question here isn't about the "max"- definition but about if we eliminate cLim and lim by what appear on their corresponding right sides of the '<->', would we see that z be the sum of x and y, as expressed in L'?
From: Nam Nguyen on 31 Jan 2010 18:46 Nam Nguyen wrote: > There are a typo and a desired simplification in my above. So the > following is a slightly different rendition of the same idea: > > Sum(x,y,z) <-> cLim(x,y,z) /\ Az'[cLim(x,y,z') -> (z=z')] > cLim(x,y,z) <-> lim(x,z) /\ lim(y,z) > lim(x,y) <-> (x <= y) > As mentioned previously, let's now use what we've had so far and express GC in L' = L'(0,*,<): GC <-> AxEp1p2[even(x) -> (prime(p1) /\ prime(p2) /\ Sum(p1,p2,x))] even(x) <-> Eyy'[2(y) /\ x=y*y'] 2(x) <-> Ey[1(y) & (y Lnext x)] 1(x) <-> Ay[y = x*y] x Lnext y <-> (x < y) & Az[(z < y) -> (y=z)] prime(x) <-> Ayz[(x=y*z) -> ((1(y) /\ x=z) \/ (1(z) /\ x=y))] It's possible some fine, detailed technical errors might exist, but I think the translation of GC from L = L(0,S,+,*,<) to L' has taken place.
From: Nam Nguyen on 31 Jan 2010 18:57 Nam Nguyen wrote: > Nam Nguyen wrote: > >> There are a typo and a desired simplification in my above. So the >> following is a slightly different rendition of the same idea: >> >> Sum(x,y,z) <-> cLim(x,y,z) /\ Az'[cLim(x,y,z') -> (z=z')] >> cLim(x,y,z) <-> lim(x,z) /\ lim(y,z) >> lim(x,y) <-> (x <= y) >> > > As mentioned previously, let's now use what we've had so far and express > GC in L' = L'(0,*,<): > > GC <-> AxEp1p2[even(x) -> (prime(p1) /\ prime(p2) /\ Sum(p1,p2,x))] > even(x) <-> Eyy'[2(y) /\ x=y*y'] > 2(x) <-> Ey[1(y) & (y Lnext x)] > 1(x) <-> Ay[y = x*y] > x Lnext y <-> (x < y) & Az[(z < y) -> (y=z)] > prime(x) <-> Ayz[(x=y*z) -> ((1(y) /\ x=z) \/ (1(z) /\ x=y))] > > It's possible some fine, detailed technical errors might exist, but I > think the translation of GC from L = L(0,S,+,*,<) to L' has taken place. Of course the actual GC would have '4' appearing in it, but we could also, in L', define 3(x), 4(x) in a manner similar to 1(x) and 2(x).
From: Nam Nguyen on 31 Jan 2010 19:46 Jesse F. Hughes wrote: > Nam Nguyen <namducnguyen(a)shaw.ca> writes: > >> Nam Nguyen wrote: >> >>> There are a typo and a desired simplification in my above. So the >>> following is a slightly different rendition of the same idea: >>> >>> Sum(x,y,z) <-> cLim(x,y,z) /\ Az'[cLim(x,y,z') -> (z=z')] >>> cLim(x,y,z) <-> lim(x,z) /\ lim(y,z) >>> lim(x,y) <-> (x <= y) >>> >> As mentioned previously, let's now use what we've had so far and express >> GC in L' = L'(0,*,<): >> >> GC <-> AxEp1p2[even(x) -> (prime(p1) /\ prime(p2) /\ Sum(p1,p2,x))] >> even(x) <-> Eyy'[2(y) /\ x=y*y'] >> 2(x) <-> Ey[1(y) & (y Lnext x)] >> 1(x) <-> Ay[y = x*y] >> x Lnext y <-> (x < y) & Az[(z < y) -> (y=z)] >> prime(x) <-> Ayz[(x=y*z) -> ((1(y) /\ x=z) \/ (1(z) /\ x=y))] >> >> It's possible some fine, detailed technical errors might exist, but I >> think the translation of GC from L = L(0,S,+,*,<) to L' has taken >> place. > > No. You have not even defined Sum(x,y,z) correctly. (Though I'm > curious why you take multiplication as primitive in L' and not > addition.) Because the primes can be defined in this "lesser" L', and primes are crucial properties of arithmetic. Ultimately I'd like to demonstrate that another "lesser" language could be a new "the"-language-of-arithmetic. > > At least I don't consider it a "fine, detailed technical error" when > > (Axyz)~Sum(x,y,z) > > is a theorem. Perhaps you disagree. > > Your Lnext predicate is evidently broken, too. I'm not sure what you > wanted (x Lnext y) to mean. Perhaps you wanted it to mean x + 1 = y. > If so, try: > > x Lnext y <-> x < y & (Az)(x < z -> y <= z). > > As it is, we can prove (Ax)(Ay)~x Lnext y, since > > x Lnext y -> (x < y & x = y). > > (Hint: instantiate the universal with x to get x < y -> y = x.) > Thanks for the information and the hints. I'll review all that.
From: Nam Nguyen on 1 Feb 2010 20:23
Nam Nguyen wrote: > Jesse F. Hughes wrote: >>> Nam Nguyen wrote: >>> >>>> There are a typo and a desired simplification in my above. So the >>>> following is a slightly different rendition of the same idea: >>>> >>>> Sum(x,y,z) <-> cLim(x,y,z) /\ Az'[cLim(x,y,z') -> (z=z')] >>>> cLim(x,y,z) <-> lim(x,z) /\ lim(y,z) >>>> lim(x,y) <-> (x <= y) >>>> >> No. You have not even defined Sum(x,y,z) correctly. (Though I'm >> curious why you take multiplication as primitive in L' and not >> addition.) > > Thanks for the information and the hints. I'll review all that. I think you're right about having little faith in expressing arithmetic completely without '+'. Reviewing my purposes, however, I think I also chose the wrong _lesser_ language to express some arithmetic concepts (e.g. GC). I should have chosen L'' = L''(0,+,*,<). I'll into L'' more. |