Imagine Peano Arithmetic extended with a modal operator $P_{n}^{\ge a/b}$, where $n$ is a variable possibly appearing free in the following expression and $a$ and $b$ are term symbols. Let $F_n$ denote a formula in which no other variables except $n$ appear free, and $F_n(k)$ denote the substitution of $n$ by $S^k 0$ (that is, $SSS \dots 0$, the numeral $k$) in $F_n$, so each $F_n(k)$ is a fully-quantified formula. The intended meaning of the formula $P_{n}^{\ge a/b} F_n$ is that if we pick a random natural number $r$ then the probability that $F_n(r)$ is true is at least $\frac{a}{b}$, and this interpretation is expressible in ZFC: there exists an algorithmically random real number $x$ such that for all $k$, $\lfloor x \cdot b^k \rfloor \space \text{mod} \space b \lt a \rightarrow \text{True}(F_n(k))$.
This yields a truth definition for every formula so the theory is consistent and has $\mathbb{N}$ as a model as long as it's axiomatized with true statements. And I can prove some non-trivial statements in the theory itself by axiomatizing it along with instances of the modal operator's truth definitions, for example that $P_n^{\ge S0/SS0}\Omega \land P_n^{\ge S0/SS0}\neg\Omega$ where $\Omega$ is a PA-formula claiming that the $n^{\text{th}}$ bit of a provable Chaitin constant is $1$. Also a similar statement about the theory's own Chaitin constant can be proved: $P_n^{\ge S0/SS0}\overline{\Omega_{MPA}} \land P_n^{\ge S0/SS0}\overline{\neg\Omega_{MPA}}$ where the overbar denotes the dyadic dual formula describing the same real but not as a binary sequence ending in all $0$'s.
I'm looking for more information about this modal probablistic arithmetic theory. First of all does this theory have a standard name? And next is there maybe any nice introductory paper about it? I have read this section of SEP about modal probability logics which starts off talking about a similar system but I did not find it very useful. So anything at all about the theory that is interesting would be welcome.