Liste des Groupes | Revenir à theory |
On 6/22/2025 3:29 AM, Mikko wrote:Not "when" but "if". The proof does not prove that Ĥ <Ĥ> transitionsOn 2025-06-21 17:30:25 +0000, olcott said:The proof shows that Ĥ <Ĥ> halts when Ĥ.embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩
On 6/21/2025 3:27 AM, Mikko wrote:On 2025-06-20 16:39:40 +0000, olcott said:Some proofs begin with "assumptions" that are defined to be
On 6/19/2025 3:12 AM, Mikko wrote:Definitions often enable a clearer presentation of the assumptionsBut this is not. A proof starts with assumptions that may be true ofSome proofs begin with definitions instead of assumptions.
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.
and of the proof.
true, thus are not really mere assumptions at all.
<snip>>>>There is nothing impossible in Linz' construction of theDepending on the style of the proof one can ither prove thatNo this is counter-factual.
the counter example exists or that if a halting decider exists
then the caunter example exists, too, and otherwise none is
needed.
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*
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.pdfNothing above shows that Ĥ cannot be consructed if H is given,
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
nor shows any error in the proof that Ĥ <Ĥ> halts if and only if
H <Ĥ> <Ĥ> says "does not halt".
transitions to Ĥ.qn yet Ĥ <Ĥ> is not an input to Ĥ.embedded_H
There has never been any HP proof where the actual inputWhat proof needs to prove and does prove is that H <Ĥ> <Ĥ> does not
does the opposite of whatever its decider decides.
Les messages affichés proviennent d'usenet.