Re: How do simulating termination analyzers work? ---Truth Maker Maximalism

On 2025-07-04 12:34:39 +0000, olcott said:

On 7/4/2025 2:25 AM, Mikko wrote:

On 2025-07-03 22:11:45 +0000, olcott said:
 

On 7/2/2025 1:53 AM, Mikko wrote:

On 2025-07-01 11:46:11 +0000, olcott said:
 

On 7/1/2025 2:51 AM, Mikko wrote:

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.

 It is relevant to the halting problem because
no input to a halt decider can possibly do the
opposite of whatever its halt decider decides.
The thing that does the opposite is not an input.

 It is irrelevant because the halting problem clarly states that the
input is a description of a Turing machine and an input to that
machine. You may say that to decide halting of a directly executed
Turing machnie is not possible from the given input but the problem
is what it is.

 Although it is called a description that term is inaccurate.
It leads people to believe that 98% of exactly what it does
is close enough. That DD() *DOES NOT DO* what DD correctly
simulated by HHH does is a key detail *THAT ALWAYS ESCAPES THEM*

 What HHH correctly or otherwise simulates is merely an implementation
detail.

 It is a detail that defines a partial halt decider
that makes the "do the opposite" code unreachable.

No, it does. The proof that a counter-example can be constructed
does not refer to any implementation details, so it applies to
every implementation that is does not violate the requirements
so obviously that the proof is not needed.

What matters is the beahviour DD specifies.

 The behavior that an input specifies is only correctly
measured by correctly simulating this input.

Wrong. It is correctly measured by a direct execution. A simulation that
is proven to reproduce the same behaviour as a direct exectuion is an
acceptable proxy.

The user's
manual must specify how DD (or any other algorithm) shall be described
for HHH.

 The C programming language translated into x86 machine code.

You said that DDD as an input to HHH specifies a non-halting behaviour.
The behaviour specifed by the x86 translation of DDD as inpterpreted
according to the x86 instruction semantics specifies a halting
behaviour. Therefore the halting behaviour specified by DDD must be
described differently to HHH and user's manual must tell how.
The situation with DD is similar but more complicated as it is not
as obvious whether DD specifies a halting or non-halting behaviour.
Anyway the result is that HHH needs something else than the C code
of DD in order to be able to tell whether DD specifies a halting or
non-halting behaviour when interpreted according to the rules of
C or x86 language.
Without a user's manual where the input rules covering DD and DDD and
similar cases are clearly specified HHH is not a conter-example to
any uncomputability proof nor a useful partial decider or analyzer.
--
Mikko