Oh, I see. So you’re replacing the usual completenes axiom for sets with a completeness schema for predicates. I hadn’t considered that. Presumably that works. Never mind. I was interpreting it as actually using sets and thereby introducing either second-order stuff or set theory.
Hm… looking at the literature, it seems like I was wrong after all. (My knowledge of this stuff is very rusty.)
There is indeed something essentially second-order about the completeness axiom. Namely, the second-order quantification over sets of reals uniquely characterizes real numbers in a way that is impossible for any first-order theory, because it eliminates countable models, which every first-order theory with countably many axioms must have as per Loewenheim-Skolem. So turning the second-order completeness axiom into a first-order axiom schema does change things.
Reading a bit further about the decision procedures for the theory of real numbers, I notice that all these sources use a different axiomatization that replaces the completeness axiom with two axioms, namely one stating that every non-negative number has a square root and a schema stating that every polynomial of odd degree has a zero. Now, the question is: is this theory equivalent to the first-order one in which the second-order completeness axiom is replaced by a first-order schema as I imagined? If not, then what I wrote above is completely wrong. I’ll have to read more about this.
Edit: According to the Stanford Encyclopedia of Philosophy entry on second-order logic:
Suppose that, by analogy, we start from our second-order axiomatization of the ordered field of real numbers, and replace the second-order least-upper-bound axiom by the corresponding schema. The result is an infinite set of first-order axioms, assuring that any definable set that is non-empty and bounded has a least upper bound. The models of this are called real-closed ordered fields.
The same term “real-closed ordered fields” is used in the literature for the above mentioned axiomatization that replaces the second-order completeness axiom with the square-root axiom and the odd-order polynomial zero axiom schema. This would suggest that they are equivalent after all. However, I was unable to find a clear and explicit statement confirming this anywhere, which I find puzzling.
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.)
Oh, I see. So you’re replacing the usual completenes axiom for sets with a completeness schema for predicates. I hadn’t considered that. Presumably that works. Never mind. I was interpreting it as actually using sets and thereby introducing either second-order stuff or set theory.
Hm… looking at the literature, it seems like I was wrong after all. (My knowledge of this stuff is very rusty.)
There is indeed something essentially second-order about the completeness axiom. Namely, the second-order quantification over sets of reals uniquely characterizes real numbers in a way that is impossible for any first-order theory, because it eliminates countable models, which every first-order theory with countably many axioms must have as per Loewenheim-Skolem. So turning the second-order completeness axiom into a first-order axiom schema does change things.
Reading a bit further about the decision procedures for the theory of real numbers, I notice that all these sources use a different axiomatization that replaces the completeness axiom with two axioms, namely one stating that every non-negative number has a square root and a schema stating that every polynomial of odd degree has a zero. Now, the question is: is this theory equivalent to the first-order one in which the second-order completeness axiom is replaced by a first-order schema as I imagined? If not, then what I wrote above is completely wrong. I’ll have to read more about this.
Edit: According to the Stanford Encyclopedia of Philosophy entry on second-order logic:
The same term “real-closed ordered fields” is used in the literature for the above mentioned axiomatization that replaces the second-order completeness axiom with the square-root axiom and the odd-order polynomial zero axiom schema. This would suggest that they are equivalent after all. However, I was unable to find a clear and explicit statement confirming this anywhere, which I find puzzling.
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.)