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.