Self-contained formalization of random variables? I have not been able to find any formalization of random variables that supports construction of new random variables dependent on previously constructed ones. In what I have found, a random variable $A$  is a measurable function from a fixed probability space $(Ω,F,P)$ to a measurable space $(X,E)$. But that means that we have to fix $Ω$ first before we can define $A$. If later we want to define another random variable $B$ that depends on $A$, we are stuck. I know that in many cases we can 'backtrack' and define $Ω$ to accommodate all the random variables that we want to have, but I want to know if it is possible to avoid that, and I would love to know of any references. I believe it may be possible to do it by defining a random variable to carry a set of probability spaces that it depends on, rather than just one probability space, but I am unable to find any reference for such a notion.
For example, what if I want a definable function $f$ on the ordinals such that $f(k)$ for each ordinal $k$ is a random variable that with probability $1/3$ is an independent uniformly random bit and otherwise is equal to the parity of the minimum ordinal $m$ such that there is an increasing function $g : k_{≥m}{→}k$ satisfying $∀i{∈}k_{≥m}\ ( \ g(i)<i ∧ f(g(i)) = f(i) \ )$? This seems conceptually well-defined, but we definitely cannot hope to have a sample space large enough to accommodate it.
To make clear what I am looking for, is there a definable class $RV$ (over ZFC) of random variables, such that we can state things like ( for every real-valued $A,B∈RV$ there is some $C∈RV$ such that $C = A$ with probability $1/3$ and $C = B$ with probability $1/3$ and $C = A+B$ with probability $1/3$ ). By "... with probability ..." I mean that we have a definable function $peq$ (over ZFC) that maps each pair of random variables to the probability that they are equal, and so we would literally have the theorem (where $RRV$ is the class of real random variables on which addition is definable):
  $∀A,B{∈}RRV\ ∃C{∈}RRV\ ( \ peq(A,C) = peq(B,C) = peq(A+B,C) = 1/3 \ )$.
This we cannot do if we do not have a self-contained formalization of random variables. Of course, we must also have all other properties of random variables. So an answer would have to show how to set up both $RV$ and suitable definable functions that allow us to carry out probability theory axiomatically.
After I added the second example above, an answer was posted that works for real random variables each with finite dependencies. But the method used is simply to create a large enough sample space to accommodate all of those random variables, so it cannot handle my first example (an $Ord$-length sequence of dependent random variables).
Here is an anecdote from Fremlin (Measure Theory Chapter 27): "[A probabilist] did not believe in the space $Ω$ in the first place, and if it turns out to be inadequate for his intuition he enlarges it without a qualm. Loève calls probability spaces ‘fictions’, ‘inventions of the imagination’ in Larousse’s words; they are necessary in the models Kolmogorov has taught us to use, but we have a vast amount of freedom in choosing them, and in their essence they are nothing so definite as a set with points." In a similar sense, the motivation for my question is to formalize random variables so that no 'enlargement' of any sample space is necessary.
 A: $\newcommand\Om\Omega\newcommand\ga\gamma$
