Re: The key undecidable instance that I know about

On 2025-03-14 14:27:24 +0000, olcott said:

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.

No further discussion about anything above.

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.

As otherwies is not specified it is reasonable to assume that tne
meanings of :=, ~, (, and ) are as usually. The meaning and even
the syntactic nature of True is something unusual that is not
specified. The usual interpretation of := makes the meaning of
LP the same as the meaning of ~True(LP) but leaves both otherwise
unspecified.

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

An intepretation may assign meanings to cyclic structures. For example,
there is a similar sycle in x = 6 - x but the expression has a well
defined arithmetic meaning.

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.

--
Mikko