Which axioms from ZF guarantee the existence of a sequence space? For example, the set of all sequences of rational numbers? Or more simply the set of all sequences generated from {0,1}?
The natural numbers are a symbolic representation of the set given to us by the axiom of infinity, called N. Z is an equivalence relation imposed on NxN. Q is an equivalence relation imposed on ZxN. And now to construct R, we need to know that the sequence space of Q exists.
My problem is how do we know in general that a sequence space exists. If we had the definitions in hand of what a sequence is (a function from N to a set X), we could generate any finite set of sequences over the set X from the axiom of union. But from where do we know that we can say that "the set of all sequences" exists and is a set?
you don't NEED the sequence space of Q to define R (although it IS a nice definition), you just need the power set of Q.
real numbers are (or at least CAN be) defined to be certain subsets of rational numbers (the typical example is √2 = {x in Q: x < 0, or x^{2}< 2}) (the "dedekind cut" construction).
however, i see no reason why the unions guaranteed by the axiom of union must be FINITE. rational sequences are just certain subsets of NxQ, which is certainly a set, so we have the set:
{f in P(NxQ): f is a function defined on N}, by the power set axiom, and the axiom of specification.
The problem I had in mine was the construction of R from the completion process of Q (which of course relied on an equivalence relation imposed on Cauchy Sequences of rational numbers). But to impose an equivalence relation to form a quotient set you need the underlying set - the cauchy sequences of Q. And I knew that I could recover that set by the axiom of specification if I knew that the set of all sequences from Q existed. That's where I hit a wall. But Deveno answered that question with {f in P(NxQ) : f is a function with domain N}.