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

[Vaughan Pratt]

On 5/24/2009 6:57 PM, Daniel Méhkeri wrote:
> Vaughan Pratt replied:
>> 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.
>
> But isn't it still possible for computable coefficients, since
> constructive witnesses of the antecedents "the computable real x_n is
> rational" would still contain the necessary info for the consequent.
> This might be why your answer and Andrej's were inconsistent.

If by "constructive witness to rationality" you mean "constructive proof 
of rationality," then while it is true that one can have a computable 
real that is provably zero (and hence provably rational), it is also 
true that one can have a computable real that is provably rational but 
not provably zero.  If by "witness" you meant an actual rational then 
I'm not following your reasoning.

I thought the inconsistency between Andrej's answer and mine was simply 
that he was referring to rational coefficients while I was referring to 
computable coefficients.  Andrej can correct me if there's more to it 
than that.  (We disagreed on other points, but not that one as far as 
I'm aware.)

>
> I found it interesting because I recall examples of this sort being
> contrived, where the classical answer is a trivial one along the
> lines of: "if P, then f(x) = +1 is a computable function satisfying
> the requirement, if not-P, then f(x) = -1 is a computable function
> satisfying the requirement." So either way there exists a function
> "computing" the answer, even if we don't know which trivial algorithm
> gives the answer.
>
> This one seems to have come up naturally.

Perhaps it seems more natural because it's an actual example of a 
computable real, which your example isn't if I understand it---it 
doesn't gradually home in on the answer but waits until after P is 
decided to pick 1 or -1.

Vaughan Pratt