Re: D correctly simulated by H cannot possibly halt --- templates and infinite sets

On 2024-05-29 03:49:02 +0000, olcott said:

On 5/28/2024 10:38 PM, Richard Damon wrote:

On 5/28/24 10:23 PM, olcott wrote:

On 5/28/2024 9:04 PM, Richard Damon wrote:

On 5/28/24 12:16 PM, olcott wrote:

typedef int (*ptr)();  // ptr is pointer to int function in C
00       int H(ptr p, ptr i);
01       int D(ptr p)
02       {
03         int Halt_Status = H(p, p);
04         if (Halt_Status)
05           HERE: goto HERE;
06         return Halt_Status;
07       }
08
09       int main()
10       {
11         H(D,D);
12         return 0;
13       }
 When Ĥ is applied to ⟨Ĥ⟩
Ĥ.q0 ⟨Ĥ⟩ ⊢* embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qy ∞
Ĥ.q0 ⟨Ĥ⟩ ⊢* embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
 *Formalizing the Linz Proof structure*
∃H  ∈ Turing_Machines
∀x  ∈ Turing_Machines_Descriptions
∀y  ∈ Finite_Strings
such that H(x,y) = Halts(x,x)

 But since for x being the description of the H^ built from that H and y being the same, it turns out that no matter what answer H gives, it will be wrong.
 

 We have not gotten to that point yet this post is so that
you can fully understand what templates are and how they work.

 But note, x, being a Turing Machine, is NOT a "template"
 And H, isn't a "set of Turing Machines", but an arbitrary member of that set, so all we need to do is find a single x, y, possible determined as a function of H (so, BUILT from a template, but not a template themselves) that shows that particular H was wrong.
  That is basically what Linz does.
 Given a SPECIFIC (but arbitary) H, we can construct a specific H^ built from a template from H, that that H can not get right.
 All the other H's might get this input right, but we don't care, we have shown that for every H we
 

 

(And I think you have an error in your reference to Halts, I think you mean Halts(x,y) not Halts(x,x)
 

 Yes good catch. I was trying to model embedded_H / ⟨Ĥ⟩
and then changed my mind to make it more general.
 

 *Here is the same thing applied to H/D pairs*
∃H ∈ C_Functions
∀D ∈ x86_Machine_Code_of_C_Functions
such that H(D,D) = Halts(D,D)

 Not the same thing.
∃H ∈ C_Functions
is not equivalent to
∃H  ∈ Turing_Machines
 as there are many C_Functions that are not the equivalent of Turing Machines.
 

 The whole purpose here is to get you to understand what
templates are and how they reference infinite sets.
 

 But the problem is that even in your formulation, H and D are, when doing the test, SPECIFIC PROGRAMS and not "templates" as Halts is defined on the domain of PROGRAMS.
 Similarly, a "Template" doesn't have a specific set of x86_Machine_Code_of_C_function, at least not one with defined behavior since if it tries to reference code outside of itself, then Halts of that just isn't defined, only Halts of that code + the specific machine deciding it.
 

 

 In both cases infinite sets are examined to see
if any H exists with the required properties.
 

 Yes, but the logic of Turing Machines looks at them one at a time, and the input is a FULL INDEPENDENT PROGRAM.
 

 ∃H  ∈ Turing_Machines
That does not look at one machine it looks as an infinite set of
machines. I am very happy to find out that you were not playing head
games. Linz actually used the words that you referred to.

 while the ∃H part can create a set of machines, each element of that set is INDIVIDUALLY TESTED in the following conditions, so, when we get to your test  H(x,y) = Halts(x,x), each of H, x, y are individual members of the set, and we THEN collect the set of all of them.
 If we try to say
∃x ∈ Natural Numbers, such that  x+x = 3
we can't say that x is both 1 and 2 and thus as a set meet the requirement. For the conditions, each qualifier select a single prospective element, and those are tested to see if that meet the requirement.
 

 So it never was about any specific machine as Linz misleading words
seemed to indicate. It was always about examining each element of an
infinite set.
 Likewise: ∃H ∈ C_Functions is about examining each element
of an infinite set. A program template specifies a set of programs
the same way that an axiom schema specifies a set of axioms.
 I am very happy that the issue was the misleading words of Linz
and not you playing head games.

In an inderect proof of an unversal claim the counter-hypothesis must
be about one example. Then the proof is about that specific example
until a contradiction is derived.
--
Mikko