(TL;DR version: I want a meaningful definition of $\Bbb{Q}$ without $\sf{Inf}$.)
In the "conventional" construction of the rationals, we define $\Bbb{Q}$ as follows:
- $\omega$ is the first limit ordinal, which can be defined with or without the Axiom of Infinity.
- $\cal{Z}=\omega\times\omega/\sim$, where $\sim$ is an equivalence relation defined by $(a,b)\sim(c,d)\iff a+d=b+c$ using ordinal addition on $\omega$. These form the pre-integers.
- $\cal{Q}=\cal{Z}\times(\omega-\{\emptyset\})/\approx$, where $(a,b)\approx(c,d)\iff ad=bc$ using multiplication on the obvious interpretation of $\cal{Z}$ as $\Bbb{Z}$ and $\omega-\{\emptyset\}$ as $\Bbb{N}^*$. These are the pre-rationals.
- $\Bbb{R}=\{x\mid\emptyset\subset x\subset\cal{Q}\wedge \forall y\in\cal{Q}\,(\exists z\in x\ y<z\to y\in x)\}$ is a relatively simple definition of the reals in terms of Dedekind cuts (although you could easily replace this step with a definition via Cauchy sequences or some other method instead if you wanted). (I'm assuming $<$ has been been defined in the obvious way on $\cal{Q}\times\cal{Q}$.)
- Having defined $+,-,\times,/$ on $\Bbb{R}\times\Bbb{R}$, we find $0$ as the unique $x$ such that $x+x=x$ and $1$ as the unique $x\ne0$ such that $x^2=x$.
- Then $\Bbb{N}_0$ is the closure of $\{0,1\}$ under $+$, and $\Bbb{N}^*=\Bbb{N}_0-\{0\}$.
- $\Bbb{Q}^{>0}$ is the closure of $\Bbb{N}^*$ under $/$, and $\Bbb{Q}$ is the closure of $\Bbb{Q}^{>0}$ under $-$.
I've attempted to be as precise as possible in the actual construction from the beginning (arguably too much so), so that I could make my notation unambiguous (in particular, it seems $\Bbb{N}$ does not have a consistent interpretation, so I've avoided its use). Now it is said that Peano arithmetic is capable of doing most math that does not require infinity in any "essential" way, and indeed $\sf{PA}$ can be proven in $\sf{ZF^\times=ZF-Inf}$. However, the construction above makes use of $\sf{Inf}$ in several different ways, and the following issues come up when working in $V_\omega$ (as a model of $\sf{ZF^\times}$):
- $\omega=\sf{On}$ is no longer a set. This is not a problem per se, but this means that $\cal{Z}$ and $\cal{Q}$ are not sets anymore either, which is expected.
- The two quotient set definitions of $\cal{Z}$ and $\cal{Q}$ each gather together infinitely many elements (i.e. $0_{\cal Z}=\{(0,0),(1,1),(2,2),\dots\}\notin V_\omega$), so the elements are proper classes, and $\cal{Z}$ and $\cal{Q}$ collapse to $\emptyset$.
- Assuming $\cal{Q}$ is somehow "fixed" and the expected properties are restored, each element of $\Bbb{R}$ is likewise an infinite subset of $\cal{Q}$ and thus $\Bbb{R}$ collapses to $\emptyset$, as well as all the dependent subsets $\Bbb{N}_0$, $\Bbb{N}^*$, $\Bbb{Q}^{>0}$, and $\Bbb{Q}$.
This is not a fortuitous state of affairs, as all of these carefully constructed sets collapse to nothing! Now $\Bbb{R}$ is uncountable, so I don't expect to patch that definition up, but I would like to recover enough of either $\Bbb{Q}$ or $\cal{Q}$ to do some algebra on it (at least the field structure), without needing to invoke $\sf{Inf}$ to prove that the elements of $\cal{Q}$ exist. (Secondary goal: it would be nice if one could construct $\Bbb{R}$ and $\Bbb{Q}$ such that $\Bbb{Q}\subseteq\Bbb{R}$, but the elements of $\Bbb{Q}$ exist in $V_\omega$, or barring that, a definition of ${\cal Q}\subseteq V_\omega$ that is sufficiently robust to build $\Bbb{R}$ as indicated. Bonus points for simplicity of definition.)
There are two tricks one can use, both in a very similar fashion.
Both tricks are used at the same points in the same fashion. So instead of referring to one, I'll just use "the trick" which would fit either choice of trick, or any other compatible with the idea of having sets of representatives for proper classes.
Step I: The Integers.
We know that $\Bbb Z$ can be seen as a quotient of $\omega\times\omega$ with the equivalence relation $(a,b)\sim_Z(c,d)\iff a+d=b+c$. Observe that $\omega\times\omega\subseteq V_\omega$, and it is a definable class there. Therefore we can define the equivalence relation.
Using the trick, let $\cal Z$ be the class of representatives, we can define addition and multiplication as usual with one twist that we revert back to our chosen representative. Let $\cal N$ denote the canonical embedding of $\omega$ into $\cal Z$, that is the representatives of $(n,0)$ for $n\in\omega$.
Step II: The rationals.
Now we have a class $\cal Z$ along with two operations, addition and multiplication. And we know that the rationals can be define from the integers by taking a quotient over $\Bbb{Z\times N\setminus\{0\}}$ defined by $(a,b)\sim_Q(c,d)\iff ad=bc$.
In exactly the same fashion as before, one can note that $\cal{Z\times N}$ is a definable class, and use the trick again to define a class $\cal Q$, and its operations and whatnot.
Again I should point out that we define the operations to have a tiny twist, because those are no longer operations on sets which are equivalence classes, we need to refine their definitions to return the correct representative, but this is not a difficult task.
Interestingly enough, if one uses Scott's trick then one ends up having $\cal Q$ as sets of sets of pairs of integers; whereas using the global choice argument one ends up with a subset of $\omega\times\omega$.