Path: ...!eternal-september.org!feeder3.eternal-september.org!i2pn.org!i2pn2.org!.POSTED!not-for-mail
From: Richard Damon <richard@damon-family.org>
Newsgroups: sci.logic
Subject: Re: How a True(X) predicate can be defined for the set of analytic
 knowledge (HoTT)
Date: Sat, 22 Mar 2025 09:37:13 -0400
Organization: i2pn2 (i2pn.org)
Message-ID: <887f551baf86bd19a5d4d500e5efd81e79dd6da3@i2pn2.org>
References: <vrfvbd$256og$2@dont-email.me> <vrh432$39r47$1@dont-email.me>
 <vrhami$3fbja$2@dont-email.me> <vrj9lu$1791p$1@dont-email.me>
 <vrjn82$1ilbe$2@dont-email.me>
 <c6652d1186f31022d0441c141f39553835511071@i2pn2.org>
 <vrl1b5$2na3e$2@dont-email.me>
 <5e7d29c760ee6b7ce75667c08a7be7b63d461500@i2pn2.org>
 <vrl9ud$2ude6$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Sat, 22 Mar 2025 13:37:13 -0000 (UTC)
Injection-Info: i2pn2.org;
	logging-data="1277830"; mail-complaints-to="usenet@i2pn2.org";
	posting-account="diqKR1lalukngNWEqoq9/uFtbkm5U+w3w6FQ0yesrXg";
User-Agent: Mozilla Thunderbird
X-Spam-Checker-Version: SpamAssassin 4.0.0
Content-Language: en-US
In-Reply-To: <vrl9ud$2ude6$1@dont-email.me>
Bytes: 5758
Lines: 107

On 3/21/25 11:14 PM, olcott wrote:
> On 3/21/2025 9:31 PM, Richard Damon wrote:
>> On 3/21/25 8:47 PM, olcott wrote:
>>> On 3/21/2025 6:49 PM, Richard Damon wrote:
>>>> On 3/21/25 8:49 AM, olcott wrote:
>>>>> On 3/21/2025 3:57 AM, Mikko wrote:
>>>>>> On 2025-03-20 15:02:42 +0000, olcott said:
>>>>>>
>>>>>>> On 3/20/2025 8:09 AM, Mikko wrote:
>>>>>>>> On 2025-03-20 02:42:53 +0000, olcott said:
>>>>>>>>
>>>>>>>>> It is stipulated that analytic knowledge is limited to the
>>>>>>>>> set of knowledge that can be expressed using language or
>>>>>>>>> derived by applying truth preserving operations to elements
>>>>>>>>> of this set.
>>>>>>>>
>>>>>>>> A simple example is the first order group theory.
>>>>>>>>
>>>>>>>>> When we begin with a set of basic facts and all inference
>>>>>>>>> is limited to applying truth preserving operations to
>>>>>>>>> elements of this set then a True(X) predicate cannot possibly
>>>>>>>>> be thwarted.
>>>>>>>>
>>>>>>>> There is no computable predicate that tells whether a sentence
>>>>>>>> of the first order group theory can be proven.
>>>>>>>>
>>>>>>>
>>>>>>> Likewise there currently does not exist any finite
>>>>>>> proof that the Goldbach Conjecture is true or false
>>>>>>> thus True(GC) is a type mismatch error.
>>>>>>
>>>>>> However, it is possible that someone finds a proof of the conjecture
>>>>>> or its negation. Then the predicate True is no longer complete.
>>>>>>
>>>>>
>>>>> The set of all human general knowledge that can
>>>>> be expressed using language gets updated.
>>>>
>>>> And thus your concept of truth breaks.
>>>>
>>>> Truth, by its definition is an immutable thing, but you just defined 
>>>> it to be mutable.
>>>>
>>>> How often do we need to re-verify our truths?
>>>>
>>>>>
>>>>>>> When we redefine logic systems such that they begin
>>>>>>> with set of basic facts and are only allowed to
>>>>>>> apply truth preserving operations to these basic
>>>>>>> facts then every element of the system is provable
>>>>>>> on the basis of these truth preserving operations.
>>>>>>
>>>>>> However, it is possible (and, for sufficiently powerful sysems, 
>>>>>> certain)
>>>>>> that the provability is not computable.
>>>>>>
>>>>>
>>>>> When we begin with basic facts and only apply truth preserving
>>>>> to the giant semantic tautology of the set of human knowledge
>>>>> that can be expressed using language then every element in this
>>>>> set is reachable by these same truth preserving operations.
>>>>>
>>>>
>>>> But you aren't begining with basic facts, but with what has been 
>>>> assumed to be the basic facts. 
>>>
>>> That is not what I stipulated.
>>> When we begin with what actual are the set of basic
>>> facts and are only allowed to apply truth preserving
>>> operations to these basic facts then it is self-evident
>>> that True(X) must always be correct.
>>
>> But you can't stipulate that you cant' get to things that you can get to.
>>
>> If your system can define the Natural Numbers, then we get Godel and 
>> Tarski, and you can't stop it.
>>
> 
> The entire semantics of G is defined in the body of human general
> knowledge that can be expressed in language henceforth called (BOK).

Yes, and that is that there does not exist a number that satifies a 
particular involved Primative Recursive Relationship.

> 
> The whole language metalanguage thing is already taken care of
> in a hierarchy of types that expresses multiple levels of logic
> in the same formal system and formal language.

Nope, it is clear you just don't understand what the metalanguage does, 
it NUMBERS all the symbols and axioms of the system. A system can not 
number itself, as the numbering creates axioms that would then need to 
be numbered, and that makes the system infinite. This allows us to 
convert ALL logic into mathematics

> 
> https://en.wikipedia.org/wiki/History_of_type_theory#G%C3%B6del_1944
> 

Which has nothing to do with this problem. Your problem is you don't 
actually understand what this means, and have replaced words with 
different meanings, and thus invalidated the truths in it.

Part of the problem seems to be that you small mind just can't 
comprehend what infinity does to logic. In fact, your concept VIOLATES 
this principle, as your "set" of Knowledge, mixes types and is thus 
excluded from the field. They are excluded, as the theory doesn't hold 
when such a set is allowed.