Path: ...!news.mixmin.net!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail From: Mikko Newsgroups: comp.theory Subject: Re: D correctly simulated by H cannot possibly halt --- templates and infinite sets Date: Fri, 31 May 2024 11:51:22 +0300 Organization: - Lines: 67 Message-ID: References: MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Fri, 31 May 2024 10:51:23 +0200 (CEST) Injection-Info: dont-email.me; posting-host="add4eb6e9b456b964993c963c59aa7fe"; logging-data="2280190"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18D2nd/ScNyFQGTPnBtIAvV" User-Agent: Unison/2.2 Cancel-Lock: sha1:QGVOil0NEdKjocXfvIXJjWyUV3Y= Bytes: 3705 On 2024-05-30 11:33:03 +0000, Richard Damon said: > On 5/30/24 6:11 AM, immibis wrote: >> On 30/05/24 05:48, olcott wrote: >>> On 5/29/2024 9:55 PM, Richard Damon wrote: >>>> On 5/29/24 10:36 PM, olcott wrote: >>>>> On 5/29/2024 9:25 PM, Richard Damon wrote: >>>>>> On 5/29/24 9:55 PM, olcott wrote: >>>>>>> When the category is examined all at once then there is no need >>>>>>> to look at each individual element. >>>>>> >>>>>> So, which one or ones gave the correct answer for their input? >>>>>> >>>>> >>>>> *Formalizing the Linz Proof structure* >>>>> ∃H  ∈ Turing_Machines >>>>> ∀x  ∈ *Turing_Machines_Descriptions* >>>>> ∀y  ∈ Finite_Strings >>>>> such that H(x,y) = Halts(x,y) >>>>> >>>>> When we formalize it that way then some simulating halt deciders >>>>> get the correct answer. >>>>> >>>>> *Everyone else implicitly assumes this incorrect formalization* >>>>> ∃H  ∈ Turing_Machines >>>>> ∀x  ∈ *Turing_Machines* >>>>> ∀y  ∈ Finite_Strings >>>>> such that H(x,y) = Halts(x,y) >>>>> >>>>> >>>> >>>> Nope. >>>> >>>> You just don't understand the meaning of a "Description" in the problem. >>>> >>> >>> A deciders compute the mapping FROM ITS INPUTS >>> to it own accept or reject state >>> Deciders cannot take ACTUAL TURING MACHINES AS INPUTS >>> Deciders can only take FINITE STRINGS AS INPUTS >>> >> >> If you want to be pedantic, you made the mistake. >> It's actually H(DescriptionOf(x),y) = Halts(x,y) >> DescriptionOf is an injective function that converts Turing machines >> into finite strings. > > OR in his formal language: > > > ∃H ∈ Turing_Machines, and for > ∀M ∈ Turing_Machines, which have a description Wm, and > ∀w ∈ Finite_Strings > such that H(Wm,w) = Halts(M,w) > > The problem is that there doesn't exist a FUNCTION "Description" as one > machine can have an potentially infinite number of descriptions. At this point we may assume the axiom of choice. > It is more that there is an inverse function, Described where we could > say that M = Described(Wm) -- Mikko