Path: csiph.com!eternal-september.org!feeder.eternal-september.org!reader01.eternal-september.org!.POSTED!not-for-mail
From: Keith Thompson <Keith.S.Thompson+u@gmail.com>
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: Wed, 15 Jul 2020 18:23:45 -0700
Organization: None to speak of
Lines: 43
Message-ID: <87eepc1cda.fsf@nosuchdomain.example.com>
References: <u8KdneInk71rAp_CnZ2dnUU7-bPNnZ2d@giganews.com> <fwek0z8c20b.fsf@foxtrot.inf.ed.ac.uk> <ZradnRnxvITXyJbCnZ2dnUU7-SXNnZ2d@giganews.com> <87k0z85tt0.fsf@nosuchdomain.example.com> <DsydnePpnqLQPJbCnZ2dnUU7-e_NnZ2d@giganews.com> <87d0505kmk.fsf@nosuchdomain.example.com> <5Lmdnehh4P6hLZbCnZ2dnUU7-LdQAAAA@giganews.com> <fwezh83boxw.fsf@foxtrot.inf.ed.ac.uk> <kZ-dnXdGw7oC5ZHCnZ2dnUU7-f_NnZ2d@giganews.com> <87365vnik3.fsf@bsb.me.uk> <TJidnbVhNKGAb5HCnZ2dnUU7-WfNnZ2d@giganews.com> <87a703lz5c.fsf@bsb.me.uk> <avadnRPjFtHdvJDCnZ2dnUU7-dfNnZ2d@giganews.com> <87pn8ykrwq.fsf@bsb.me.uk> <7e-dnQpoj9jkoZPCnZ2dnUU7-UHNnZ2d@giganews.com> <875zapk0bb.fsf@bsb.me.uk> <zsCdncdz36GK7ZPCnZ2dnUU7-S_NnZ2d@giganews.com> <87lfjkixu6.fsf@bsb.me.uk> <neidnU7COZFyr5LCnZ2dnUU7-XnNnZ2d@giganews.com> <renekb$d4h$1@dont-email.me> <Bt6dnbCdOYJYBpLCnZ2dnUU7-NnNnZ2d@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="6855"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX18smsk4hEvbBnpp01YZOepo"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux)
Cancel-Lock: sha1:G4+XgOFJmqDVqD+EAIc2/8iHDIA= sha1:gld2WIfKbm47L9TvdRIBdFuw+hs=
Xref: csiph.com comp.theory:21693 comp.ai.philosophy:22042 comp.ai.nat-lang:2422

olcott <NoOne@NoWhere.com> 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.

You claim that x + y = y + x does not express the commutativity of
addition.  In fact it does.

> In any case it was a great example while it lasted.
> Do you have another equally simple example that <is> a closed WFF of a
> formal system and is not provable or disprovable in that 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 */