Re: The key undecidable instance that I know about

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.
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(...))))))
Normally expressions derive their semantics from a knowledge
ontology inheritance hierarchy.
https://en.wikipedia.org/wiki/Ontology_(information_science)
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.
--
Copyright 2025 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer