Path: csiph.com!weretis.net!feeder7.news.weretis.net!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 13:10:53 -0700 Organization: None to speak of Lines: 78 Message-ID: <87lfjjz0du.fsf@nosuchdomain.example.com> References: <87d0505kmk.fsf@nosuchdomain.example.com> <5Lmdnehh4P6hLZbCnZ2dnUU7-LdQAAAA@giganews.com> <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> Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit Injection-Info: reader02.eternal-september.org; posting-host="02ec520d1b2b3210c7ee6ae74092840a"; logging-data="1583"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/LvZI6ytsR3abhgRRI4+kQ" User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux) Cancel-Lock: sha1:fYRAbq2WcEjUxW45WKutv/vNTlw= sha1:Est2/3Ka7Y73pO4MD/f3M0zhSeY= Xref: csiph.com comp.theory:21709 comp.ai.philosophy:22056 comp.ai.nat-lang:2434 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] -- 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 */