Path: csiph.com!eternal-september.org!feeder.eternal-september.org!reader01.eternal-september.org!.POSTED!not-for-mail
From: Ben Bacarisse <ben.usenet@bsb.me.uk>
Newsgroups: comp.theory,comp.ai.philosophy,comp.ai.nat-lang,sci.lang.semantics
Subject: Re: Simply defining =?iso-8859-1?Q?G=F6del?= Incompleteness and Tarski Undefinability away V24 (Are we there yet?)
Followup-To: comp.theory
Date: Thu, 16 Jul 2020 01:37:44 +0100
Organization: A noiseless patient Spider
Lines: 46
Message-ID: <87y2nkguqv.fsf@bsb.me.uk>
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="1d907a2f9470dff665d5047b0cbf0087"; logging-data="24892"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1+jCfQrfMCypbud9IGJRmEIuPob2GErfoQ="
Cancel-Lock: sha1:h91ZwIOi17rdFhQOtyp0PTZgsA4= sha1:HQuiihoPBfnffKiKt3ruI+wmiNw=
X-BSB-Auth: 1.b1f79d790fbf359e27af.20200716013744BST.87y2nkguqv.fsf@bsb.me.uk
Xref: csiph.com comp.theory:21690 comp.ai.philosophy:22041 comp.ai.nat-lang:2421

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
(That second x should be a y of course)
>>>>
>>>> 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.

No.  Commutativity is expressed as ∀x ∀y x + y = y + x (or just x + y =
y + x if you prefer).  This expresses the commutativity of the two-place
function symbol + for /any/ theory that has a + operation (Q being the
example we are interested in here).

Adding references to ℕ transform it into a statement about a specific
set.  If you bite the bullet and do the exercise I asked you to try, I
could show you why it's so wrong to include ℕ here.

> 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?

Yes: ∀x ∀y x + y = y + x.  It's even simpler than your "poetic" version
with its incorrect references to the natural numbers.  (Of course, you
might have your own meaning for ℕ -- that would be classic PO -- but you
never let on when you added it.)

-- 
Ben.