Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!eternal-september.org!.POSTED!not-for-mail
From: Mikko <mikko.levanto@iki.fi>
Newsgroups: sci.logic
Subject: Re: The key undecidable instance that I know about
Date: Thu, 13 Mar 2025 13:08:00 +0200
Organization: -
Lines: 56
Message-ID: <vqueag$37be7$1@dont-email.me>
References: <vqkib1$r5np$1@dont-email.me> <vqmcgu$19ima$1@dont-email.me> <vqn0tt$1drh6$1@dont-email.me> <vqp5vr$1uhhq$1@dont-email.me> <vqqgr4$27b5f$3@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Thu, 13 Mar 2025 12:08:01 +0100 (CET)
Injection-Info: dont-email.me; posting-host="9ea8f9a729b53f03addc529017f754af";
	logging-data="3386823"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX19YmdXYNn27yYGXfuwKKY8j"
User-Agent: Unison/2.2
Cancel-Lock: sha1:h0TYsIr+E5iJcDkycNOW88pcBkA=
Bytes: 3045

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