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:10:28 -0700 Organization: None to speak of Lines: 87 Message-ID: <87r1taye6j.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>

<878sfjywms.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="U2FsdGVkX19kcAErtDBoEpULdWmE37EB" User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux) Cancel-Lock: sha1:8Vqx0sUlY07Y70jaoonM4yBka8c= sha1:v9HXnBgpSBPpZCPBctPaFwJviqA= Xref: csiph.com comp.theory:21731 comp.ai.philosophy:22077 comp.ai.nat-lang:2452 olcott writes: > On 7/16/2020 4:31 PM, Keith Thompson wrote: >> olcott writes: >>> On 7/15/2020 9:25 PM, André G. Isaak wrote: >>>> On 2020-07-15 18:13, olcott wrote: >>>>> 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. >>>>>> >>>>>> André >>>>> >>>>> 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. >>>>> >>>>> In any case it was a great example while it lasted. >>>>> Do you have another equally simple example that a closed WFF >>>>> of a formal system and is not provable or disprovable in that >>>>> system? >>>> >>>> That IS an example of a closed WFF of a formal system that is >>>> neither provable nor disprovable in that system. >>> >>> So it can't prove S03 + S02 = S02 + S03 ? >> >> "S03" and "S02" aren't even valid syntax in Q, and I'm not sure what you >> mean by them. Q starts with 0 and the successor operation S. S0, SS0, >> and SSS0 can reasonably be referred to as 1, 2, and 3, respectively. >> >> "SSSS0 + SSS0 = SSS0 + SSSS0" is provable in Q. >> The more general statement "x + y = y + x" is not provable in Q. > > Exactly !!! Wait, what? That's what I've been saying all along, and now you agree with me? What were you arguing about? >>>> We're talking about Q. If you want to talk about Q, you should >>>> probably learn the syntax of Q. In Q, all variables are implicitly >>>> assumed to be bound by a universal quantifier unless an explicit >>>> existential quantifier, so >>>> >>>> x + y = y + x >>>> >>>> means 'for all x and for all y, x + y = y + x'. >>> >>> Then it does not mean: S03 + S02 = S02 + S03 >> >> Again, you should probably learn the syntax of Q. No, of course it >> doesn't mean that. If S03 and S02 were syntactically valid, it would >> imply it as a special case. >> >> [...] > > I already know that the actual syntax of Q is a subset of PA. > https://mathworld.wolfram.com/PeanosAxioms.html > Q is 1 - 4 Is it? The description of Q at https://en.wikipedia.org/wiki/Robinson_arithmetic shows 7 axioms, including recursive definitions of addition and multiplication. That page says: Q is *almost* PA without the axiom schema of mathematical induction. (emphasis added). -- 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 */