Path: csiph.com!eternal-september.org!feeder.eternal-september.org!reader01.eternal-september.org!.POSTED!not-for-mail From: Keith Thompson Newsgroups: comp.theory Subject: Re: Simply defining =?utf-8?Q?G=C3=B6del?= Incompleteness and Tarski Undefinability away V24 (Are we there yet?) Date: Mon, 13 Jul 2020 12:24:21 -0700 Organization: None to speak of Lines: 79 Message-ID: <87pn8z43ru.fsf@nosuchdomain.example.com> References: <2tCdnb0urbddzpfCnZ2dnUU7-b_NnZ2d@giganews.com> <87k0z85tt0.fsf@nosuchdomain.example.com> <87d0505kmk.fsf@nosuchdomain.example.com> <5Lmdnehh4P6hLZbCnZ2dnUU7-LdQAAAA@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="4a04b42c90924d8b69f548a8105eba02"; logging-data="19012"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19ZTsxKtHogWFnbvhft9VK0" User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux) Cancel-Lock: sha1:2xZwYbotzyLkaOhrIxK1VtnSUiw= sha1:3iDnJ9YZnfmE6ub63Fqc9iQxDkA= Xref: csiph.com comp.theory:21624 Alan Smaill writes: > olcott writes: > >> On 7/13/2020 7:05 AM, Alan Smaill wrote: >>> olcott writes: >>> >>>> On 7/12/2020 7:22 PM, Keith Thompson wrote: >>>>> olcott writes: >>>>>> On 7/12/2020 4:04 PM, Keith Thompson wrote: >>>>>>> olcott writes: >>> [..] >>>>>>> Robinson Arithmetic cannot prove or disprove commutativity >>>>>>> of addition. We can construct a consistent system based on >>>>>>> Robinson Arithmetic in which addition is provably commutative. >>>>>> >>>>>> Sure just add an axiom: ∀x ∈ ℕ ∃y ∈ ℕ (x + y = y + x) >>> >>> No. >>> You want ∀x ∈ ℕ ∀y ∈ ℕ (x + y = y + x) -- >>> don't you? >> >> Yes, typo. >> >>>>>>> Can we construct a consistent system based on Robinson Arithmetic >>>>>>> in which addition is provably *not* commutative? >>>>>> >>>>>> Not within the conventional semantics of the meaning of those terms. >>> >>> The question is not about semantics, it's about provability. >>> >>> it's about the existence of a formal system which is both syntactically >>> consistent (ie cannot prove S and also not S, for some statement), >>> extends Q, and can prove non-commutativity. >> >> For the same reason that "cats are animals" is true in biology and not >> true in mathematics there cannot be any expression of the language of >> any formal system that is true in this formal system yet lacks a >> mapping in this formal system from this expression to a Boolean value. > > Let's stick with the example at hand, which you said you wanted to > sort out 100% before moving on. > >>> That's a different question. >>> >>>>> OK. Can you prove that? >>>> >>>> Nothing can possibly be disproved that is true by definition. >>> >>> But the sound deductive model for Q does not *prove* that >>> commutativity is true, so does not prove it "true by definition". >>> You have acceoted that upthread. >> >> φ = ∀x ∈ ℕ ∀y ∈ ℕ (x + y = y + x) >> >> φ is not true or false in Q because Q lacks a mapping in Q from φ to a >> Boolean value. > > That's not what I was asking about. > >>> But the sound deductive model for Q does not *prove* that >>> commutativity is true, so does not prove it "true by definition". >>> You have accepted that upthread. > > In other words, I am asking you about what is *provable* or not in Q, > not about whether commutativity is "true or false". > > You have accepted that Q does not prove commutativity. > If you want to change your mind on that, let us know. He believes that provability and truth are the same thing. He also seems to believe that it's so obvious that they're the same thing that anyone who says otherwise (like Gödel, for example) is being deliberately disingenuous. (That last part is my interpretation and may not be an entirely accurate summary of his belief.) -- 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 */