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

[Vaughan Pratt]

Daniel Méhkeri wrote:
> I guess we have stumbled on a neat example where classical recursion
> theory and constructive mathematics are at odds: a constructive
> mathematician would disagree that c is rational! (To say
> "either T halts or it doesn't" is of course not kosher.)

It is not a requirement of the theorems of a theory that they all be 
intuitionistic tautologies.  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.

> So it would be correct, as is, to say that for rational coefficients
> the roots are computable, without worry about the representation
> concerns mentioned. 

Yes.  My interpretation of "polynomials with rational coefficients" is 
that they are presented in some decidable representation, which I 
understand to be the usual meaning.  This interpretation is not possible 
for "polynomials with computable coefficients" with the usual notion of 
"computable real."  My answer to Karim was only for the second case he 
asked about, namely computable coefficients.

(This topic seems to come with more than the usual number of logical 
potholes.)

Vaughan Pratt