Re: The key undecidable instance that I know about

On 2025-03-11 23:26:28 +0000, olcott said:

On 3/11/2025 6:15 AM, Mikko wrote:

On 2025-03-10 15:36:28 +0000, olcott said:
 

I created Minimal Type Theory such that self-reference
can be expressed concisely and correctly.

 Have you pbulished that "Minimal Type Theory" or put it to a web page?
Without a pointer to it there is no point to mention it. Of course one
can create a language that can express a self reference but why would
one?

 https://www.researchgate.net/publication/315367846_Minimal_Type_Theory_MTT

Does not define any theory.

https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF

The article 315367846_Minimal_Type_Theory_MTT says that "Types must be
expressly stated in Minimal Type Theory" but the syntax allows untyped
quantification.

https://www.researchgate.net/publication/317953772_Provability_with_Minimal_Type_Theory 

This article uses @ as definition article but a comment in the syntax
says that := is used.
None of the articles defines what is a valid proof in Minimal Type Theory.

We need such a language so that we don't stupidly
fail to understands how this can convert expressions
of language into non-truth-bearers having no truth value.
 Until we do this we get confused into believing
that such expressions are in any way undecidable.
 

Apparently this cannot be expressed concisely and correctly in
any formal logic system.

 A self reference cannot be expressed in an uninterpreted formal language.
Sometimes some symbols and expressions are interpreted to represent
themselves or other symbols or expressions. For example, the symbol 0
of arthmetic can be interpreted to mean the symbol 0 and the term
S0 the sqence of symbols S and 0.

 LP := ~True(LP)
has all of its semantics encoded in its syntax, thus no
interpretation required.

Without decoding no semantics can be extracted from the syntax.
--
Mikko