[FOM] Computing roots of a polynomial

[Vaughan Pratt]

On 5/24/2009 12:13 PM, Andrej Bauer wrote:
> 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."

I confess I had not been thinking at that level of precision.  But now 
that you bring it up, I did not intend (A) simply as a disjunction but 
as the statement that exactly one of S, B, or D holds.

1.  Does this change what you say above?

2.  Are you assuming any particular specification of D for your claim 
that (C) is provable?

One might think to define D as not(S or B), in which case (C) is not 
merely intuitionistically provable (from the properties of Turing 
machines) but an instance of P --> P.  In that case even I with my 
limited intuition about intuitionism can see that (C) is 
intuitionistically provable.  :)

But if instead you define D as "every state reached from the initial 
state is a non-final non-blocked state" (assuming a deterministic Turing 
machine), then I have no intuition as to what the intuitionistically 
correct phrasing of (A) should be.

(Although I can calculate formally very well with Heyting algebra, I 
can't do so naturally the way I can with Boolean algebra, and have to 
rely on those with more experience with intuitionistic reasoning.)

Vaughan