Path: news.eternal-september.org!eternal-september.org!.POSTED!not-for-mail From: Mikko 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