[FOM] Computing roots of a polynomial (was: isomorphism as identity)
Vaughan Pratt
pratt at cs.stanford.edu
Sat May 23 23:55:18 EDT 2009
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
More information about the FOM
mailing list