It depends on the theory you’re working with. The set of real numbers can be axiomatized using thirteen axioms that merely say that it’s a totally ordered field whose every non-empty subset has a least upper bound. These 13 axioms allow you to prove a whole lot of interesting stuff about real numbers, and yet they constitute a decidable theory, though with wildly intractable complexity. However, this theory makes it impossible to construct a formula saying “x is an integer” (unless you move to second-order logic).
On the other hand, you can start with set theory, use it to construct natural numbers (i.e. define a set and a relation which can be proven to satisfy the Peano axioms), and then use that to construct a set that can be shown to satisfy the thirteen real-number axioms. This can be done in several ways, for example via Dedekind cuts (in which case the reals are defined as partitions of the set of rational numbers, which are in turn equivalence classes of pairs of integers, which are themselves equivalence classes of pairs of natural numbers). Here, of course, you can talk about natural numbers and integers, but you’ve been working all along in set theory, which is undecidable.
(More precisely, when you construct real numbers in set theory, you end up with multiple isomorphic sets satisfying Peano axioms: the “original” natural numbers, and the subsets of the subsequently defined integers, rationals, and reals that are isomorphic to them. However, at each step, you can construct formulas that will distinguish the subsets corresponding to the previously defined sets in the newly constructed one.)
So, basically, expressing propositions of the sort “there exists x such that x is an integer and P(x)” is possible with real numbers constructed in the undecidable set theory, but it’s not possible in the decidable theory of real numbers based on the 13 axioms.
It depends on the theory you’re working with. The set of real numbers can be axiomatized using thirteen axioms that merely say that it’s a totally ordered field whose every non-empty subset has a least upper bound. These 13 axioms allow you to prove a whole lot of interesting stuff about real numbers, and yet they constitute a decidable theory, though with wildly intractable complexity. However, this theory makes it impossible to formulate a predicate saying “x is an integer” (unless you move to second-order logic).
Technical nitpicking—this doesn’t quite make sense; one of the axioms needed to characterize R is the existence of least upper bounds, which if you’re only talking about R rather than set theory is second order. Of course the resulting first-order theory can’t distinguish integers, but let’s note that without set theory you have to allow second-order logic to see just what this first-order theory consists of.
Of course, at a first-order level, R is indistinguishable from any real closed field, so you could do a true first-order axiomatization that way.
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.)
It depends on the theory you’re working with. The set of real numbers can be axiomatized using thirteen axioms that merely say that it’s a totally ordered field whose every non-empty subset has a least upper bound. These 13 axioms allow you to prove a whole lot of interesting stuff about real numbers, and yet they constitute a decidable theory, though with wildly intractable complexity. However, this theory makes it impossible to construct a formula saying “x is an integer” (unless you move to second-order logic).
On the other hand, you can start with set theory, use it to construct natural numbers (i.e. define a set and a relation which can be proven to satisfy the Peano axioms), and then use that to construct a set that can be shown to satisfy the thirteen real-number axioms. This can be done in several ways, for example via Dedekind cuts (in which case the reals are defined as partitions of the set of rational numbers, which are in turn equivalence classes of pairs of integers, which are themselves equivalence classes of pairs of natural numbers). Here, of course, you can talk about natural numbers and integers, but you’ve been working all along in set theory, which is undecidable.
(More precisely, when you construct real numbers in set theory, you end up with multiple isomorphic sets satisfying Peano axioms: the “original” natural numbers, and the subsets of the subsequently defined integers, rationals, and reals that are isomorphic to them. However, at each step, you can construct formulas that will distinguish the subsets corresponding to the previously defined sets in the newly constructed one.)
So, basically, expressing propositions of the sort “there exists x such that x is an integer and P(x)” is possible with real numbers constructed in the undecidable set theory, but it’s not possible in the decidable theory of real numbers based on the 13 axioms.
Technical nitpicking—this doesn’t quite make sense; one of the axioms needed to characterize R is the existence of least upper bounds, which if you’re only talking about R rather than set theory is second order. Of course the resulting first-order theory can’t distinguish integers, but let’s note that without set theory you have to allow second-order logic to see just what this first-order theory consists of.
Of course, at a first-order level, R is indistinguishable from any real closed field, so you could do a true first-order axiomatization that way.
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.)