Path: news.eternal-september.org!eternal-september.org!.POSTED!not-for-mail
From: Mikko <mikko.levanto@iki.fi>
Newsgroups: comp.theory
Subject: Re: How do simulating termination analyzers work? ---Truth Maker Maximalism
Date: Tue, 1 Jul 2025 10:51:08 +0300
Organization: -
Lines: 100
Message-ID: <104041c$2nne5$1@dont-email.me>
References: <102sjg5$2k3e9$1@dont-email.me> <1607e7860c899b930b87d371c747708dbeaf1062@i2pn2.org> <102t67r$2o80a$1@dont-email.me> <102u3et$31q0g$4@dont-email.me> <102ufv8$35emj$1@dont-email.me> <1030kqk$3pfor$1@dont-email.me> <10319mv$3u901$7@dont-email.me> <103394q$m26r$1@dont-email.me> <1033pf6$25t1$1@dont-email.me> <1035vdm$10d9c$1@dont-email.me> <1036qg0$16lpk$3@dont-email.me> <1038glb$e9bd$1@dont-email.me> <1039kq9$n1od$1@dont-email.me> <103aupj$13t8e$1@dont-email.me> <103c0mb$1cme6$2@dont-email.me> <103dp34$1toq7$1@dont-email.me> <103eeie$22250$12@dont-email.me> <103g682$2k9u7$1@dont-email.me> <103h1ch$2q86f$5@dont-email.me> <103j40h$3col5$1@dont-email.me> <103n9si$ecm8$1@dont-email.me> <103okoh$r8lq$1@dont-email.me> <103oql4$rq7e$7@dont-email.me> <103qu9v$1egu3$1@dont-email.me> <103rh5r$1hc53$7@dont-email.me> <103th0k$22kgq$1@dont-email.me> <103uin0$292c0$7@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 01 Jul 2025 09:51:08 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="7f7db4a9208ad5ef51039c9fed5a5eed";
	logging-data="2874821"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX19FWxvXloOGJtIiOZ9LJnbZ"
User-Agent: Unison/2.2
Cancel-Lock: sha1:gyH8y3ttx9Vn+4hRW/2NxfPgKp4=

On 2025-06-30 17:49:20 +0000, olcott said:

> On 6/30/2025 3:14 AM, Mikko wrote:
>> On 2025-06-29 14:04:43 +0000, olcott said:
>> 
>>> On 6/29/2025 3:42 AM, Mikko wrote:
>>>> On 2025-06-28 13:28:04 +0000, olcott said:
>>>> 
>>>>> On 6/28/2025 6:47 AM, Mikko wrote:
>>>>>> On 2025-06-27 23:35:46 +0000, olcott said:
>>>>>> 
>>>>>>> On 6/26/2025 4:30 AM, Mikko wrote:
>>>>>>>> On 2025-06-25 14:33:52 +0000, olcott said:
>>>>>>>> 
>>>>>>>>> On 6/25/2025 1:50 AM, Mikko wrote:
>>>>>>>>>> On 2025-06-24 15:00:30 +0000, olcott said:
>>>>>>>>>> 
>>>>>>>>>>> 
>>>>>>>>>>> A proof is any set of expressions of language that
>>>>>>>>>>> correctly concludes that another expression of
>>>>>>>>>>> language is definitely true.
>>>>>>>>>> 
>>>>>>>>>> A singlet set of expressions that just states a correct conclusion
>>>>>>>>>> satisfy the above definition but does not prove anything. A proof
>>>>>>>>>> is something that gives a sufficient reson to believe what otherwise
>>>>>>>>>> might not be believed.
>>>>>>>>> 
>>>>>>>>> Correct proofs can also depend on the meaning of natural
>>>>>>>>> language words.
>>>>>>>> 
>>>>>>>> Yes, and avoid ambiguous expressions or disambiguate them when needed.
>>>>>>>> 
>>>>>>>>> It is typical that formal proofs make sure
>>>>>>>>> to totally ignore every aspect of this.
>>>>>>>> 
>>>>>>>> That is the main advantage of formal proofs. But an application
>>>>>>>> of a formal proof usually requires natural language to express
>>>>>>>> the interpretation.
>>>>>>>> 
>>>>>>>>> An expression of language is proven true when a set of
>>>>>>>>> semantic meanings makes it true.
>>>>>>>> 
>>>>>>>> Often it is sufficiently proven if it is observed to be true
>>>>>>>> though that of course depends on the qualyty of the obserfation
>>>>>>>> and of the quality of the report of the observation.
>>>>>>>> 
>>>>>>>>> To really understand this requires deep understanding of
>>>>>>>>> the philosophy of truth, rather than rote memorization
>>>>>>>>> of some conventional steps.
>>>>>>>> 
>>>>>>>> Deep understanding is rarely useful. Often it is sufficient to
>>>>>>>> understand that what is presented as a proof isn't a proof.
>>>>>>>> 
>>>>>>>>> Two elements that require very deep understanding are
>>>>>>>>> (a) truth-makers and (b) truth-bearers.
>>>>>>>>> Truthmaker Maximalism says that when there is nothing
>>>>>>>>> that makes an expression of language true then this
>>>>>>>>> expression is not true.
>>>>>>>> 
>>>>>>>> That is not a useful result as the non-existence is usually
>>>>>>>> unobservable and unverifiable.
>>>>>>> 
>>>>>>> Analytical truth has nothing to do with observation
>>>>>>> and has everything to do we semantic connections
>>>>>>> between expressions of language.
>>>>>> 
>>>>>> Your claims above were about truth in general with no restriction
>>>>>> to analytical truths. But if you don't know that a sentence has
>>>>>> no truth maker it may be hard to find out.
>>>>>> 
>>>>>>> All of math, computer science and logic is analytic truth.
>>>>>>> We don't observe that 5 > 3, it is defined that way.
>>>>>> 
>>>>>> And that includes the non-existence of halt deciders.
>>>>> 
>>>>> *This is only based on false assumptions*
>>>>> (a) An *input* can be defined that does the opposite
>>>>> of whatever its decider reports. // proven false
>>>> 
>>>> Not an assumption but proven true from definitions.
>>> 
>>> No one ever noticed that it is never an actual
>>> *input* that does this.
>> 
>> That "input" is an input to the halting problem. The input to the
>> decider candidate is a representation of input to the halting
>> problem. To "do the opposite" refers to what happens if the
>> "input" computation is executed. Whether it is actually executed
>> is irrelevant.
> 
> Yet no directly executed Turing Machine DDD() can be an input
> to another Turing Machine HHH making this DDD() outside of the
> domain of HHH thus its behavior is irrelevant to the correctness
> of HHH(DDD).

Irrelevant to the halting problem.

-- 
Mikko