Re: Proving a negative is hard

From: George Greene (greeneg_at_cs.unc.edu)
Date: 08/19/04 

Date: 19 Aug 2004 10:01:32 -0700

Mitch Harris <harrisq@tcs.inf.tu-dresden.de> wrote in message news:<2ojchaFb661oU1@uni-berlin.de>...
 
> LoopIfHalts uses a generic halt analyzer, that's shorthand
> for "for all possible halt analyzers (with the implicit
> nuance that these are all -correct- halt analyzers), the
> very allowable construction of LoopIfHalts causes a
> contradiction.

You're missing the point. The fact that LoopIfHalts uses
a halt analyzer is irrelevant to the causing of the
contradiction. As long as "Loop" is *defined* as the
*opposite* of "Halt", i.e., you Loop on an input iff
you don't Halt on it, then LoopIffHalts(LoopIffHalts)
produces a contradiction. If you can FORM THIS CALL AT ALL,
then you have a contradiction. This proves immediately that
you CAN'T legitimately form this call, not with TMs AND
NOT WITH ANYTHING ELSE EITHER.
> PO:
> > That you can thwart this one case with another one
> > case does not cut it. You must thwart each and every possible
> > case. Proving a negative is much harder than proving a positive.
> > I need only one case, your's must apply to infinitely many cases.

And IT DOES. The argument above applies to ALL THE INFINTELY
MANY WAYS in which ANYone MIGHT construct "LoopIffHalts".
It doesn't matter whether its with Turing machines or with
nail clippings from your left big toe: it's STILL a contradiction.

MH:
> and, if we happen to be talking about the same thing, it
> -does- apply to infinitely many cases (of possible halt
> analyzers) no matter what purported halt analyzer you
> present, LoopIfHalts will result in the same behavior.

Or, at any rate, it will result in a contradiction if it tries
to analyze itself. But again, it's not correct, it's not actually
LoopIffHalts, UNLESS it correctly loops on EVERY program-being-
analyzed that does in fact halt, and inversely.

The point is that there is a trivial easy proof that LoopIffHalts
CAN'T BE WRITTEN, and the proof is, "If it could, what would
LoopIffHaltsOnItself(LoopIffHaltsOnItself) do?
Would it Loop or would it Halt?"

PO is so stupid that he hasn't even understood THAT proof.

AFTER you prove that, you can show that if WillHalt could be
written, then LoopIffHalts unavoidably/necessarily would have
to be writeable as well, and we already know that THAT's a contradiction.

It doesn't matter how many other treatments PO may have seen at nerp
or at nist or even in the original paper by Turing. THIS is what's
REALLY going on. Though actually the original treatment at nerp
is a lot like this, just forward instead of backward.

Relevant Pages