[FOM] Computing roots of a polynomial (was: isomorphism as identity)

[Andrej Bauer]

On Sun, May 24, 2009 at 5:55 AM, Vaughan Pratt <pratt at cs.stanford.edu> wrote:
> The assertion that a Turing machine either
> halts, blocks (cannot proceed but its finite state control is not in the
> set F of final states), or diverges (runs forever) is part of the theory
> of Turing machines, regardless of whether the theory makes any claim to
> be intuitionistically acceptable.

In intuitionistic theory you need to be a bit more careful how you
phrase things. Consider the following statements:

(A) Every Turing machine stops, block or diverges.

(B) Every Turing machine which does not diverge either stops or blocks.

(C) Every Turing machine which dot not stop or block must diverge.

Classically these are equivalent. Intuitionistically (A) => (B) =>
(C), but reverse implications cannot be proved intuitionistically.
Furthermore, (A) is equivalent to Bishop's lesser principle of
omniscience, (B) to Markov principle, and (C) is intuitionistically
provable. Therefore, a classically insignificant change is needed in
your statement to make it true, namely:

"The assertion that a Turing machine which does not stop or block must diverge
is part of the theory of Turing machines, regardless of whether the theory makes
any claim to be intuitionistically acceptable."

With kind regards,

Andrej