Re: The key undecidable instance that I know about

On 3/14/25 10:27 AM, olcott wrote:

On 3/13/2025 6:08 AM, Mikko wrote:

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

 LP := ~True(LP) obtains its entire semantics from the expression.

But none of your arguments have talked about an expression that derives itself from that expression

 Because of the cycle in the directed graph of its evaluation
sequence LP cannot derive its semantic meaning from anything
else: ~True(~True(~True(~True(~True(~True(...))))))

But the p that can be developed as a statement in the languaged, based on the idea in the metalanguge that must be true if and only if it is false, doesn't.

 Normally expressions derive their semantics from a knowledge
ontology inheritance hierarchy.
https://en.wikipedia.org/wiki/Ontology_(information_science)

Right, like Godel's expression G specifically derives its semantics from the natured of the system F and the mathematics the system F creates. And, in the meta we can construct a mathematical statement in F, whose truth is the direct opposite of its provability, and thus must be True and Unprovable, as it can't be False but Provably True.
This language seems to be beyond what you can understand, so you just make up lies to cover your ignorance.

 of the set of general knowledge of the world encoded as
Rudolf Carnap meaning postulates using something like Montague
Grammar. Each unique sense meaning has its own GUID.
 

WHich is irrelevent here, as Formal systems don't have that problem.
Your problem