Path: ...!weretis.net!feeder9.news.weretis.net!i2pn.org!i2pn2.org!.POSTED!not-for-mail
From: Richard Damon <richard@damon-family.org>
Newsgroups: sci.logic
Subject: Re: The key undecidable instance that I know about
Date: Sat, 15 Mar 2025 07:24:40 -0400
Organization: i2pn2 (i2pn.org)
Message-ID: <2a12440d8b443f3dd5db8731b7e1ec4d51686b1c@i2pn2.org>
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>
 <abb2ab85e0f15e105af37c6e83d80b3dd882e099@i2pn2.org>
 <vr1ueg$1qopn$2@dont-email.me>
 <753c684398ffb94b1c1e34cc82ed6a8147fc7baf@i2pn2.org>
 <vr2tmc$2kq04$2@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Sat, 15 Mar 2025 11:24:41 -0000 (UTC)
Injection-Info: i2pn2.org;
	logging-data="282557"; mail-complaints-to="usenet@i2pn2.org";
	posting-account="diqKR1lalukngNWEqoq9/uFtbkm5U+w3w6FQ0yesrXg";
User-Agent: Mozilla Thunderbird
X-Spam-Checker-Version: SpamAssassin 4.0.0
In-Reply-To: <vr2tmc$2kq04$2@dont-email.me>
Content-Language: en-US
Bytes: 8826
Lines: 190

On 3/14/25 11:54 PM, olcott wrote:
> On 3/14/2025 8:57 PM, Richard Damon wrote:
>> On 3/14/25 3:01 PM, olcott wrote:
>>> On 3/14/2025 1:42 PM, Richard Damon wrote:
>>>> 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
>>>
>>> In my type theory based system there is no need for
>>> any separate language and meta-language.
>>>
>>> Rudolf Carnap meaning postulates are arranged in an
>>> inheritance hierarchy where each unique sense meaning
>>> is assigned its own GUID.
>>>
>>> The language is something like Montague Grammar.
>>> LP := ~True(LP) is rejected as semantically incorrect.
>>>
>>
>> but the existing systens aren't built on your "Type Theory" so you 
>> need to show that it works in THOSE systems to use it,
>>
> 
> Discard all inferior systems.

NOT A VALID OPERATION.

Sorry, but you are just proving you don't understand what you are talkig 
about.

"Inferior" can't be precisely defined in this context.

> 
>> I guess you are just admitting that you don't understand what you are 
>> talking about, and your "logic" assumes you can just make up crap and 
>> call it true,
>>
> 
> We axiomatize all the basic facts of the world (facts
> that cannot be derived on the basis of other facts).
> Then we plug everything else into an inheritance hierarchy
> knowledge ontology.

But what about contradictory "facts"? Things that define differents 
systems of current logic, thinks like two parrallel lines will never 
meet (Plane Gemoetry) vs Two non-conincident lines will allways have two 
points of intersection (Spherical Geometry).

> 
> Anything that cannot be derived by applying Truth preserving
> operations to these basic facts is either untrue or unknown.

And what about things we can't know if we can know?

> 
> This gives us a True() predicate that always works except
> for unknowns. It certainty does not get totally confused
> by self-contradictory expressions. These simply cannot be
> derived by applying truth preserving operations to basic facts.

No, it doesn't give one, as it has been shown by Godel and Tarski and 
many others, that if you system of logic has enough axioms to create a 
system which has the full power of Natural Numbers, which by your 
description, yours will, it is possible to derive via the use of a 
meta-system, (which is created by a set of valid assumption of 
possiblities, a major part of which is assigning a number to every one 
of the finite number of axioms and basic symbols of the system) we can 
construct a statement whose truth value is the opposite of its 
provability, and thus must be true but unprovable in the basic system.

========== REMAINDER OF ARTICLE TRUNCATED ==========