what to do about the Successor axiom once it reaches 999....9999#318; Correcting Math
in [Logic]
|
From: Nam Nguyen on 29 Jan 2010 15:10 Nam Nguyen wrote: > Nam Nguyen wrote: >> Nam Nguyen wrote: >>> OK. One final thrust from me here on the topic before creating >>> a new thread that would involve a lot of semantics-definitions >>> and translations. >>> >>> We know L(PA) = L(0,S,+,<). Suppose then L' = L'(0,<,*), would >>> we be able to express GC strictly in L'? At least what would be a >>> road map? Any constructive idea would be appreciated. >> >> Sorry for the typo: of course L(PA) = L(0,S,+,*,<). > > OK, let me start. Basically the set of the 2-tuples for 'S' is a subset > of that for '<', meaning this subset could be defined strictly in term > of '0', '=', '<' and other logical symbols. Therefore in formulas > involving S, S could be eliminated. In addition, '+' can be defined in > term of 'S' and hence would also be eliminated-able. > > Would you think this road map is logically sound? An example would be defining, in L', the (successor) property S(x): S(x) <-> EyAz[(x<y) /\ ((z<y) -> (x=z))] Then the typical (axiom) formula in L: Ax[~(S(x)=0)] would be translated in L' as: ~(Ex[(x<0) /\ S(x)])
From: Nam Nguyen on 29 Jan 2010 16:14 Jesse F. Hughes wrote: > Nam Nguyen <namducnguyen(a)shaw.ca> writes: > >> An example would be defining, in L', the (successor) property S(x): >> >> S(x) <-> EyAz[(x<y) /\ ((z<y) -> (x=z))] > > Looks like you've come up with a formula which is true iff x = 0. I'm > not sure what you meant by "the successor property", but surely that > isn't it. > > A hint of what you meant is below. > >> Then the typical (axiom) formula in L: >> >> Ax[~(S(x)=0)] > > This formula is not well-formed, since S(x) is a formula and not a > function symbol. In L, S(x) is a term, not a formula. Let's remember that L = L(PA) = L(0,S,+,*,<).
From: Nam Nguyen on 29 Jan 2010 16:36 Jesse F. Hughes wrote: > > Sorry. For some reason, I snipped the remainder of your post when > replying, so I missed > >> would be translated in L' as: > >> ~(Ex[(x<0) /\ S(x)]) > > So you wanted S(x) to hold iff x = 0? What exactly did you want S(x) > to express? Well, in metal level and using English, I'd like for the property S(x), in L', to express the following semantics: "There exists an y such that if we extend L' into L then y is L-successor of x." or, to be independent from any reference to L: "There exists an y such that y is immediately next to x [in the direction opposite to less-than]." or something semantically the same.
From: Nam Nguyen on 29 Jan 2010 16:45 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.
From: Nam Nguyen on 29 Jan 2010 16:57
Nam Nguyen wrote: > 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. Btw, by many accounts, G(PA) is one heck of a "utterly silly" looking formula to write out, and yet somehow its semantics could also mean "consistency of PA"! |