The real numbers surely include the integers, but whether “the theory of real numbers” includes “the theory of the integers” depends on what you mean. By “the theory of real numbers” people often mean those aspects of the real numbers you can reason about using finite combinations of arithmetic signs and inequalities. Whether or not you can reason about integers starting from the ability to reason about real numbers depends on whether you can cut out the set of integers from the set of real numbers according to these rules, i.e. whether the integers are a “definable subset” of the real numbers according to our “first order theory of real numbers”. It’s easy to see they aren’t: i.e. the integers are not the solutions to any finite system of polynomial equations and inequalities.
Interesting. Does it mean that e.g. a proposition “there is an integer x which solves the equation exp x=57.24” can’t be formulated inside a theory of real numbers because there is no way how to encode the word “integer”? Or is the problem more subtle?
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 cannot be formulated with the first-order theory of the real numbers with addition and multiplication. It is easily formulated within, say, the second-order theory of the real numbers (n is a whole number iff it’s in every subset S of R such that 0 is in S and, for every m in S, m+1 is in S), or within the first-order theory of the complex numbers if you allow not only addition and multplication but also exponentiation (n is an integer iff for every z such that e^z=1, e^nz is also 1).
I don’t even understand what you’re talking about when you speak of algorithms on real numbers. Computers can’t work with real numbers. Are you assuming some sort of hypercomputation, like a Blum-Shub-Smale computer? Or how are you restricitng your input? (Computable reals, via taking a Turing machine as input? Definable reals handled… somehow?)
(Of course, my answer to any of those questions is “I don’t know, this isn’t really my area, but you could probably look it up pretty easily”—but my point is that your question doesn’t seem to make sense as asked.)
In any case, we’re just talking about defining subsets here, not computing them. There’s a pretty big gap between being first-order-definable and being computable. And that “first condition” is the same as being a whole number so you could just ask that.
Your questions seem to be predicated on a number of confusions. I think you should really go back and read some standard stuff on this first.
EDIT a few minutes later: Of course, if you stick to first-order stuff, then reals are equivalent to definable reals, or to just computable reals—or to just algebraic reals, even—so perhaps your question could be formulated there? But it still seems ill-founded, i.e., I doubt it gets at what you actually want to know. You seem to be confused about the distinction between computation, first-order description, and description more generally.
A little more subtle, I think. Recall that the key idea in Godel’s proof was ’Godelization”—he exhibited an algorithm which matched each sentence about arithmetic in some formal language with a particular natural number. And he also exhibited an algorithm going in the opposite direction—given any number (or formula representing a number), it would either tell you that the number does not correspond to a sentence, or it would tell you what sentence that number represents.
Now suppose we tried to duplicate this with real numbers. Our language still has only a countable number of sentences, so we still want to map sentences to integers (or naturals). So all we need is an algorithm—given any real number or formula representing a real number, determine whether that number is an integer. But there is no such algorithm. It isn’t so much a difficulty in simply encoding or defining the word “integer”, it is a difficulty in producing an operational or algorithmic definition of “integer”.
Incidentally, returning to the original Godel and arithmetic, the only way Godel was able to produce an algorithm deciding whether a formula representing a number does or does not also represent a sentence … the only way he could be sure his algorithm terminated, was to assume a standard model of arithmetic. I.e., count backward and you will eventually get to zero in a finite number of steps. That is, Godel’s undecidable sentence could be assumed either true or false, given the axiomatization of arithmetic. But, also assuming a standard model, that sentence can only be true.
So all we need is an algorithm—given any real number or formula representing a real number, determine whether that number is an integer. But there is no such algorithm. It isn’t so much a difficulty in simply encoding or defining the word “integer”, it is a difficulty in producing an operational or algorithmic definition of “integer”.
Yes, this was approximately what I meant by “encoding the word integer”. Somehow it didn’t occur to me that it may be difficult, or even impossible, to test real numbers for integerness. Still, I am not sure if I understand. A concrete example of a uniquely defined real number whose integerness is unknown would help.
I think you misunderstood. I said there exists no algorithm such that for all formulas it can decide whether the formula represents an integer. Which is equivalent to saying that forall algorithms there exists a formula which can’t be decided.
In other words, the way this game is played, first you specify the algorithm and then I supply the formula that breaks it.
I understood that the algorithm valid for all formulae had to be produced in advance, but still I found it strange that it doesn’t exist. Further thinking about it it doesn’t seem so strange after all.
The real numbers surely include the integers, but whether “the theory of real numbers” includes “the theory of the integers” depends on what you mean. By “the theory of real numbers” people often mean those aspects of the real numbers you can reason about using finite combinations of arithmetic signs and inequalities. Whether or not you can reason about integers starting from the ability to reason about real numbers depends on whether you can cut out the set of integers from the set of real numbers according to these rules, i.e. whether the integers are a “definable subset” of the real numbers according to our “first order theory of real numbers”. It’s easy to see they aren’t: i.e. the integers are not the solutions to any finite system of polynomial equations and inequalities.
Interesting. Does it mean that e.g. a proposition “there is an integer x which solves the equation exp x=57.24” can’t be formulated inside a theory of real numbers because there is no way how to encode the word “integer”? Or is the problem more subtle?
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.)
It cannot be formulated with the first-order theory of the real numbers with addition and multiplication. It is easily formulated within, say, the second-order theory of the real numbers (n is a whole number iff it’s in every subset S of R such that 0 is in S and, for every m in S, m+1 is in S), or within the first-order theory of the complex numbers if you allow not only addition and multplication but also exponentiation (n is an integer iff for every z such that e^z=1, e^nz is also 1).
Thanks. Is there a terminating algorithm which tests the first condition for any given n?
I don’t even understand what you’re talking about when you speak of algorithms on real numbers. Computers can’t work with real numbers. Are you assuming some sort of hypercomputation, like a Blum-Shub-Smale computer? Or how are you restricitng your input? (Computable reals, via taking a Turing machine as input? Definable reals handled… somehow?)
(Of course, my answer to any of those questions is “I don’t know, this isn’t really my area, but you could probably look it up pretty easily”—but my point is that your question doesn’t seem to make sense as asked.)
In any case, we’re just talking about defining subsets here, not computing them. There’s a pretty big gap between being first-order-definable and being computable. And that “first condition” is the same as being a whole number so you could just ask that.
Your questions seem to be predicated on a number of confusions. I think you should really go back and read some standard stuff on this first.
EDIT a few minutes later: Of course, if you stick to first-order stuff, then reals are equivalent to definable reals, or to just computable reals—or to just algebraic reals, even—so perhaps your question could be formulated there? But it still seems ill-founded, i.e., I doubt it gets at what you actually want to know. You seem to be confused about the distinction between computation, first-order description, and description more generally.
A little more subtle, I think. Recall that the key idea in Godel’s proof was ’Godelization”—he exhibited an algorithm which matched each sentence about arithmetic in some formal language with a particular natural number. And he also exhibited an algorithm going in the opposite direction—given any number (or formula representing a number), it would either tell you that the number does not correspond to a sentence, or it would tell you what sentence that number represents.
Now suppose we tried to duplicate this with real numbers. Our language still has only a countable number of sentences, so we still want to map sentences to integers (or naturals). So all we need is an algorithm—given any real number or formula representing a real number, determine whether that number is an integer. But there is no such algorithm. It isn’t so much a difficulty in simply encoding or defining the word “integer”, it is a difficulty in producing an operational or algorithmic definition of “integer”.
Incidentally, returning to the original Godel and arithmetic, the only way Godel was able to produce an algorithm deciding whether a formula representing a number does or does not also represent a sentence … the only way he could be sure his algorithm terminated, was to assume a standard model of arithmetic. I.e., count backward and you will eventually get to zero in a finite number of steps. That is, Godel’s undecidable sentence could be assumed either true or false, given the axiomatization of arithmetic. But, also assuming a standard model, that sentence can only be true.
Yes, this was approximately what I meant by “encoding the word integer”. Somehow it didn’t occur to me that it may be difficult, or even impossible, to test real numbers for integerness. Still, I am not sure if I understand. A concrete example of a uniquely defined real number whose integerness is unknown would help.
I think you misunderstood. I said there exists no algorithm such that for all formulas it can decide whether the formula represents an integer. Which is equivalent to saying that forall algorithms there exists a formula which can’t be decided.
In other words, the way this game is played, first you specify the algorithm and then I supply the formula that breaks it.
I understood that the algorithm valid for all formulae had to be produced in advance, but still I found it strange that it doesn’t exist. Further thinking about it it doesn’t seem so strange after all.