Re: Undecidability based on epistemological antinomies V2 --Mendelson--

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