I think all you need to do is clarify/formalize the terms you are using.
Given a measurable space $(X,E)$, let us say that random variables (r.v.'s) $A_1$ and $A_2$ with values in $(X,E)$ defined on probability spaces $(\Om_1,F_1,P_1)$ and $(\Om_2,F_2,P_2)$ are equivalent if they have the same distributions (that is, pushforward measures): $P_1A_1^{-1}=P_2A_2^{-1}$.
Then, for each measurable space $(X,E)$, there is a natural one-to-one correspondence between the set of all probability spaces $(X,E,\mu)$ over the given measurable space $(X,E)$ and the set of all equivalence classes of r.v.'s with values in $(X,E)$. This follows because, for any probability space $(X,E,\mu)$, the identity map of $X$ is a r.v. defined on the probability space $(X,E,\mu)$ with values in $(X,E)$, and the distribution of this identity map is $\mu$.
Now, when you say "we want to define another random variable $B$ that depends on $A$" (in a certain way), the only natural interpretation of this seems to be the following: you have/know the probabilities of the "joint events" of the form $\{A\in S,B\in T\}:=(A,B)^{-1}(S\times T)$ for some measurable spaces $(X,E)$ and $(Y,F)$, all $S\in E$, and all $T\in F$. In other words, you have/know the "joint" distribution (say $\ga$) of a random pair $(A,B)$ in some measurable space of the product form $(X\times Y,E\otimes F)$, and you want to have a probability space on which a random pair $(A,B)$ with distribution $\ga$ is to be defined.
Well, then you need to do almost nothing: as in the previous paragraph, just let $(A,B)$ be the identity map of $X\times Y$. Then $(A,B)$ will be a r.v. defined on the probability space $(X\times Y,E\otimes F,\ga)$ with values in $(X\times Y,E\otimes F)$, and the distribution of this identity map will be $\ga$. Added: In particular, each of the so-defined r.v.'s $A$ and $B$ will be defined on the probability space $(X\times Y,E\otimes F,\ga)$: $A$ is the map $X\times Y\ni(x,y)\mapsto x\in X$ and $B$ is the map $X\times Y\ni(x,y)\mapsto y\in Y$.
Similarly one can deal with any family of r.v.'s in place of a random pair $(A,B)$.

A short summary: once you have the joint distribution of all your random variables, you automatically and effortlessly have a probability space on which all your random variables can be defined. And if you do not have the joint distribution, then you cannot construct appropriate random variables.

Response to the comment by the OP:
You wrote: "What your last paragraph is saying is that, given any desired joint distribution of a conceptual set of random variables (it isn't a set since we haven't constructed them yet), there exists random variables with that joint distribution. I agree, but this is precisely what I want to avoid."
I think your language is very imprecise. First here, it does not make sense to talk about the "joint distribution of a [...] set of random variables". In particular, the phrase "the joint distribution of the set $\{A,B\}$ of r.v.'s" has no meaning. Instead, we may want to talk about the joint distribution of the random pair $(A,B)$ (which is in general different from that of $(B,A)$) or of the random pair $(A,A)$ (rather than of the set $\{A,A\}=\{A\}$). More generally, we can talk about the joint distribution of any family (not set!) of r.v.'s.
Next, the existence of a family of r.v.'s with a given joint distribution is a (very simple) fact, and you cannot possibly avoid facts, even if "this is precisely what [you] want to avoid."
You also wrote: "Can you address my suggested idea that a random variable carries a set of probability spaces instead of just one? Then we do not need to modify the probability space in random variable $A$ when constructing another random variable $B$ that depends on $A$."
I think your idea for a r.v. to "carry" a set of probability spaces instead of just one was addressed in the beginning of my answer, by suggesting to consider the equivalence classes of r.v.'s (defined on possibly different probability spaces) with the same distribution. So, as now noted in the Added sentence above, if you have a r.v. $B$ in addition to $A$, you don't need to modify anything; you can just automatically and immediately choose a certain probability space (namely, $(X\times Y,E\otimes F,\ga)$), which is one of the probability space "carried by $A$".
A: $\newcommand{\om}{\omega}
\newcommand{\Om}{\Omega}
\newcommand{\N}{\mathbb N}
\newcommand{\la}{\lambda}
\newcommand{\si}{\sigma}
\newcommand{\R}{\mathbb R}$
The latest clarification by the OP appears useful, giving rise to the following construction.

Define the class $RV$ as follows.
Let $\Om:=\{0,1\}^\N$, let $F$ be the Borel $\si$-algebra with respect to the product topology over $\Om$, and let $P$ be the product probability measure $\la^{\otimes\N}$, where $\la$ is the uniform distribution on $\{0,1\}$. Clearly, the probability space $(\Om,F,P)$ is isomorphic to the Lebesgue probability space over the interval $[0,1]$.
Say that a subset $S$ of $\N$ is thin if the cardinality of $S\cap[n]$ is $o(n)$ as $n\to\infty$, where $[n]:=\{1,\dots,n\}$.
Let now $RV$ be the set of all (say real-valued) random variables (r.v.'s) $A$ defined on the probability space $(\Om,F,P)$ such that for some thin $S=S_A\subset\N$, some Borel function $f=f_A\colon\{0,1\}^S\to\R$, and all $\om\in\Om$ we have
$$A(\om)=f(\om|_S);$$
that is, $A\in RV$ iff $A(\om)$ depends only on the values of the function $\om$ on a thin subset $S$ of $\N$.
Clearly, for any $k\in\N$, any r.v.'s $A_1,\dots,A_k$ in $RV$, and any Borel function $g\colon\R^k\to\R$, we have $g(A_1,\dots,A_k)\in RV$. This follows because the union of finitely many thin subsets of $\N$ is thin.
Moreover, for any $k\in\N$ and any probability distribution $\nu$ on $\R^k$, there are r.v.'s $A_1,\dots,A_k$ in $RV$ such that the "joint" distribution of $(A_1,\dots,A_k)$ is $\nu$. This follows because there are infinite thin subsets of $\N$.
Further, for any countable set $T$ and consistent family of finite-dimensional probability distributions on $\R^S$ indexed by finite subsets $S$ of $T$, there is a family $(A_t)_{t\in T}$ of r.v.'s in $RV$ with the given finite-dimensional distributions. This follows because there is a countable set of disjoint infinite thin subsets of $\N$.
Furthermore, for any r.v.'s $A$ and $B$ in $RV$ there is a r.v. $K\in RV$ such that $K$ is independent of $(A,B)$ and $P(K=1)=P(K=2)=P(K=3)=1/3$. Letting then
$$C:=A\,1(K=1)+B\,1(K=2)+(A+B)\,1(K=3),$$
we get a r.v. $C\in RV$ such that "$C$ is $A$ with probability $1/3$, $C$ is $B$ with probability $1/3$, and $C$ is $A+B$ with probability $1/3$", as desired.

In view of the Borel isomorphism theorem, here instead of real-valued r.v.'s we may consider r.v.'s with values in arbitrary Polish spaces.
A: Proposition: Let $\kappa$ be some infinite number cardinal number. There exists a probability space $(\Omega,\Sigma,\nu)$ that carries $\kappa$ independent random variables with uniform distribution on $[0,1]$ and such that
such for every family $\langle g_i\rangle_{i\in I}$ of real-valued random variables with $\#I\leq\kappa$ and every probability measure $\mu$ on $\mathbb{R}^I\times\mathbb{R}^J$ with $\#J\leq\omega$ and $\mathbb{R}^I$-marginal equal to the joint distribution of $\langle g_i\rangle_{i\in I}$, there exists a family of random variables $\langle g_i\rangle_{i\in J}$ such that the joint distribution of $\langle g_i\rangle_{i\in I\cup J}$ equals $\mu$. $$~$$
One can take
$\Omega={0,1}^{\kappa^+}$, $\Sigma$ the product-$\sigma$-algebra, and $\nu$ the fair coin-flipping measure. The proposition can be proven using ideas from this paper.
The proposition shows that one can find a probability space that can carry a lot of nontrivial random variables and such that one can always add ex-post a countable number of random variables at a time whose distribution relates in any way to the other random variables. One never runs out of space; there is no need to enlarge the underlying probability space.
This is probably more than enough for any reasonable probabilistic argument, but works with only set-many random variables. If one wants to do this with random variables indexed by the class of ordinals, one could do this by viewing the class of all sets as a genuine set in a larger universe that contains a strongly inaccessible cardinal; this seems to be the preferred method of foundation-conscious category theorists for dealing with similar size problems.
A: Not an answer, but too long for a comment.

*

*Although by definition a random variable is a measurable function defined on a probability space, abstract formulation of the concept of a random variable seems, to some extent, possible: one can think of (real- or complex-valued) random variables as elements of a commutative unital $C^*$ algebra, equipped with a linear functional called expectation that sends the unit to $1$. (And if one drops commutativity, one arrives in the world of non-commutative probability.)


*"Functions that take values in the class of random variables" are most commonly called stochastic processes. That is, the second paragraph of your question asks for a stochastic process indexed by a class rather than a set, with given properties. Or — equivalently, I think — a single random variable taking values in the class of $\operatorname{Ord}$-indexed functions (is this a class?). Unfortunately I know next to nothing about foundations of mathematics, and have no idea what the answer is.


*Given the first point of this comment, your question about $\operatorname{Ord}$-indexed stochastic process can be rephrased in the language of $C^*$ algebras — is there a $C^*$-algebra-like object (if I understand correctly, a "definable class") that can accommodate such a process. This makes your question very loosely related to probability, as a similar question can be asked about essentially any other mathematical structure. (I believe this was the source of misunderstanding in your discussion with Iosif Pinelis.)


*The question about the class of all random variables is, I believe, addressed in Michael Greinecker's excellent answer. This approach is, however, extremely exotic for a probabilist like me, and again not really related to probability. (I can give essentially the same questions in the context of, say, finite sets: is there a class of finite sets such that for any two of them there is another one such that it shares exactly one element with both of the two. Is this any simpler?)


*Fremlin's anecdote is perhaps nice, but — believe it or not — this mysterious underlying probability space that nobody cares about is an extremely useful concept in probability theory. No other way of thinking about random variables seems to be more productive. Just like the internal structure in, say, manifold theory is usually well hidden, but still essential.
