Path: csiph.com!eternal-september.org!feeder.eternal-september.org!reader01.eternal-september.org!.POSTED!not-for-mail From: Keith Thompson Newsgroups: comp.theory,comp.ai.philosophy,comp.ai.nat-lang,sci.lang.semantics Subject: Re: Simply defining =?utf-8?Q?G=C3=B6del?= Incompleteness and Tarski Undefinability away V24 (Are we there yet?) Date: Thu, 16 Jul 2020 21:04:54 -0700 Organization: None to speak of Lines: 87 Message-ID: <87v9imyeft.fsf@nosuchdomain.example.com> References: <87365vnik3.fsf@bsb.me.uk> <87a703lz5c.fsf@bsb.me.uk> <87pn8ykrwq.fsf@bsb.me.uk> <7e-dnQpoj9jkoZPCnZ2dnUU7-UHNnZ2d@giganews.com> <875zapk0bb.fsf@bsb.me.uk> <87lfjkixu6.fsf@bsb.me.uk> <87eepc1cda.fsf@nosuchdomain.example.com> <87wo33z5fl.fsf@nosuchdomain.example.com> <2sKdndYwVpfsAo3CnZ2dnUU7-VfNnZ2d@giganews.com> <87lfjjz0du.fsf@nosuchdomain.example.com> Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit Injection-Info: reader02.eternal-september.org; posting-host="22913342158febd17ce42e5a39ff8077"; logging-data="10736"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18grOuajbwR2hdBEuj/sjNm" User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux) Cancel-Lock: sha1:K4syOg/FymufeINt5rZr0NcOsYg= sha1:TW6dPRpH9/F26rbw/jxAG4WIMQg= Xref: csiph.com comp.theory:21730 comp.ai.philosophy:22076 comp.ai.nat-lang:2451 olcott writes: > On 7/16/2020 3:10 PM, Keith Thompson wrote: >> olcott writes: >>> On 7/16/2020 1:21 PM, Keith Thompson wrote: >>>> olcott writes: >>>>> On 7/15/2020 8:23 PM, Keith Thompson wrote: >>>>>> olcott writes: >>>>>>> On 7/15/2020 12:32 PM, André G. Isaak wrote: >>>>>>>> On 2020-07-15 10:46, olcott wrote: >>>>>>>>> On 7/15/2020 10:48 AM, Ben Bacarisse wrote: >>>>>>>>>> A formula you've talked a lot about, namely, >>>>>>>>>> >>>>>>>>>>    ∀x ∈ ℕ ∀x ∈ ℕ x + y = y + x >>>>>>>>>> >>>>>>>>>> is not, in fact, a well-formed formula of Q (at least not in any version >>>>>>>>>> of Q that I know) > so asking about it's provability in Q is pointless. >>>>>>>>> >>>>>>>>> You may be correct on this. It had been assumed that the above >>>>>>>>> expression was a WFF in Q, if this is not the case then the example >>>>>>>>> ceases to be useful. >>>>>>>> >>>>>>>> The example was originally offered by me as x + y = y + x which *is* >>>>>>>> a WFF of Q. You are the one who keeps insisting on adding extraneous >>>>>>>> symbols to every formula you come across. >>>>>>> >>>>>>> You know that the "extraneous" symbols are not extraneous at all >>>>>>> because they transform the expression into the commutativity of >>>>>>> addition and without them the commutativity of addition is not >>>>>>> expressed. >>>>>> >>>>>> If the added symbols are not extraneous, what exactly is ℕ? >>>>>> >>>>>> Normally (outside the context of Q), ℕ is the set of natural numbers, >>>>>> but Q does not assume that such a set exists. Perhaps you can construct >>>>>> ℕ from the axioms of Q *and then* make statements about ℕ, but you >>>>>> haven't done so. >>>>> >>>>> Yes I see this now. It does not assume natural numbers it defines them >>>>> with its successor function. >>>> >>>> Right, it doesn't assume natural numbers. Whether the things it >>>> defines are natural numbers is another question. It may (or may >>>> not, I don't know) be possible for something other than the set of >>>> natural numbers to satisfy the Q axioms. More precisely, there may >>>> (or may not) be something that satisfies the Q axioms but does not >>>> satisfy all the characteristics of the natural numbers. >>>> >>>>>> You claim that x + y = y + x does not express the commutativity of >>>>>> addition. In fact it does. >>>>> >>>>> If it does express the commutativity of addition and it is provable in >>>>> Q then the statement that the commutativity of addition is not >>>>> provable in Q is a false statement. >>>> >>>> Why did you add "and it is provable"? >>> >>> The whole question is: >>> >>> Are there any formulas of a formal system that are unprovable in the >>> formal system and true in the formal system. Everything that I said >>> for the last several weeks is seeking to answer that one single >>> question. >>> >>> If this formula: "x + y = y + x" does fully express the commutativity >>> of addition and is provable in Q then every reference to Q in the last >>> two weeks is pointless. >> >> If "x + y = y + x" *were* provable in Q, you'd have a point. >> >> I haven't seen anyone here suggest that "x + y = y + x" is provable >> in Q. I'm reasonably sure that it isn't. The first reference >> I've seen to the idea that it might be provable is your own post, >> in which you gratitiously added the words "and it is provable". >> >> [SNIP] >> > Ben was trying to show that a concrete instance: > Successor(Successor(Successor(0))) + Successor(Successor(0)) = > Successor(Successor(0)) + Successor(Successor(Successor(0))) Did you mean to say something else? The above is a sentence fragment, and it doens't respond to what I wrote. -- Keith Thompson (The_Other_Keith) Keith.S.Thompson+u@gmail.com Working, but not speaking, for Philips Healthcare void Void(void) { Void(); } /* The recursive call of the void */