Path: ...!news.mixmin.net!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Mikko <mikko.levanto@iki.fi>
Newsgroups: sci.logic
Subject: Re: Undecidability based on epistemological antinomies V2 --Mendelson--
Date: Mon, 29 Apr 2024 12:09:18 +0300
Organization: -
Lines: 71
Message-ID: <v0no3u$1ldmf$1@dont-email.me>
References: <uvq0sg$21m7a$1@dont-email.me> <uvq359$1doq3$4@i2pn2.org> <uvrbvs$2acf7$1@dont-email.me> <uvs70t$1h01f$1@i2pn2.org> <uvsgcl$2i80k$1@dont-email.me> <uvsj4v$1h01e$1@i2pn2.org> <uvsknc$2mq5c$1@dont-email.me> <uvvrj6$3i152$1@dont-email.me> <v00r07$3oqra$1@dont-email.me> <v02ggt$6org$1@dont-email.me> <v03866$bitp$1@dont-email.me> <v056us$rmqi$1@dont-email.me> <v08i2i$1m5hp$2@dont-email.me> <v0akj8$28ghd$1@dont-email.me> <v0bada$2defp$2@dont-email.me> <v0d42v$2tclm$1@dont-email.me> <v0dp8c$31vd9$1@dont-email.me> <v0fpdc$3j50e$1@dont-email.me> <v0gh69$3oudg$1@dont-email.me> <v0iccd$8odv$1@dont-email.me> <v0iv1p$cu99$1@dont-email.me> <v0l56g$vmnj$1@dont-email.me> <v0ljn0$12q0o$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 29 Apr 2024 11:09:18 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="10e1451e65cafef29a572281d306f9b3";
	logging-data="1750735"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX19oB0Y6XK3AInesivyAEJs1"
User-Agent: Unison/2.2
Cancel-Lock: sha1:16pyLwR/Sx3YYvmWhLwezK4G5uI=
Bytes: 4457

On 2024-04-28 13:41:50 +0000, olcott said:

> On 4/28/2024 4:34 AM, Mikko wrote:
>> On 2024-04-27 13:36:56 +0000, olcott said:
>> 
>>> On 4/27/2024 3:18 AM, Mikko wrote:
>>>> On 2024-04-26 15:28:08 +0000, olcott said:
>>>> 
>>>>> On 4/26/2024 3:42 AM, Mikko wrote:
>>>>>> On 2024-04-25 14:27:23 +0000, olcott said:
>>>>>> 
>>>>>>> On 4/25/2024 3:26 AM, Mikko wrote:
>>>>>>>> epistemological antinomy
>>>>>>> 
>>>>>>> It <is> part of the current (thus incorrect) definition
>>>>>>> of undecidability because expressions of language that
>>>>>>> are neither true nor false (epistemological antinomies)
>>>>>>> do prove undecidability even though these expressions
>>>>>>> are not truth bearers thus not propositions.
>>>>>> 
>>>>>> That a definition is current does not mean that is incorrect.
>>>>>> 
>>>>> 
>>>>> ...14 Every epistemological antinomy can likewise be used for a similar
>>>>> undecidability proof...(Gödel 1931:43-44)
>>>>> 
>>>>>> An epistemological antinomy can only be an undecidable sentence
>>>>>> if it can be a sentence. What epistemological antinomies you
>>>>>> can find that can be expressed in, say, first order goup theory
>>>>>> or first order arithmetic or first order set tehory?
>>>>>> 
>>>>> 
>>>>> It only matters that they can be expressed in some formal system.
>>>>> If they cannot be expressed in any formal system then Gödel is
>>>>> wrong for a different reason.
>>>> 
>>>> How is it relevant to the incompleteness of a theory whether an
>>>> epistemological antińomy can be expressed in some other formal
>>>> system?
>>> 
>>> When an expression of language cannot be proved in a formal system only
>>> because it is contradictory in this formal system then the inability to
>>> prove this expression does not place any actual limit on what can be
>>> proven because formal system are not supposed to prove contradictions.
>> 
>> The first order theories of Peano arithmetic, ZFC set theory, and
>> group theroy are said to be incomplete but you have not shown any
>> fromula of any of them that could be called an epistemoloigcal
>> antinomy.
>> 
> 
> The details of the semantics of the inference steps are hidden behind
> arithmetization and diagonalization in Gödel's actual proof.

The correctness of a proof can be checked without any consideration of
semantics. If the proof is fully formal there is an algorithm to check
the correctness.

> ($)   ⊢k G ⇔ (∀x2) ¬𝒫𝑓 (x2, ⌜G⌝)
> 
> Observe that, in terms of the standard interpretation (∀x2) ¬𝒫𝑓 (x2,
> ⌜G⌝) says that there is no natural number that is the Gödel number of a
> proof in K of the wf G, which is equivalent to asserting that there is
> no proof in K of G.

The standard interpretation of artihmetic does not say anything about
proofs and Gödel numbers.

-- 
Mikko