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: Sat, 15 Mar 2025 11:30:07 +0200
Organization: -
Lines: 87
Message-ID: <vr3hav$38g2v$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> <vqueag$37be7$1@dont-email.me> <vr1ecc$1ev1a$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sat, 15 Mar 2025 10:30:07 +0100 (CET)
Injection-Info: dont-email.me; posting-host="36a1a36f171f1bbb0b5488c4cb1bb98a";
	logging-data="3424351"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1/7I+js2rlRZZtz56cXm3/E"
User-Agent: Unison/2.2
Cancel-Lock: sha1:DqMs4KQlzMidjhQofzbdN+30nIY=
Bytes: 4489

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