what to do about the Successor axiom once it reaches 999....9999#318; Correcting Math
in [Logic]
|
From: Nam Nguyen on 30 Jan 2010 19:36 Nam Nguyen wrote: > Jesse F. Hughes wrote: >> Nam Nguyen <namducnguyen(a)shaw.ca> writes: >> >>> Imho, the next battle in completely replacing L-formulas having '+' >>> by L'-formulas would be "brutal" and "uglier". But for what it's >>> worth I have some faith. >> >> Well, I have much less faith in that step, but I don't have good >> intuitions here. > > Not 100% sure but I think I've found a solution, albeit it's somewhat > "cheating". > > The both '<' and ZF's 'e' are 2-nary symbols so we'd translate L-formulas > into L(ZF), and then transform them further to L' by replacing 'e' by '<' > > It'd still be "horrible" formulas to look at in the end, but we know > for sure, thanks to ZF, the translation/transformation is syntactically > possible. As for semantics, being a member of a set x could be > interpreted as being "less-than" - at least in part-hood (mereology) > sense. > > Would this "solution" work? Thanks again. This solution wouldn't work as-is. There's transitivity with the "less-than" semantic for '<' but there isn't for the "epsilon" semantic, hence the 2 semantics aren't the same. I'll stick with my original plan, using the fact that although we might not have an n-ary symbol (e.g. we don't have '+' in L') we still could define an n-ary relation using what we already have in the underlying language (L' in this case).
From: Nam Nguyen on 31 Jan 2010 11:15 Nam Nguyen wrote: > Nam Nguyen wrote: >> Jesse F. Hughes wrote: >>> Nam Nguyen <namducnguyen(a)shaw.ca> writes: >>> >>>> Imho, the next battle in completely replacing L-formulas having '+' >>>> by L'-formulas would be "brutal" and "uglier". But for what it's >>>> worth I have some faith. >>> >>> Well, I have much less faith in that step, but I don't have good >>> intuitions here. >> >> Not 100% sure but I think I've found a solution, albeit it's somewhat >> "cheating". >> >> The both '<' and ZF's 'e' are 2-nary symbols so we'd translate L-formulas >> into L(ZF), and then transform them further to L' by replacing 'e' by '<' >> >> It'd still be "horrible" formulas to look at in the end, but we know >> for sure, thanks to ZF, the translation/transformation is syntactically >> possible. As for semantics, being a member of a set x could be >> interpreted as being "less-than" - at least in part-hood (mereology) >> sense. >> >> Would this "solution" work? Thanks again. > > This solution wouldn't work as-is. There's transitivity with the > "less-than" > semantic for '<' but there isn't for the "epsilon" semantic, hence the 2 > semantics aren't the same. > > I'll stick with my original plan, using the fact that although we might > not have an n-ary symbol (e.g. we don't have '+' in L') we still could > define an n-ary relation using what we already have in the underlying > language (L' in this case). > 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.
From: Nam Nguyen on 31 Jan 2010 11:34 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)
From: Nam Nguyen on 31 Jan 2010 11:43 Jesse F. Hughes wrote: > Nam Nguyen <namducnguyen(a)shaw.ca> writes: > >> 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. > > First, the minimal common upper bound of both x and y is max(x,y), not > x + y. > > Second, your definition of lub doesn't work, though it is easy enough > to define lub correctly. Seems to me that I can prove > > (Ax)(Ay)(Az)~lub(x,y,z). > > Let x and y be given and let z be any number such that cLim(x,y,z) and > let z' = z + 1. Then > > cLim(x,y,z') & ~ z = z'. > > Thus, ~lub(x,y,z). > > The proper way to define lub(x,y,z) is > > x <= z & y <= z & (Az')( (x <= z' & y <= z') -> z <= z' ) > > Again, all of this is a bit irrelevant, since the lub of {x,y} is > *not* x + y. > I think the name "l.u.b" is a bit confusing in this context, so I've left it out my revised definition in a recent post.
From: Nam Nguyen on 31 Jan 2010 11:57
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. |