what to do about the Successor axiom once it reaches 999....9999#318; Correcting Math
in [Logic]
|
From: Nam Nguyen on 29 Jan 2010 17:24 Jesse F. Hughes wrote: > Nam Nguyen <namducnguyen(a)shaw.ca> writes: > >> Jesse F. Hughes wrote: >>> "Jesse F. Hughes" <jesse(a)phiwumbda.org> writes: >>> >>>> In either case, the axiom becomes: >>>> >>>> (Ax)(S(x) -> ~ x = 0) >>> What an utterly silly way to write ~S(0)! >>> >> How would you transform Ax[~S(x) = 0], written in L, into a formula, >> written in L', and yet still expressing the same semantics? >> >> Why don't you try. > > I think you misunderstood my comment. I was mocking my own > translation. Sorry. I overreacted in this case. > I wrote > > (Ax)(S(x) -> ~ x = 0), > > which is just an overly complicated way of writing > > ~S(0). > > In any case, I *did* indicate how to express that axiom (using either > of the above two formulas). However, I defined S(x) to hold whenever > x *is* a successor for some y, rather than x *has* a successor. Thus, > > S(x) <-> (Ey)( y < x & (Az)(z < x -> z <= y) ). > > With S thus defined, then > > ~S(0) > > expresses that 0 is not a successor. Thanks. Let me dwell into it (your formula) to see how I could use it, for my purposes.
From: Nam Nguyen on 29 Jan 2010 17:30 Nam Nguyen wrote: > Jesse F. Hughes wrote: >> Nam Nguyen <namducnguyen(a)shaw.ca> writes: >> >>> Jesse F. Hughes wrote: >>>> "Jesse F. Hughes" <jesse(a)phiwumbda.org> writes: >>>> >>>>> In either case, the axiom becomes: >>>>> (Ax)(S(x) -> ~ x = 0) >>>> What an utterly silly way to write ~S(0)! >>>> >>> How would you transform Ax[~S(x) = 0], written in L, into a formula, >>> written in L', and yet still expressing the same semantics? >>> >>> Why don't you try. >> >> I think you misunderstood my comment. I was mocking my own >> translation. > > Sorry. I overreacted in this case. > > >> I wrote >> >> (Ax)(S(x) -> ~ x = 0), >> >> which is just an overly complicated way of writing >> >> ~S(0). >> >> In any case, I *did* indicate how to express that axiom (using either >> of the above two formulas). However, I defined S(x) to hold whenever >> x *is* a successor for some y, rather than x *has* a successor. Thus, >> >> S(x) <-> (Ey)( y < x & (Az)(z < x -> z <= y) ). >> >> With S thus defined, then >> >> ~S(0) >> expresses that 0 is not a successor. > > Thanks. Let me dwell into it (your formula) to see how I could use it, for > my purposes. 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.
From: Nam Nguyen on 29 Jan 2010 19:48 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. [Speaking for myself, many times I thought I had some intuitions but they turned out to be incorrect; I actually felt "ashame" to what I had written in some files saved in my computer. Though I'd tend to believe if one ventures into an area for a long time then it's possible that one might just happen to be more familiar to with the terrain, so to speak. Which could be expected of anyone else.] Any rate, in real numbers, a "summation" could be defined as a _convergence_: x = y1 + y2 + y3 +.... So I'd think if in L' we could define "Convergence", "Finite", "Sequence" or the like then the property Sum(x,y,z), meaning the concept of z being the sum of x and y, could be defined. Again, this perceived "road map" is still sketchy.
From: Nam Nguyen on 30 Jan 2010 15:00 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.
From: Nam Nguyen on 30 Jan 2010 16:11
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 seems to expose some element of circularity in Godel's work.] |