Wojowu の BIG FOOT を解説した Nathan Ho による "First-order Oodle Theory"  の日本語対訳です。一番の肝となる ordinal \(\text{Ord}\) の定義の方法が載っている "Sets?" と題された項のところだけ訳してみました。もしも間違いがあれば訂正しますのでコメントで書いてください。

2A question arises: how to define sets inside this structure?疑問がひとつ生じます:どうやってこの構造の中で集合を定義するの?
3Turns out, it's impossible.結果を言うと、それは無理なんです。
4Firstly, because "sets" don't even have definition, secondly, oodleverse could as well work out as a universe of sets.まず、「集合」は定義すら持っていないし、もっと言うと、ooldverse のほうがより集合の宇宙としてうまく働くことができます。
5However, if we had some quite large oodinal, which we'll denote \(\text{Ord}\), we could define sets as oodles which have rank \(<\text{Ord}\).しかし、もし大きな oodinal、それを \(\text{Ord}\) と書こうと思いますが、それがないと \(<\text{Ord}\) の階数をもつ oodle として集合を定義することができません。
6We will also call elements of \(\text{Ord}\) ordinals.\(\text{Ord}\) の要素を ordinal と呼びたいわけでもあるのです。
7But the problem now could be, how to choose \(\text{Ord}\) ?しかし問題は、どうやって \(\text{Ord}\) を選べばいいのか?ということになってしまいます。
8Because we want these sets to satisfy some natural properties, we can't choose it in any way we want.なぜなら、私たちはこれらの集合をある自然な性質を満たすようにさせたいわけで、好き勝手な方法で選ぶわけにはいかないです。
9Also, because we know that \(V\) can work as the universe of sets, we want \(V_\text{Ord}\) to satisfy the same statements about sets as \(V\) does about oodles, counting only formulas with parameters in \(V_\text{Ord}\) (we want it to be elementary substructure).それに、ご存知の通り\(V\) は集合の宇宙としてうまく機能できますし、私たちは \(V_\text{Ord}\) を \(V\) が集合についてやっているような文を oodle についても満たしてほしいわけです。
10Here is how we can construct such oodinal \(\text{Ord}\):そんな oodinal である \(\text{Ord}\) の構築の仕方はこのようにします:
11\(\alpha_0\) is the least oodinal which, for every formula \(\Phi\) without parameters, satisfies "if there exists oodinal \(\alpha\) such that \(\Phi(\alpha)\), then there is oodinal \(\beta<\alpha_0\) such that \(\Phi(\beta)\)".\(\alpha_0\) は、引数のないあらゆる論理式 \(\Phi\) について、「もし \(\Phi(\alpha)\) となる oodinal \(\alpha\) が存在するならば、\(\Phi(\beta)\) となる oodinal \(\beta<\alpha_0\)も存在する」を満たす最小の oodinal である。
12Then, if we already have \(\alpha_n\)defined, we define \(\alpha_{n+1}\) as the least oodinal which, for every formula \(\Phi\) and finite collection \(A\) of parameters from \(V_{\alpha_n}\), satisfies "if there exists oodinal \(\alpha\) such that \(\Phi(\alpha,A)\), then there is oodinal \(\beta<\alpha_{n+1}\) such that \(\Phi(\alpha,A)\)".そして、\(\alpha_n\)を定義したら、\(\alpha_{n+1}\) を、あらゆる論理式 \(\Phi\) と \(V_{\alpha_n}\) のパラメータを持つ有限の族Aについて、「もし \(\Phi(\alpha,A)\) となる oodinal \(\alpha\) が存在するならば、\(\Phi(\beta,A)\) となる oodinal \(\beta<\alpha_{n+1}\) も存在する」を満たす最小の oodinal である、と定義します。
13Now we define \(\text{Ord}=\text{lim}_{n\rightarrow \omega}\alpha_n\)そして、\(\text{Ord}=\text{lim}_{n\rightarrow \omega}\alpha_n\)と定義します。
14Now we have to verify that formula \(\Phi(A)\), for\(A\in V_\text{Ord}\) is true in \(V\)  iff it is in \(V_\text{Ord}\).次は、論理式 \(\Phi(A)\) を検証、つまり、\(A\in V_\text{Ord}\) について \(V_\text{Ord}\) の下で \(\Phi(A)\) で真であるときに限り \(V\)  の下でも \(\Phi(A)\) が真であることを検証しなければなりません。
15The verification goes by induction on structure of formula, with only tricky case being existential quantifier.検証は論理式の構造の帰納法で行われますが、存在量化子を使うトリッキーなやり方で済みます。
16So let \(\Phi(A)\)  have form \(\exists x:\Phi(x,A)\).\(\Phi(A)\)  が \(\exists x:\Phi(x,A)\) の形をもつとしましょう。
17Assume this holds in \(V\) .これは \(V\)  の下で成り立つと仮定します。
18Then, there exists \(X\) such that \(\Phi(X,A)\) holds in \(V\) .それなら、\(\Phi(X,A)\) が \(V\)  の下で成り立つような\(X\) が存在します。
19But then, rank of \(X\) satisfies "there exists \(x\) with this rank which makes \(\Phi(x,A)\) true".しかしその場合、\(X\) の階数は「 \(\Phi(x,A)\) が真となるような階数の \(x\) が存在する」を満たすような階数、となります。
20Because \(A\in V_\text{Ord}\)\(A\in V_{a_n}\) for some \(n\).なぜなら、\(A\in V_\text{Ord}\) であり、ある \(n\) に対して \(A\in V_{a_n}\) であるからです。
21So, by construction, there exists an ordinal \(\beta<\alpha_{n+1}<\text{Ord}\) which satisfies the formula, so there exists \(X'\) with rank below \(\text{Ord}\), thus in \(V_\text{Ord}\), which makes \\(\Phi(X',A)\) true, so formula (\Phi(A)\) holds in \(V_\text{Ord}\).よって、その論理式を満たす ordinal \(\beta<\alpha_{n+1}<\text{Ord}\) は存在し、\(\text{Ord}\) 以下の階数をもつ \(X'\) は存在し、それにより \(\Phi(X',A)\) は真となり、よって \(\Phi(A)\) が \(V_\text{Ord}\)の下で真である、となるのです。
22Conversely, assume \(\exists x:\Phi(x,A)\), and let \(\Phi(X,A)\).逆に、\(\exists x:\Phi(x,A)\) の仮定から、\(\Phi(X,A)\) を真としてみましょう。
23By inductive assumption, as \(\Phi(X,A)\) holds in \(V_\text{Ord}\), it holds in \(V\), so \(\Phi(A)\)  holds in \(V\) .\(\Phi(X,A)\) が \(V_\text{Ord}\) の下で真であるという帰納法の仮定から、\(\Phi(X,A)\) は \(V\) の下で成り立ちます。よって \(\Phi(A)\)  も \(V\)  の下で成り立ちます。