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: Mon, 13 Jul 2020 00:58:24 -0700 Organization: None to speak of Lines: 81 Message-ID: <874kqb6e3j.fsf@nosuchdomain.example.com> References: <87k0zc8ps5.fsf@nosuchdomain.example.com> <2tCdnb0urbddzpfCnZ2dnUU7-b_NnZ2d@giganews.com> <87k0z85tt0.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="4a04b42c90924d8b69f548a8105eba02"; logging-data="8550"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19t1feOPIS5TTmfq0K343fs" User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux) Cancel-Lock: sha1:HwTgrIK5J/VHI284dk47kUmjado= sha1:9VqGFma23E4ZFZ37kEotAJTn+Fo= Xref: csiph.com comp.theory:21612 comp.ai.philosophy:21943 comp.ai.nat-lang:2356 Jeff Barnett writes: > On 7/12/2020 3:04 PM, Keith Thompson wrote: >> It's occurred to me that this raises a (perhaps) interesting question >> -- or maybe I'm missing something obvious. >> >> In a system that includes Euclid's first four postulate but not the >> fifth (the parallel postulate), neither the parallel postulate nor >> its negation can be proven. We can construct a consistent system >> with the parallel postulate as an axiom. We can *also* construct >> a consistent system with the negation of the parallel postulate as >> an axiom. >> >> 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. >> Can we construct a consistent system based on Robinson Arithmetic >> in which addition is provably *not* commutative? > > It's been awhile but my memory might be working. Let's first look at > what a "fixed" use of commutativity might look like: 1+2 = 2+1 > expressed as S0 + SS0 = SS0 + S0, where "s" is the successor function > and "0" is a constant given by the axioms. This can be proven in > Robinson (R) and so can ANY other fixed example. What you can not > prove is the combined version: > forall x in I forall y in I x+y = y+x > Since you can prove each instance, within R, there will be no model > where commutativity does not hold, i.e, where > there exist x in I there exist y in I x+y ~= y+x > can be demonstrated. If we endow R with an appropriate induction > axiom, we can prove commutativity within R. There is no extension to R > that can make commutativity false and the extension consistent. There > are many properties of number like systems where all individual > examples can be proven but the combined property cannot. > > The above example is very instructive: a formal system besides syntax > rules must have proof rules as we all keep saying. Here we can extend > R to be commutative in at least two ways: 1) make it an axiom of R or > 2) adopt an appropriate induction rule a proof rule. (Apparently Robinson Arithmetic is usually called Q, not R.) So Q can't prove that addition is commutative, but Q+induction can, yes? I wonder if a system in which induction specifically *doesn't* work, such as Q+¬induction, so that a statement that would be true in Q+induction might be provably false, could be made to work. But I digress. > Now let's make an observation: R is incomplete because it can't prove > something that is true in it. Of course you can't prove its false > either. In this example, you can prove commutativity is true by using > the power of the meta logic which will have some sort of induction > equivalent available. > > Let's look at another case floating through these discussions or > corrective lectures to a poor student. Consider Euclid with the > standard four postulates P1, P2, P3. P4 plus a bunch of definitions > and the axioms of measure - sort of the real numbers. We know that P5, > the parallel postulate, can be added and so could its negation. In > other words we know that there can be zero, one, or more lines through > a point (not on another line) that do not intersect that other > line. In this case we don't bother to say that P1, P2, P3, P4 are not > complete; rather we make the much more powerful statement that P5 is > INDEPENDENT of basic Euclid. This is in the same way that the axiom of > choice is independent of the rest of basic set theory. That makes sense. So the relationship between Q and the commutativity of addition is fundamentally different from the relationship between Euclid-P5 (Euclid without the parallel postulate) and P5. The former is true but unprovable in Q, but P5 can consistently be made either true or false in a system built on top of Euclid-P5. (But if we could create a system like Q+¬induction, they might be more similar. It seems difficult to think about such as system.) -- 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 */