Path: csiph.com!3.eu.feeder.erje.net!feeder.erje.net!news.szaf.org!nntp-feed.chiark.greenend.org.uk!ewrotcd!usenet.inf.ed.ac.uk!.POSTED!not-for-mail
From: Alan Smaill <smaill@SPAMinf.ed.ac.uk>
Newsgroups: comp.theory
Subject: Re: Simply defining =?utf-8?Q?G=C3=B6del?= Incompleteness and Tarski Undefinability away V24 (Are we there yet?)
Date: Sat, 11 Jul 2020 12:25:46 +0100
Lines: 60
Message-ID: <fweo8om8f9h.fsf@foxtrot.inf.ed.ac.uk>
References: <u8KdneInk71rAp_CnZ2dnUU7-bPNnZ2d@giganews.com> <ybCdnWSasLM_y5jCnZ2dnUU7-UPNnZ2d@giganews.com> <re3m63$6gj$1@dont-email.me> <GJednZgniKUVwpjCnZ2dnUU7-fHNnZ2d@giganews.com> <re3o8o$fut$1@dont-email.me> <KIWdndtXOfObf5jCnZ2dnUU7-UXNnZ2d@giganews.com> <re4pvf$tfs$1@dont-email.me> <uO6dnXdLIenDY5jCnZ2dnUU7-cnNnZ2d@giganews.com> <re76nh$kfu$1@dont-email.me> <FqidnaWu_N0e35rCnZ2dnUU7-WHNnZ2d@giganews.com> <87k0zc8ps5.fsf@nosuchdomain.example.com> <bNWdndqU8Kz86pXCnZ2dnUU7-U_NnZ2d@giganews.com> <W9KdnaeGwPnf5pXCnZ2dnUU7-f-dnZ2d@giganews.com> <rea299$p7c$1@dont-email.me> <l_WdnYLO9uGGEpXCnZ2dnUU7-e_NnZ2d@giganews.com> <rea6hg$m4j$1@dont-email.me> <sLGdnelhK8QZP5XCnZ2dnUU7-c_NnZ2d@giganews.com> <rea8ev$2re$1@dont-email.me> <RrydndCJKL46MJXCnZ2dnUU7-dvNnZ2d@giganews.com> <fweo8onfcyl.fsf@foxtrot.inf.ed.ac.uk> <wOOdncmMTradKJXCnZ2dnUU7-dvNnZ2d@giganews.com>
NNTP-Posting-Host: foxtrot.inf.ed.ac.uk
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 8bit
X-Trace: macpro.inf.ed.ac.uk 1594466746 13772 129.215.24.196 (11 Jul 2020 11:25:46 GMT)
X-Complaints-To: usenet@macpro.inf.ed.ac.uk
NNTP-Posting-Date: Sat, 11 Jul 2020 11:25:46 +0000 (UTC)
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.5 (gnu/linux)
Cancel-Lock: sha1:AzYdhq9FBneA2dELpLidjyEHRDc=
Xref: csiph.com comp.theory:21576

olcott <NoOne@NoWhere.com> writes:

> On 7/10/2020 1:21 PM, Alan Smaill wrote:
>> olcott <NoOne@NoWhere.com> writes:
>>
>>> On 7/10/2020 12:27 PM, André G. Isaak wrote:
>>
>> [..]
>>
>>>> Why don't you actually *think* about things instead of just
>>>> randomly making minor changes to your formulae. If you want to
>>>> express the fact that commutativity is not provable in Q, the
>>>> correct expression would be:
>>>>
>>>> Q ⊬ (∀x ∀y (x + y = y + x))
>>> Yes that makes sense. That is a good way to say it.
>>> I need to translate that into this form: 
>>>
>>> φ = (∀x ∀y (x + y = y + x))
>>> Q ⊬ φ // This is true in Q
[..]
>>> ∴ φ ↔ Q ⊬ φ is not true in Q
[..]
>> if you want to see what you are trying to refute,
>> take "A <-> B" as "(A & B) or (~A & ~B)".
>
> If this is unsatisfiable in every model: ∃φ (φ ↔ T ⊬ φ)
> Then it is unsatisfiable in every model of arithmetic.

"If" ...

You miss the point of my comment --
try thinking before you give your stock response.

Let's go back to the start and try again:

>>> Q ⊬ φ // This is true in Q

Agreed.

>>> ∴ φ ↔ Q ⊬ φ is not true in Q

What makes you think this?

>> if you want to see what you are trying to refute,
>> take "A <-> B" as "(A & B) or (~A & ~B)".

Can either of these cases hold?

Yes, we could be in the A & B case:
  φ ↔ Q ⊬ φ  *can* be true when  Q ⊬ φ is true.

So your claim tyat therefore:

>>> ∴ φ ↔ Q ⊬ φ is not true in Q

is not justified.

-- 
AS