"ill-formed" TM descriptions

From: George Greene (greeneg_at_greeneg-cs.cs.unc.edu)
Date: 06/20/04 

Date: 20 Jun 2004 17:12:38 -0400

There are two descriptions of TMs that in natural lanuage look
syntactically so much alike that you would be hard-pressed to allege
that one of these questions was well-formed and the other wasn't.
Assume (harmlessly) that TMs can be coded by individual numbers.

(1)
What is the smallest code of
  a TM that takes (M,w) as input, where M is the code of a TM,
and halts when and only when M DOES halt on w?

This is a well-formed question and it has a well-formed answer; the answer
is the code of the smallest relevant Universal Turing Machine, and there
are plenty of papers in the literature pointing you to explicit definitions
of small Universal Turing Machines.

Now, consider another question differing from this one by ONLY ONE WORD.
In terms of form, these two questions are so similar that you cannot
hope to claim that one of them is well-formed while the other is ill-
formed.
(2)
What is the smallest code of
  a TM that takes (M,w) as input, where M is the code of a TM,
and halts when and only when M DOESN'T halt on w?

There is no smallest code of such TMs because there
ARE NO such TMs. But there are plenty of TMs that are
"correct" for the spec in (1). And the fact that
no program satisfies a given spec does NOT imply
that the spec was "ill-formed".
The fact that there is no r satisfying
Ax[ rRx <-> ~ xRx ]
does NOT mean that that sentence is ill-formed.
It is just FALSE.
It is precisely because it is so WELL-formed that
we can SUCCEED in evaluating its truth-value enough,
or deriving it (or its denial) via inference rules,
to LEARN that it is always false. In the case of the
spec of a Halt(,) TM, it is precisely because the
spec is WELL-formed that we are ABLE to prove about it
that it is unsatisfiable. 

-- 
 --- The history of our nation has demonstrated that separate is seldom, if ever, equal.
 --- (Feb.3,2004) Supreme Judicial Court of Massachusetts (4-3), adv.Sen.#2175

Relevant Pages
Quantcast