[FOM] Computing roots of a polynomial

[Andrej Bauer]

I am hoping that my current burst of posts to FOM will soon be over,
so I am only planning to reply once more to Vaughn's specific
questions and stop after that. Assuming we have defined Turing
machines and their executions, the natural definitions of "stops",
"blocks" and "diverges" would be:

"T stops" = there exists an execution step in which the machine is in
a final state

"T blocks" = there exists an execution step in which the machine is
not in a final state and it cannot make progress

"T diverges" = for every excution step, the machine is not in a final
state and it can make progress

Under these definitions my claims from the previous post hold.

Here are some basic observations. Intuitionistically (and therefore
classicaly) it follows from the definition of Turing machines that:

T stops => not (T block) and not (T diverges) => not not (T stops)
T blocks => not (T stops) and not (T diverges) => not not (T blocks)
T diverges <=> not (T stops or T blocks)

The equivalence on the third line answers one of your questions, see below.

> 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.

Normally, the statement that "exactly one of S, B or D holds" means

(S or B or D) and
(S => not B and not D) and
(B => not S and not D) and
(D => not S and not B)

but in our case, using above observations, this reduces just to "S or
B or D" because S, B and D are mutually exclusive. So I think saying
"exactly one of S, B or D holds" is the same as "S or B or D" in our
case.

> 1.  Does this change what you say above?

Well, one just has to be careful about how to say things
intuitionistically. For example, assuming that the set

  {0 | T stops} union {1 | T blocks} union {2 | T diverges}

has a size measured as a natural number entails "T stops or T blocks
or T diverges".

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

The one given above.

> 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.
>
> 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.

The two definitions of "T diverges" that you suggest are equivalent,
as I claimed above. If you would like to see details, I can send them
privately and spare the FOM readers from further details. Briefly, one
uses the fact that "not exists, phi" is intuitionistically equivalent
ot "forall, not phi", and that at every step the machine is either
stopped, blocked, or can make progress.

With kind regards,

Andrej