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

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.

(b) Turing machines can take directly executing Turing
machines as *inputs* // false by definition

Not assumend and not relevant to halting problem.

A Turing machine partial halt decider computes the
mapping from a finite string input to the behavior
that this finite string actually specifies.
 A Turing machine partial halt decider never computes the
mapping from the direct execution of any other Turing
machine because direct executions are not finite string
inputs.

A partial halt decider is permitted to compute nothing for some
inputs but if it does compute and answer the answer must agree
with the direct execution (if there is a direct execution to
compare).

None of which affects the truth that
 

A set of expressions is not sufficiently organized to count as a
proof. The conclusion of the proor is its last sentence and in a
set there is no last one.

--
Mikko