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

On 2024-05-02 13:22:29 +0000, olcott said:
 

On 5/2/2024 3:19 AM, Mikko wrote:

On 2024-05-01 15:11:00 +0000, olcott said:
>

On 5/1/2024 4:01 AM, Mikko wrote:

On 2024-04-30 16:08:08 +0000, olcott said:
>

On 4/30/2024 7:04 AM, Mikko wrote:

On 2024-04-29 15:26:23 +0000, olcott said:
>

On 4/29/2024 10:13 AM, Mikko wrote:

On 2024-04-29 14:22:36 +0000, olcott said:
>

On 4/29/2024 4:09 AM, Mikko wrote:

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

>
That was a direct quote from a math textbook, here it is again:

>
That quote didn't define "standard semantics".
>

>
It need not define standard semantics once is has summed of the essence of that whole proof as: G says “I am not provable in K”.

>
In the standard semantics of arithmetic nothing means "I am not provable
in K". That simply is not an arithmetic statement about numbers.
>

>
Mendelson says that Gödel's actual proof is equivalent to:
G says “I am not provable in K”.

>
For a certain kind of equivalence. But they are not semantically equivalent:
G is an arithmetic sentence and in the standard smeantics it is interpreted
as an arithmetic statement about numbers. The statement "I am not provable
in K" is an English sentence and in the standard semantics of English it
does not refer to numbers.
>
You can regard the two sentences equivalent if you use some non-stadard
semantics for arithmetic or English or both. Or you may try to find a
mapping from one system to another that has the necessary properties to
prove someting.
>

>
G says “I am not provable in K”. // Mendelson

>
That is obviously a non-arithmetic interpretation of G. As G is a formula
of arithmetic, a non-arithmetic interpretation depends on non-statndard
semantics.
>

...We are therefore confronted with a proposition which asserts its own unprovability. 15 ...(Gödel 1931:43-44)

>
Likewise.
>

This is the correct way to encode that:
>
∃G ∈ K (G := (K ⊬ G))

>
No, it isn't, as := means definition and its syntactic rules prohibit
from using the same symbol (here G) on both sides.
>

>
The conventional way to encode that is to intentionally represent
self-reference incorrectly I overrode that incorrect convention
with actual self-reference.
>
https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
>
The Liar Paradox in Minimal is this
LP := ~True(LP) which means: ~True(~True(~True(~True(...))))
when coded correctly.

 You can't use any conventional logic if your formulas violate their
syntax rules. If you use unconventional logic it is safest to regard
your proofs as arguments as unacceptable.