Yes, all real closed fields are first-order equivalent; don’t ask me how to prove this, I don’t know. (Well, I’m pretty sure you do it via quantifier elimination, but I don’t know how that actually goes.) When I said “presumably this works”, I meant “presumably this is enough to get all the first-order properties of R”, which is the same thing as saying “presumably this is enough to get a real closed field”. Going by the SEP cite you found, apparently this is so.
Oh, I feel silly—of course it’s enough. Real closedness is equivalent to intermediate value theorem for polynomials, so if you have “first-order completeness” you can just do the usual proof of intermediate value theorem, just for polynomials. (Because after all the topology on R can be described in terms of its order structure, which allows you to state and use continuity and such as first-order statements.)
Yes, all real closed fields are first-order equivalent; don’t ask me how to prove this, I don’t know. (Well, I’m pretty sure you do it via quantifier elimination, but I don’t know how that actually goes.) When I said “presumably this works”, I meant “presumably this is enough to get all the first-order properties of R”, which is the same thing as saying “presumably this is enough to get a real closed field”. Going by the SEP cite you found, apparently this is so.
Oh, I feel silly—of course it’s enough. Real closedness is equivalent to intermediate value theorem for polynomials, so if you have “first-order completeness” you can just do the usual proof of intermediate value theorem, just for polynomials. (Because after all the topology on R can be described in terms of its order structure, which allows you to state and use continuity and such as first-order statements.)