ラツィエンにより再構成されたバッハマンの関数 (Bachmann's function recasted by Rathjen) は、ラツィエンにより公開されている The Art of Ordinal Analysis という論文の 15 ページ目に記載されている関数である。
定義[]
\( \Omega \) を都合の良い巨大な順序数とする。例えば \( \omega _ 1 \) などである。
\( C ^ \Omega ( \alpha, \beta ) \) を \( ( \xi, \zeta ) \mapsto \xi + \zeta \) と \( \xi \mapsto \omega ^ \xi \) と \( \xi _ { \_ < \alpha } \mapsto \psi _ \Omega ( \xi ) \) に対する \( \beta \cup \{ 0, \Omega \} \) の閉包とする。
\( \psi _ \Omega ( \alpha ) \) を \( \min \{ \rho < \Omega : C ^ \Omega ( \alpha, \rho ) \cap \Omega = \rho \} \) とする。
定義の解説[]
\( \psi _ \Omega ( \alpha ) \) は超限再帰により定義される。もっと詳しくするならば \( [ \psi _ \Omega ( \alpha ) = \gamma ] \) という \( \alpha \) と \( \gamma \) を取るアリティが 2 の述語に対して、次の論理式が成り立つことが超限帰納法により証明されるという形となるはずである。
\[ \forall \alpha \ldotp \alpha \in \mathrm{On} \rightarrow \exists \gamma \ldotp \gamma \in \mathrm{On} \land [ \psi _ \Omega ( \alpha ) = \gamma ] \land \forall \gamma' \ldotp \gamma' \in \mathrm{On} \land [ \psi _ \Omega ( \alpha ) = \gamma' ] \rightarrow \gamma = \gamma' \]
\( ( \xi, \zeta ) \mapsto \xi + \zeta \) の定義域は \( \rangle \mathrm{On}, \mathrm{On} \langle \) であり \( \xi \mapsto \omega ^ \xi \) と \( \xi \mapsto \psi _ \Omega ( \xi ) \) の定義域は \( \mathrm{On} \) である。 \( \xi _ { \_ < \alpha } \mapsto \psi _ \Omega ( \xi ) \) にある \( \_ < \alpha \) は定義域を \( \alpha \) 未満に制限することを示している。
量化子[]
「ただ一つ存在する」を意味する量化子を次のように定義する。
| 定義 1.1 |
|---|
\( \exists _ 1 x \ldotp P ( x ) \) を \( \exists x \ldotp P ( x ) \land \forall y \ldotp P ( y ) \rightarrow x = y \) の略記とする。 |
順序数[]
順序数のクラス \( \mathrm{On} \) を次のように定義する。
| 定義 2.1 |
|---|
\( \alpha \in \mathrm{On} \) を \( \left( \bigcup \alpha \right) \subseteq \alpha \land \forall x y \ldotp x \in \alpha \land y \in \alpha \rightarrow x \in y \lor x = y \lor y \in x \) の略記とする。 |
この定義は 新井 2016 の 132 ページの定義 4.3.4 に拠る。
| 定義 2.2 |
|---|
\( [ \min X = \alpha ] \) を \( X \in \mathcal{P} ( \mathrm{On} ) \land \alpha \in X \land \forall x \ldotp x \in X \rightarrow \alpha \leq x \) の略記とする。 |
順序数の集合についての最小元の表記を定義する。なお、ここで \( X \) はクラスであっても良いとする。
| 定義 2.3 |
|---|
\( [ \sup X = \alpha ] \) を \( X \in \mathcal{P} ( \mathrm{On} ) \land \bigcup X = \alpha \) の略記とする。 |
順序数の集合についての上限の表記を定義する。
加算[]
定義の基本的なパーツとして順序数の加算がある。順序数の加算は \( [ \alpha + \beta = \gamma ] \) という述語として考えられる。
| 仮定 3.1 |
|---|
\[ \forall \alpha \beta \ldotp \alpha \in \mathrm{On}\land \beta \in \mathrm{On} \rightarrow \exists _ 1 \gamma \ldotp \gamma \in \mathrm{On} \land [ \alpha + \beta = \gamma ] \] |
これは \( [ \alpha + \beta = \gamma ] \) が \( \mathrm{On} \) における関数であることを表す。
| 仮定 3.2 |
|---|
\[ \forall x y z \ldotp x + ( y + z ) = ( x + y ) + z \] ただし、 \( x, y, z \) は \( \mathrm{On} \) の要素である。 |
これは順序数の加算の結合法則を表す。
| 定義 3.3 |
|---|
\( x \in \mathrm{AP} \) を \( \alpha \in \mathrm{On} \land 0 < \alpha \land \forall \alpha \beta \ldotp \alpha \in x \land \beta \in x \land \alpha + \beta < x \) と同値であるとする。 |
加素順序数[note 1] (additive principal number) のクラスを定義する。これはのちの性質を記述するために必要になる。
| 仮定 3.4 |
|---|
\[ \forall x y \ldotp ( \exists z \ldotp z \in \mathrm{AP} \land x < z \land z \leq y ) \leftrightarrow [ x + y = y ] \] ただし、 \( x, y, z \) は \( \mathrm{On} \) の要素である。 |
これは順序数の加算の第二引数における不動点の必要十分条件を示す。
仮定 2.2 と仮定 2.4 を使えば順序数の加算に関する標準形を計算できるはずである。ある \( x \) に対して \( \min \{ y \in \mathrm{AP} : x < y \} \) なる順序数を計算できたら、 \( x + y \) を \( y \) に簡約できるか分かるはずである。
| 定義 3.5 |
|---|
\( [ \mathrm{succ} _ \mathrm{AP} ( x ) = y \) を \( [ \min \{ x' \in \mathrm{AP} : x < x' \} = y ] \) の略記とする。 |
標準形の定義の補助のための関数 \( \mathrm{succ} _ \mathrm{AP} ( x ) \) の定義を行う。
| 仮定 3.6 |
|---|
\[ [ \forall x \ldotp x \in \mathrm{On} \rightarrow \exists _ 1 y \ldotp y \in \mathrm{On} \land \mathrm{succ} _ \mathrm{AP} ( x ) = y \] メモ: \( \mathrm{AP} \) には上限がなく、それゆえに \( \min \{ x' \in \mathrm{AP} : x < x' \} \) の値は存在する。最小性より一意性も成り立つ。 |
\( \mathrm{succ} _ \mathrm{AP} ( x ) \) が \( \mathrm{On} \) における関数であることを表す。
| 定義 3.6 |
|---|
\( \mathrm{NF} _ { + } ( \alpha, \beta ) \) を \( \alpha \in \mathrm{AP} \land \mathrm{succ} _ \mathrm{AP} ( \alpha ) > y \) と同値であるとする。 |
\( \alpha + \beta \) の形に対する浅い標準形を定義する。
ω の冪[]
\( \omega \) の冪も同様に述語として定義できる。
| 仮定 4.1 |
|---|
\[ \forall \alpha \ldotp \alpha \in \mathrm{On} \rightarrow \exists _ 1 \beta \ldotp \beta \in \mathrm{On} \land \left[ \omega ^ \alpha = \beta \right] \] |
これは \( \left[ \omega ^ \alpha = \beta \right] \) が関数であることを表す。
| 仮定 4.2 |
|---|
\[ \forall \beta \ldotp \beta \in \mathrm{On} \rightarrow \left( \exists \alpha \ldotp \alpha \in \mathrm{On} \land \omega ^ \alpha = \beta \right) \leftrightarrow \beta \in \mathrm{AP} \] |
これは \( \omega \) の冪と \( \mathrm{AP} \) の関係を表す。
| 定義 4.3 |
|---|
\( x \in \mathrm{Cr} \) を \( \alpha \in \mathrm{On} \land \omega ^ \alpha = \alpha \) と同値であるとする。 |
臨界順序数[note 2] (critical ordinal[note 3]) のクラスを定義する。
| 定義 4.4 |
|---|
\( x \in \mathrm{NCr} \) を \( \alpha \in \mathrm{On} \land \alpha < \omega ^ \alpha \) と同値であるとする。 |
非臨界順序数[note 4] (non-critical ordinal[note 5]) のクラスを定義する。
| 仮定 4.5 |
|---|
\[ \forall \alpha \ldotp ( \alpha \in \mathrm{Cr} \lor \alpha \in \mathrm{NCr} ) \land \lnot ( \alpha \in \mathrm{Cr} \land \alpha \in \mathrm{NCr} \] |
\( \mathrm{Cr} \) と \( \mathrm{NCr} \) が順序数を二分することを示す。
閉包[]
\( C ^ \Omega ( \alpha, \beta ) \) は \( \psi _ \Omega ( \alpha ) \) と共に超限帰納法により定義されるが、ここで \( C ^ \Omega ( \alpha, \beta ) \) は自身を定義に使っていないため、 \( \psi _ \Omega ( \alpha ) \) のみを超限帰納法の対象とすることが出来る。
| 仮定 5.1 |
|---|
\[ C ^ \Omega ( \alpha, \beta ) = \bigcup \{ C : \beta \cup \{ 0, \Omega \} \subset C \land ( \forall x y \ldotp x \in C \land y \in C \rightarrow ( x + y ) \in C ) \land ( \forall x \ldotp x \in C \rightarrow \omega ^ x \in C ) \land ( \forall x \ldotp x \in C \land x < \alpha \rightarrow \psi _ \Omega ( x ) \in C ) \} \] |
\( C ^ \Omega ( \alpha, \beta ) \) の定義を直接的に翻訳したものとの一致を示す。
注釈[]
参考文献[]
- 新井 2016
- 新井 敏康, 数学基礎論, 岩波書店, 2016. ISBN 978-4007304590.