Re: Unpartial Halt Decider 4.0

Mr Flibble <flibble@red-dwarf.jmc.corp> writes:

On Sat, 19 Apr 2025 13:00:42 -0700, Keith Thompson wrote:

Mr Flibble <flibble@red-dwarf.jmc.corp> writes:
[...]

Theorem (Flibble’s Model-Theoretic Parity Principle):
In any theoretical system that permits infinite computational behavior,
a decider analyzing that system may be equipped with equivalent
infinite resources, so long as both reside in a consistent meta-model.

 
If that's a theorem, what's the proof?

>
Proof of Flibble’s Model-Theoretic Parity Principle:
>
Theorem (Flibble’s Model-Theoretic Parity Principle)
In any theoretical system S that permits computational entities M to
exhibit unbounded or infinite behavior (e.g., infinite tape, unbounded
runtime), it is logically consistent to define an analyzer (decider) D
within an extended system S' with equally unbounded or infinite resources,
such that D analyzes M's behavior within the constraints of S, without
contradiction — provided S' ⊇ S and D is not subject to stricter
constraints than M.
Proof
Let S be a computational system
S allows machines M ∈ S with infinite computational behaviors, such as
unbounded tape or unbounded execution time.
Let D be a proposed decider for machines in S
D is designed to determine properties such as halting behavior by
simulating M.
Let S' be an extension of S
S' includes all descriptions and behaviors of S and additionally permits
unbounded computational analysis (e.g., infinite simulation time and
memory).
Construction of D
Define D ∈ S' such that D(M, x) simulates M on input x. D may take
infinite steps but is allowed to do so in S'. D returns 'halts' or
'doesn’t halt' based on complete simulation.
Consistency of D
D does not exist in S and does not violate Turing’s Halting Theorem since
it operates outside the constraints of S. Turing’s proof applies only to
deciders within the same system as the machine they analyze.
Conclusion
Therefore, defining a decider D with equivalent or greater resources than
machines M ∈ S is logically consistent, provided D exists in a model S'
that extends S and permits such analysis.

I believe you have moved the goalposts.

I'll let others analyze and criticize your proof, but what you're
proving doesn't seem to be interesting or useful.

Your claim is that it is "logically consistent" to define an analyzer
with certain kinds of unbounded or infinite resources.

I don't recall anyone claiming it wasn't.  We can certainly discuss
and analyze, for example, halt deciders that require infinite time
and/or storage requirements, and that do not give an answer in finite
time.  (I'm not sure that it's meaningful to yield a result "after"
an infinite number of steps, but perhaps that can be worked out.)

Your implicit claim (and please correct me if I'm mistaken) is that
there's something wrong with the existing widely accepted rules,
in which a halt decider, if such a thing were possible, must yield
a yes/no answer within a finite number of steps.

Your invention of a new system has no effect on theorems proven
within the old one.

An analogy: Within the real numbers, there is no square root of -1.
You can reasonably and usefully talk about complex numbers, a
field in which -1 has a square root (actually two of them, ±i).
But that's changing the subject, and it does not affect the fact
that -1 has no *real* square root.

It would be extremely interesting and useful if we could construct a
halt decider that always yields a result in a finite number of steps.
That has been proven to be impossible.  You can define a system in
which a halt decider can require an infinite number of steps, but
that's less interesting and less useful than a finite halt decider
would be, and it's answering a question that AFAIK nobody asked.

Oh, and I don't think you ever answered by questions about Goldbach's
Conjecture.

--
Keith Thompson (The_Other_Keith) Keith.S.Thompson+u@gmail.com
void Void(void) { Void(); } /* The recursive call of the void */