Re: Formal systems that cannot possibly be incomplete except for unknowns and unknowable

Richard Heathfield <rjh@cpax.org.uk> writes:
...

Having been on the receiving end of lengthy Usenet diatribes by cranks in
my own field, I don't hold out much hope for our current culprits
developing either the capacity for clear thought or any measure of respect
for expertise any time soon.
>
Nor do I believe they are capable of understanding proof by contradiction,
which is just about the easiest kind of proof there is. In fact, the most
surprising aspect of this whole affair is that (according to Mike)

It was me, but Mike may well have pointed it out recently.

Mr
Olcott seems to have (correctly) spotted a minor flaw in the proof
published by Dr Linz. How can he get that and not get contradiction? Proof
by contradiction is /much/ easier.
>
Let us say we have a hypothesis X. If it is false, we might prove its
falsity in any number of 'positive' ways. But proof by contradiction takes
a different track.
>
We begin by assuming that X is true.
>
Then we show that IF X is true, it necessarily entails Y, where Y is
self-evidently a load of bollocks. From this we deduce that X is false.
>
That's all there is to it.

As I am sure you know, that it not all there is to it, but I digress...

In the present case, X is the proposition that a computer can answer any
question that we can present to it.

That's way too vague!!  Questions like "what are next week's lottery
numbers?" don't need much of proof.  In this case, the proposition is
something like

  There exists a TM, H, that computes h(n, i).

To be specific, all TMs over some alphabet are numbered in lexicographic
order so h is just a function from N x N to {true, false}.  h(n, i) is
true if TM number n halts when given a tape containing the encoding of
the number i in the TM alphabet.

Turing constructed the Halting Problem to illustrate that IF X were true it
would necessarily be false - a contradiction. Conclusion: X is bollocks.
>
The proof couldn't be simpler. If Messrs Flibble and Olcott don't
understand it by now, they never will.

To be fair, when I used to teach this, I did not like using proof by
contradiction.  By that time (second term of the second year) CS
students seemed to have developed the idea that anything that could be
precisely specified could be implemented.  The function h was so clearly
specified (TM number n only performs a finite number of state
transitions from its initial configuration) that the proof assumption
was hard for some students to reject.

But there is a simple direct proof using a diagonal argument.  In
effect, we prove that, for all n, the function computed by TM number n
differs from h for at least one element of h's domain.  That element is,
of course, constructed in the usual way.  And just to drive the point
home, one can go on to show that every TM fails to compute h over an
infinite subset of h's domain -- no TM even comes close!

It helped, at this point, to remind the students that this is not at all
surprising.  There are only countably many TMs, but there are
uncountably many functions from N to {true, false} (let alone from N x N
to {true false}).  The non-computable ones literally out number the
computable ones.

Another thing I used to do was to set Post's Correspondence Problem
(though I never named it) as a programming task on day one of the course
"just because there's so little fun programming in a formal course like
this".  The idea was that the students would gradually find out that
it's mysteriously difficult to even imagine a solution, let alone code
one up.  I never left it too long before coming clean, but even so I
stopped doing this after a couple of years as the deception involved
didn't sit well with me.  But the example of a simple to specify but
impossible to implement program is a very useful one, and I always
brought it up later even after I stopped setting it as an exercise.

Another example, more closely related to halting, is the Busy Bee
function.  This has the additional advantage that Rado's original proof
(that no TM can compute it) gives an entirely different way to prove the
halting theorem.  PO has been urged to look at that proof as well, but
of course he hasn't.

--
Ben.