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 14:12:46 -0700 Organization: None to speak of Lines: 130 Message-ID: <87eepf3yr5.fsf@nosuchdomain.example.com> References: <87k0zc8ps5.fsf@nosuchdomain.example.com> <2tCdnb0urbddzpfCnZ2dnUU7-b_NnZ2d@giganews.com> <87k0z85tt0.fsf@nosuchdomain.example.com> <874kqb6e3j.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="25497"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+HCCKciqBOVYJ/9XJzsi6Q" User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux) Cancel-Lock: sha1:vAC+etFPxaHmZJiw4TvIA0+faJ4= sha1:YBZYl4b3s0osEpkqoFryfDeqhms= Xref: csiph.com comp.theory:21626 comp.ai.philosophy:21956 comp.ai.nat-lang:2366 Jeff Barnett writes: > On 7/13/2020 1:58 AM, Keith Thompson wrote: >> 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.) > > Recall, we can't prove commutativity in R|Q period. However, our meta > logic can do the proof because it provides additional > mechanisms. Let's look at a Peano-like induction rule where I is the > integers and S is the successor function: If Z subset-of I, 0 in Z, > and whenever x in Z then Sx in Z; then Z = I. How would an > anti-induction rule be expressed? What would it mean? And would it > lead to inconsistency? In other words would it falsify even one > theorem provable in R|Q by the remaining axioms? The answer to most of that is "I don't know", but I can sketch one possible partial answer. https://en.wikipedia.org/wiki/Robinson_arithmetic#Axioms Consider a set consisting of blue natural numbers (integers >= 0, colored blue) and red integers (all integers, negative, 0, and positive, colored red). The successor of any blue number is a blue number, and the successor of any red number is a red number. (red 0 is zero in the model; blue 0 is not. Blue 0 is the successor of blue -1.) This satisfies at least the first 3 of the 7 axioms described at the link above: 1. Sx ≠ 0 2. (Sx = Sy) → x = y 3. y=0 ∨ ∃x (Sx = y) It breaks induction, since induction would indicate that all numbers are red. I suspect that it breaks one or both of the 5th and 7th axioms, the ones that define addition and multiplication: 4. x + 0 = x 5. x + Sy = S(x + y) 6. x·0 = 0 7. x·Sy = (x·y) + x You'd have to assign meanings to blue-red, red-blue, and red-red addition and multiplication, and I haven't taken the time to try to do so consistently. But if that doesn't work, what I'm wondering is whether there's *some* formulation that's consistent with Robinson Arithmetic in which induction doesn't work. And if there is, that *might* lead to a system consistent with Q in which addition is not commutative. Is induction the only way to prove that Q addition is commutative? -- 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 */