From Newsgroup: comp.ai.philosophy

On 10/11/2026 3:51 PM, Python wrote:

This sentence finally isolates our disagreement:

   "That predicate has always violated Axiom 1
    for all inputs."

No. Axiom 1 says:

   computation = finite-string transformations
                 applied to finite-string inputs.

The predicate

   HALT(<P>, x) = "does P(x) halt?"

does not violate that.

<P> and x are finite strings.
The decider receives those finite strings.
It performs finite-string transformations.
It returns a finite answer.

Nothing in Axiom 1 says that the property being decided must be
identical to the behavior generated during the decider's own simulation.

Rewrite to be more clear and tie axioms together better https://github.com/plolcott/x86utm/blob/master/README.md

Axiom 1 --- Paraphrase of Emil Post definition of computation
All computations are essentially the application of finite string transformation rules to finite string inputs to derive any and all
outputs.

All computations are only allowed to apply finite string
transformations to their finite string inputs.

Axiom 2
The only correct finite string transformation rules that HHH is
allowed to apply to its finite string input DD is specified by the
operational semantics of the C programming language. This
requires DD to be simulated by HHH according to these rules.

HHH cannot correctly guess that DD will ignore its own line 03
and leap to its own line 06.

Axiom 3
This single unique correct simulation trace derived from (2) can be seen
below. This trace excludes behavior equivalent to DD() directly executed
from main(). HHH cannot report on the behavior of its caller DD().

Axiom 4
DD correctly simulated by HHH cannot possibly reach its own simulated
final halt state is determined by the simulation trace shown below.

Conclusion
From (4) HHH is correct to reject its input as non-halting. From (3)
we know that it is incorrect to require HHH to report on the behavior of
its own caller DD().

Every instance of the Halting Problem proof requires a halt decider H
to report on the behavior it its own caller D otherwise this caller D cannot possibly do the opposite of whatever value that H returns to it.

You have added that restriction yourself.

And this:

   "HHH has no idea who its caller is"

is irrelevant.

A halt decider is not asked:

   "Who called me?"

It is asked:

   "Does the computation encoded by my input halt?"

In the diagonal construction, the relevant program is encoded in the
input. It does not have to be discovered by inspecting the runtime caller.

So PSR may certainly cause:

   HHH(DD)  -> simulation sequence A
   HHH1(DD) -> simulation sequence B

I grant that completely.

But from that you still cannot derive:

   therefore HALT(<DD>) is an invalid predicate.

HHH<DD> reports on the basis of the updated axioms that
more clearly show that DD() executed from main() never
has been the point.

Axiom 1 constrains HOW a computation computes.

You are adding, without proof, a new axiom constraining WHAT a
computation may compute:

   Axiom 1A:
   A decider may only decide properties of the
   particular execution sequence it generates internally.

That statement is nowhere in Axiom 1.

And your entire conclusion now depends on Axiom 1A, not Axiom 1.

I rewrote it to me more clear. It is not in (1)
none-the-less still mandatory.
--
Copyright 2026 Olcott

The essence of computation is applying finite
string transformations to finite string inputs
to derive outputs. // paraphrase of Emil Post

My 28 year goal has been to make
"true on the basis of meaning expressed in language"
reliably computable for the entire body of general knowledge.
The complete structure of this system is now defined.

The entire body of knowledge expressed in language is
comprised of two types of relations between finite strings:
(a) *Axioms* Expressions of language that are stipulated to be true.

My system bridges the analytic/synthetic distinction by
expressly encoding all empirical "atomic facts" in a formal
language such as CycL of the Cyc project.

(b) *Inference Rules* Expressions of language that are semantically
entailed syntactically from (a) and/or (b).
--- Synchronet 3.22a-Linux NewsLink 1.2