Yes, of course, barring second-order logic, the “13 axioms” are in fact twelve plus a countably infinite set of axioms generated by the completeness axiom scheme, just like the Peano axiom of induction is in fact an axiom scheme generating an infinite set of axioms.
However, I’m not sure I understand what you mean when you say that “without set theory you have to allow second-order logic to see just what this first-order theory consists of.” The theory is meant to have the set of real numbers as its universe of discourse, and sets of real numbers correspond to its formulas with one free variable, for which you instantiate the custom completeness axioms in proofs as necessary. What exactly do you need set theory or second-order logic for?
(Also, on a more careful reading, I was a bit loose with terminology in my earlier comment. In first-order logic, you cannot “define predicates,” since their number is fixed in the given language. What I meant is constructing a formula N(x) with one free variable that is satisfied by, and only by, natural numbers.)
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.)
Yes, of course, barring second-order logic, the “13 axioms” are in fact twelve plus a countably infinite set of axioms generated by the completeness axiom scheme, just like the Peano axiom of induction is in fact an axiom scheme generating an infinite set of axioms.
However, I’m not sure I understand what you mean when you say that “without set theory you have to allow second-order logic to see just what this first-order theory consists of.” The theory is meant to have the set of real numbers as its universe of discourse, and sets of real numbers correspond to its formulas with one free variable, for which you instantiate the custom completeness axioms in proofs as necessary. What exactly do you need set theory or second-order logic for?
(Also, on a more careful reading, I was a bit loose with terminology in my earlier comment. In first-order logic, you cannot “define predicates,” since their number is fixed in the given language. What I meant is constructing a formula N(x) with one free variable that is satisfied by, and only by, natural numbers.)
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.)