olcott <NoOne@NoWhere.com> writes:
Linz's "proof" that no universal halt decider exists is entirely based
on his belief that H cannot decide ⟨Ĥ⟩ ⟨Ĥ⟩ correctly.
It's a proof, not a "proof". It only becomes a "proof" when someone
finds a mistake in it. And it does not rely on his beliefs. That's not
the word to use when talking about simple logic like this:
If a TM, H, existed such that
Hq0 <M> s ⊦* Hqy if M applied to s halts, and
Hq0 <M> s ⊦* Hqn if M applied to s does not halt,
we could construct from it an H' such that
H'q0 <M> s ⊦* oo if M applied to s halts, and
H'q0 <M> s ⊦* H'qn if M applied to s does not halt.
And from that we could construct an Ĥ such that
Ĥq0 <M> ⊦* Ĥqx <M> <M> ⊦* oo if M applied to <M> halts, and
Ĥq0 <M> ⊦* Ĥqx <M> <M> ⊦* Ĥqn if M applied to <M> does not halt.
Setting M to Ĥ, so <M> becomes <Ĥ>, we see that the existence of H (as
Linz defines it) logically entails that a TM Ĥ that does this
Ĥq0 <Ĥ> ⊦* Ĥqx <Ĥ> <Ĥ> ⊦* oo if Ĥ applied to <Ĥ> halts, and
Ĥq0 <Ĥ> ⊦* Ĥqx <Ĥ> <Ĥ> ⊦* Ĥqn if Ĥ applied to <Ĥ> does not halt.
would also have to exist. But, as Linz says, "this is clearly
nonsense".
To call such trivial sequence of deductions a belief is just rhetorical
spin.
On Tuesday, 26 October 2021 at 15:47:36 UTC+1, olcott wrote:WOULD
On 10/26/2021 9:28 AM, Ben Bacarisse wrote:Well that hasn't been thought through. Assuming simulating halt decider H
olcott <No...@NoWhere.com> writes:Because this is necessarily true (only a fool would disagree)
Linz's "proof" that no universal halt decider exists is entirely based >>>> on his belief that H cannot decide ⟨Ĥ⟩ ⟨Ĥ⟩ correctly.
It's a proof, not a "proof". It only becomes a "proof" when someone
finds a mistake in it. And it does not rely on his beliefs. That's not
the word to use when talking about simple logic like this:
Simulating Halt Decider Theorem (Olcott 2021):
Whenever simulating halt decider H correctly determines that input P
never reaches its final state (whether or not its simulation of P is
aborted) then H correctly decides that P never halts.
to be a Turing machine, if H's simulation of P is not halted, H never terminates,
so, using Turing's model, you never see the result of the decision.
Simulating Halt Decider Theorem (Olcott 2021):
Whenever simulating halt decider H correctly determines that input P
REACHnever
aborted) then H correctly decides that P never halts.
(In Turing's model, intermediate states of the tape whilst the machine is running can't be treated as results. What looks like a result might be scratch
space. You have to wait until the machine has halted to read the result).
olcott <NoOne@NoWhere.com> writes:a simulating halt decider
On 10/26/2021 9:28 AM, Ben Bacarisse wrote:
olcott <NoOne@NoWhere.com> writes:
Linz's "proof" that no universal halt decider exists is entirely based >>>> on his belief that H cannot decide ⟨Ĥ⟩ ⟨Ĥ⟩ correctly.It's a proof, not a "proof". It only becomes a "proof" when someone
finds a mistake in it. And it does not rely on his beliefs. That's not >>> the word to use when talking about simple logic like this:
Because this is necessarily true (only a fool would disagree)
Simulating Halt Decider Theorem (Olcott 2021):
Whenever simulating halt decider H correctly determines that input P
never reaches its final state (whether or not its simulation of P is
aborted) then H correctly decides that P never halts.
What is H?
What is P?input to Simulating Halt Decider
What does it mean
to say an input does or does not halt?
Linz's proof does not leave any
of these things unspecified. He defines what H should do in all cases.
He does not introduce new symbols like P without definition. (The last
time you used P it as a scrap of C code, not an input string to a
Turning machine.)
As soon as I show that Ĥq0 <Ĥ> <Ĥ> meets the above theorem then Linz
has been refuted. Only a fool would disagree.
No. You need to point out where Linz goes wrong, not pontificate about
an ill-defined "theorem".
On 10/27/21 9:51 AM, olcott wrote:
On 10/27/2021 8:12 AM, Ben Bacarisse wrote:
olcott <NoOne@NoWhere.com> writes:
On 10/26/2021 6:47 PM, Ben Bacarisse wrote:
olcott <NoOne@NoWhere.com> writes:
All you do is assert that H decides ⟨Ĥ⟩ ⟨Ĥ⟩ correctly.
Are you willing to admit that if it is shown that H correctly decides >>>>>> the halt status of ⟨Ĥ⟩ ⟨Ĥ⟩ that Linz has been refuted or are you
going
to dishonestly dodge this key point?
I keep trying not to dodge it but you keep ignoring my answer. No
proof
is invalided by other truths. You might render all of mathematics
inconsistent, but previously valid chains of reasoning remains valid. >>>>>
You made it plain that don't accept what a proof is when you stated
that
if A,B,C ⊦ X, then ~A,A,B,C ⊬ X. As far as I know you have never >>>>> retracted this incorrect statement.
As it happens, you can't show that Linz's H is correct about the input >>>>> ⟨Ĥ⟩ ⟨Ĥ⟩, so the point is moot, but I have been trying to get you to
note
my answer to this hypothetical question for years, but you keep
pretending not to notice.
I ask you a YES / NO question and you dodge.
How could you miss the answer yet again? Clearly it's no: I don't
accept that if it is shown that H correctly decides the halt status of
⟨Ĥ⟩ ⟨Ĥ⟩ that Linz has been refuted.
So you reject the idea of a semantic tautology.
If X says Y is true and I prove that Y is false then X could still be
correct. No wonder we are having trouble communicating, you are simply
irrational.
Perhaps in smaller words so you can understand.
IF we have one proof that says X.
And we then come up with another proof that says Not X.
That second proof does NOT 'disprove' the first proof.
| Sysop: | Keyop |
|---|---|
| Location: | Huddersfield, West Yorkshire, UK |
| Users: | 427 |
| Nodes: | 16 (2 / 14) |
| Uptime: | 35:19:51 |
| Calls: | 9,029 |
| Calls today: | 12 |
| Files: | 13,384 |
| Messages: | 6,008,861 |