On 6/21/2025 3:27 AM, Mikko wrote:
On 2025-06-20 16:39:40 +0000, olcott said:
On 6/19/2025 3:12 AM, Mikko wrote:
But this is not. A proof starts with assumptions that may be true of
false. Each statement that is not a definition, axiom, postulate,
hypthesis or other assumption follows from some previous statements
by an inference rule. The conclusion of a proof is the last statement
of the sequence.
Some proofs begin with definitions instead of assumptions.
Definitions often enable a clearer presentation of the assumptions
and of the proof.
Some proofs begin with "assumptions" that are defined to be
true, thus are not really mere assumptions at all.
<snip>>>>
Depending on the style of the proof one can ither prove that
the counter example exists or that if a halting decider exists
then the caunter example exists, too, and otherwise none is
needed.
No this is counter-factual.
It has never been possible for *AN ACTUAL INPUT* to do
the opposite of whatever value that it decider decides.
*For 90 years no one ever bothered to notice this*
There is nothing impossible in Linz' construction of the
counter example. If you think there is you could tell us
the page, paragraph, and sentence in Linz' book that says
someting impossible.
https://www.liarparadox.org/Peter_Linz_HP_317-320.pdf
When M is applied to WM
q0 WM ⊢* Ĥ q0 WM WM ⊢* Ĥ∞
if M applied to WM halts, and
q0 WM ⊢* Ĥ q0 Wm WM ⊢* Ĥ y1 qn y2
if M applied to WM does not halt.
*From the bottom of page 319 has been adapted to this*
When Ĥ is applied to ⟨Ĥ⟩
Ĥ.q0 ⟨Ĥ⟩ ⊢* embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.∞
if Ĥ applied to ⟨Ĥ⟩ halts
Ĥ.q0 ⟨Ĥ⟩ ⊢* embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
if Ĥ applied to ⟨Ĥ⟩ does not halt
This does not have embedded_H reporting on the
behavior specified by its input it has embedded_H
reporting on its own behavior.
When embedded_H is a simulating partial halt decider
then its transition to Ĥ.qn does correctly report that
⟨Ĥ⟩ ⟨Ĥ⟩ correctly simulated by embedded_H cannot possibly
reach its own simulated final halt state of ⟨Ĥ.qn⟩.
*It does this even though embedded_H itself halts. embedded_H*
*is not allowed to report on its own behavior. It is only*
*allowed to report on the behavior that its input specifies*
When Ĥ is applied to ⟨Ĥ⟩ and embedded_H is a
simulating partial halt decider
(a) Ĥ copies its input ⟨Ĥ⟩
(b) Ĥ invokes embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩
(c) embedded_H simulates ⟨Ĥ⟩ ⟨Ĥ⟩
(d) simulated ⟨Ĥ⟩ copies its input ⟨Ĥ⟩
(e) simulated ⟨Ĥ⟩ invokes simulated embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩
(f) simulated embedded_H simulates ⟨Ĥ⟩ ⟨Ĥ⟩
(g) goto (d) with one more level of simulation until
embedded_H sees the repeating pattern and transitions to Ĥ.qn.
⟨Ĥ⟩ ⟨Ĥ⟩ correctly simulated by embedded_H cannot possibly
reach its own simulated final halt state of ⟨Ĥ.qn⟩ thus can
never do the opposite of whatever embedded_H decides. https://www.liarparadox.org/Peter_Linz_HP_317-320.pdf
On 6/22/2025 3:29 AM, Mikko wrote:
On 2025-06-21 17:30:25 +0000, olcott said:
On 6/21/2025 3:27 AM, Mikko wrote:
On 2025-06-20 16:39:40 +0000, olcott said:
On 6/19/2025 3:12 AM, Mikko wrote:
But this is not. A proof starts with assumptions that may be true of >>>>>> false. Each statement that is not a definition, axiom, postulate,
hypthesis or other assumption follows from some previous statements >>>>>> by an inference rule. The conclusion of a proof is the last statement >>>>>> of the sequence.
Some proofs begin with definitions instead of assumptions.
Definitions often enable a clearer presentation of the assumptions
and of the proof.
Some proofs begin with "assumptions" that are defined to be
true, thus are not really mere assumptions at all.
<snip>>>>
Depending on the style of the proof one can ither prove that
the counter example exists or that if a halting decider exists
then the caunter example exists, too, and otherwise none is
needed.
No this is counter-factual.
It has never been possible for *AN ACTUAL INPUT* to do
the opposite of whatever value that it decider decides.
*For 90 years no one ever bothered to notice this*
There is nothing impossible in Linz' construction of the
counter example. If you think there is you could tell us
the page, paragraph, and sentence in Linz' book that says
someting impossible.
https://www.liarparadox.org/Peter_Linz_HP_317-320.pdf
When M is applied to WM
q0 WM ⊢* Ĥ q0 WM WM ⊢* Ĥ∞
if M applied to WM halts, and
q0 WM ⊢* Ĥ q0 Wm WM ⊢* Ĥ y1 qn y2
if M applied to WM does not halt.
*From the bottom of page 319 has been adapted to this*
When Ĥ is applied to ⟨Ĥ⟩
Ĥ.q0 ⟨Ĥ⟩ ⊢* embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.∞
if Ĥ applied to ⟨Ĥ⟩ halts
Ĥ.q0 ⟨Ĥ⟩ ⊢* embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
if Ĥ applied to ⟨Ĥ⟩ does not halt
This does not have embedded_H reporting on the
behavior specified by its input it has embedded_H
reporting on its own behavior.
When embedded_H is a simulating partial halt decider
then its transition to Ĥ.qn does correctly report that
⟨Ĥ⟩ ⟨Ĥ⟩ correctly simulated by embedded_H cannot possibly
reach its own simulated final halt state of ⟨Ĥ.qn⟩.
*It does this even though embedded_H itself halts. embedded_H*
*is not allowed to report on its own behavior. It is only*
*allowed to report on the behavior that its input specifies*
When Ĥ is applied to ⟨Ĥ⟩ and embedded_H is a
simulating partial halt decider
(a) Ĥ copies its input ⟨Ĥ⟩
(b) Ĥ invokes embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩
(c) embedded_H simulates ⟨Ĥ⟩ ⟨Ĥ⟩
(d) simulated ⟨Ĥ⟩ copies its input ⟨Ĥ⟩
(e) simulated ⟨Ĥ⟩ invokes simulated embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩
(f) simulated embedded_H simulates ⟨Ĥ⟩ ⟨Ĥ⟩
(g) goto (d) with one more level of simulation until
embedded_H sees the repeating pattern and transitions to Ĥ.qn.
⟨Ĥ⟩ ⟨Ĥ⟩ correctly simulated by embedded_H cannot possibly
reach its own simulated final halt state of ⟨Ĥ.qn⟩ thus can
never do the opposite of whatever embedded_H decides.
https://www.liarparadox.org/Peter_Linz_HP_317-320.pdf
Nothing above shows that Ĥ cannot be consructed if H is given,
nor shows any error in the proof that Ĥ <Ĥ> halts if and only if
H <Ĥ> <Ĥ> says "does not halt".
The proof shows that Ĥ <Ĥ> halts when Ĥ.embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ transitions to Ĥ.qn yet Ĥ <Ĥ> is not an input to Ĥ.embedded_H
There has never been any HP proof where the actual input
does the opposite of whatever its decider decides.
On 6/23/2025 2:02 AM, Mikko wrote:
On 2025-06-22 16:01:23 +0000, olcott said:
On 6/22/2025 3:29 AM, Mikko wrote:
On 2025-06-21 17:30:25 +0000, olcott said:
On 6/21/2025 3:27 AM, Mikko wrote:
On 2025-06-20 16:39:40 +0000, olcott said:
On 6/19/2025 3:12 AM, Mikko wrote:
But this is not. A proof starts with assumptions that may be true of >>>>>>>> false. Each statement that is not a definition, axiom, postulate, >>>>>>>> hypthesis or other assumption follows from some previous statements >>>>>>>> by an inference rule. The conclusion of a proof is the last statement >>>>>>>> of the sequence.
Some proofs begin with definitions instead of assumptions.
Definitions often enable a clearer presentation of the assumptions >>>>>> and of the proof.
Some proofs begin with "assumptions" that are defined to be
true, thus are not really mere assumptions at all.
<snip>>>>
Depending on the style of the proof one can ither prove that
the counter example exists or that if a halting decider exists >>>>>>>> then the caunter example exists, too, and otherwise none is
needed.
No this is counter-factual.
It has never been possible for *AN ACTUAL INPUT* to do
the opposite of whatever value that it decider decides.
*For 90 years no one ever bothered to notice this*
There is nothing impossible in Linz' construction of the
counter example. If you think there is you could tell us
the page, paragraph, and sentence in Linz' book that says
someting impossible.
https://www.liarparadox.org/Peter_Linz_HP_317-320.pdf
When M is applied to WM
q0 WM ⊢* Ĥ q0 WM WM ⊢* Ĥ∞
if M applied to WM halts, and
q0 WM ⊢* Ĥ q0 Wm WM ⊢* Ĥ y1 qn y2
if M applied to WM does not halt.
*From the bottom of page 319 has been adapted to this*
When Ĥ is applied to ⟨Ĥ⟩
Ĥ.q0 ⟨Ĥ⟩ ⊢* embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.∞
if Ĥ applied to ⟨Ĥ⟩ halts
Ĥ.q0 ⟨Ĥ⟩ ⊢* embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
if Ĥ applied to ⟨Ĥ⟩ does not halt
This does not have embedded_H reporting on the
behavior specified by its input it has embedded_H
reporting on its own behavior.
When embedded_H is a simulating partial halt decider
then its transition to Ĥ.qn does correctly report that
⟨Ĥ⟩ ⟨Ĥ⟩ correctly simulated by embedded_H cannot possibly
reach its own simulated final halt state of ⟨Ĥ.qn⟩.
*It does this even though embedded_H itself halts. embedded_H*
*is not allowed to report on its own behavior. It is only*
*allowed to report on the behavior that its input specifies*
When Ĥ is applied to ⟨Ĥ⟩ and embedded_H is a
simulating partial halt decider
(a) Ĥ copies its input ⟨Ĥ⟩
(b) Ĥ invokes embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩
(c) embedded_H simulates ⟨Ĥ⟩ ⟨Ĥ⟩
(d) simulated ⟨Ĥ⟩ copies its input ⟨Ĥ⟩
(e) simulated ⟨Ĥ⟩ invokes simulated embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ >>>>> (f) simulated embedded_H simulates ⟨Ĥ⟩ ⟨Ĥ⟩
(g) goto (d) with one more level of simulation until
embedded_H sees the repeating pattern and transitions to Ĥ.qn.
⟨Ĥ⟩ ⟨Ĥ⟩ correctly simulated by embedded_H cannot possibly
reach its own simulated final halt state of ⟨Ĥ.qn⟩ thus can
never do the opposite of whatever embedded_H decides.
https://www.liarparadox.org/Peter_Linz_HP_317-320.pdf
Nothing above shows that Ĥ cannot be consructed if H is given,
nor shows any error in the proof that Ĥ <Ĥ> halts if and only if
H <Ĥ> <Ĥ> says "does not halt".
The proof shows that Ĥ <Ĥ> halts when Ĥ.embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩
transitions to Ĥ.qn yet Ĥ <Ĥ> is not an input to Ĥ.embedded_H
Not "when" but "if". The proof does not prove that Ĥ <Ĥ> transitions
to Ĥ.qn. Instead it proves that if and only if H <Ĥ> <Ĥ> halts in H.qn
then Ĥ halts in Ĥ.qn.
When we hypothesize that Ĥ.embedded_H is a simulating PHD
then we know that Ĥ.embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ transitions to H.qn
There has never been any HP proof where the actual input
does the opposite of whatever its decider decides.
What proof needs to prove and does prove is that H <Ĥ> <Ĥ> does not
do what a halt decider is required to do, from which it then proves
that H is not a halt decider.
A halt decider is:
(a) Required to report on its own behavior
(b) Not allowed to report on its own behavior.
On 6/24/2025 3:13 AM, Mikko wrote:
On 2025-06-23 14:56:01 +0000, olcott said:
On 6/23/2025 2:02 AM, Mikko wrote:
On 2025-06-22 16:01:23 +0000, olcott said:
On 6/22/2025 3:29 AM, Mikko wrote:
On 2025-06-21 17:30:25 +0000, olcott said:
On 6/21/2025 3:27 AM, Mikko wrote:
On 2025-06-20 16:39:40 +0000, olcott said:
On 6/19/2025 3:12 AM, Mikko wrote:
But this is not. A proof starts with assumptions that may be true of >>>>>>>>>> false. Each statement that is not a definition, axiom, postulate, >>>>>>>>>> hypthesis or other assumption follows from some previous statements >>>>>>>>>> by an inference rule. The conclusion of a proof is the last statement
of the sequence.
Some proofs begin with definitions instead of assumptions.
Definitions often enable a clearer presentation of the assumptions >>>>>>>> and of the proof.
Some proofs begin with "assumptions" that are defined to be
true, thus are not really mere assumptions at all.
<snip>>>>
Depending on the style of the proof one can ither prove that >>>>>>>>>> the counter example exists or that if a halting decider exists >>>>>>>>>> then the caunter example exists, too, and otherwise none is >>>>>>>>>> needed.
No this is counter-factual.
It has never been possible for *AN ACTUAL INPUT* to do
the opposite of whatever value that it decider decides.
*For 90 years no one ever bothered to notice this*
There is nothing impossible in Linz' construction of the
counter example. If you think there is you could tell us
the page, paragraph, and sentence in Linz' book that says
someting impossible.
https://www.liarparadox.org/Peter_Linz_HP_317-320.pdf
When M is applied to WM
q0 WM ⊢* Ĥ q0 WM WM ⊢* Ĥ∞
if M applied to WM halts, and
q0 WM ⊢* Ĥ q0 Wm WM ⊢* Ĥ y1 qn y2
if M applied to WM does not halt.
*From the bottom of page 319 has been adapted to this*
When Ĥ is applied to ⟨Ĥ⟩
Ĥ.q0 ⟨Ĥ⟩ ⊢* embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.∞
if Ĥ applied to ⟨Ĥ⟩ halts
Ĥ.q0 ⟨Ĥ⟩ ⊢* embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
if Ĥ applied to ⟨Ĥ⟩ does not halt
This does not have embedded_H reporting on the
behavior specified by its input it has embedded_H
reporting on its own behavior.
When embedded_H is a simulating partial halt decider
then its transition to Ĥ.qn does correctly report that
⟨Ĥ⟩ ⟨Ĥ⟩ correctly simulated by embedded_H cannot possibly >>>>>>> reach its own simulated final halt state of ⟨Ĥ.qn⟩.
*It does this even though embedded_H itself halts. embedded_H*
*is not allowed to report on its own behavior. It is only*
*allowed to report on the behavior that its input specifies*
When Ĥ is applied to ⟨Ĥ⟩ and embedded_H is a
simulating partial halt decider
(a) Ĥ copies its input ⟨Ĥ⟩
(b) Ĥ invokes embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩
(c) embedded_H simulates ⟨Ĥ⟩ ⟨Ĥ⟩
(d) simulated ⟨Ĥ⟩ copies its input ⟨Ĥ⟩
(e) simulated ⟨Ĥ⟩ invokes simulated embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ >>>>>>> (f) simulated embedded_H simulates ⟨Ĥ⟩ ⟨Ĥ⟩
(g) goto (d) with one more level of simulation until
embedded_H sees the repeating pattern and transitions to Ĥ.qn.
⟨Ĥ⟩ ⟨Ĥ⟩ correctly simulated by embedded_H cannot possibly >>>>>>> reach its own simulated final halt state of ⟨Ĥ.qn⟩ thus can >>>>>>> never do the opposite of whatever embedded_H decides.
https://www.liarparadox.org/Peter_Linz_HP_317-320.pdf
Nothing above shows that Ĥ cannot be consructed if H is given,
nor shows any error in the proof that Ĥ <Ĥ> halts if and only if >>>>>> H <Ĥ> <Ĥ> says "does not halt".
The proof shows that Ĥ <Ĥ> halts when Ĥ.embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ >>>>> transitions to Ĥ.qn yet Ĥ <Ĥ> is not an input to Ĥ.embedded_H
Not "when" but "if". The proof does not prove that Ĥ <Ĥ> transitions >>>> to Ĥ.qn. Instead it proves that if and only if H <Ĥ> <Ĥ> halts in H.qn >>>> then Ĥ halts in Ĥ.qn.
When we hypothesize that Ĥ.embedded_H is a simulating PHD
then we know that Ĥ.embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ transitions to H.qn
There has never been any HP proof where the actual input
does the opposite of whatever its decider decides.
What proof needs to prove and does prove is that H <Ĥ> <Ĥ> does not
do what a halt decider is required to do, from which it then proves
that H is not a halt decider.
A halt decider is:
(a) Required to report on its own behavior
(b) Not allowed to report on its own behavior.
For some inputs (a), for other inputs (b).
No halt decider can possibly report on its
own behavior because no halt decider takes
an executing process as its input.
| Sysop: | Keyop |
|---|---|
| Location: | Huddersfield, West Yorkshire, UK |
| Users: | 546 |
| Nodes: | 16 (0 / 16) |
| Uptime: | 170:31:11 |
| Calls: | 10,385 |
| Calls today: | 2 |
| Files: | 14,057 |
| Messages: | 6,416,559 |