WIP
Note that for \(\psi_0\) I use \(\psi\) and for \(\psi_n\) I use the \(\psi_{\Omega_{n+1}}\) convention.
Below OFP[]
Below OFP, it works like EBOCF
Examples:
\(\psi(\Omega) = \varepsilon_0\)
\(\psi(\Omega^\omega) = \varphi(\omega,0)\)
\(\psi(\Omega^\Omega) = \varphi(1,0,0)\)
\(\psi(\Omega^{\Omega^2}) = \varphi(1,0,0,0)\)
\(\psi(\Omega^{\Omega^\omega}) = \varphi\begin{pmatrix}1 \\ \omega \end{pmatrix} = SVO\)
\(\psi(\Omega^{\Omega^\Omega}) = LVO\)
\(\psi(\Omega_2) = BHO\)
\(\psi_{\Omega_2}(0) = \Omega\)
\(\psi_{\Omega_2}(\Omega_2) = \varepsilon_{\Omega+1}\)
\(\psi_{\Omega_3}(0) = \Omega_2\)
\(\psi_{\Omega_3}(\Omega_3) = \varepsilon_{\Omega_2+1}\)
\(\psi_{\Omega_{\omega+1}}(\Omega_{\omega+1}) = \varepsilon_{\Omega_{\omega}+1}\)
etc.
The first inaccessible[]
Now we have the first inaccessible. We introduce the function \(\psi_I\), where \(I\) denotes the least weakly inaccessible cardinal. The function generates OFPs like so:
\(\psi_I(0) = \Phi(1,0) = OFP\)
\(\psi_I(1) = \Phi(1,1)\)
\(\psi_I(2) = \Phi(1,2)\)
\(\psi_I(\Omega) = \Phi(1,\Omega)\)
\(\psi_I(OFP) = \Phi(1,\Phi(1,0))\)
\(\psi_I(I) = \Phi(2,0) = \Phi(1,\Phi(1,\Phi(1,\cdots)))\)
\(\psi_I(I^\Omega) = \Phi(\Omega,0)\)
\(\psi_I(I^I) = \Phi(1,0,0)\)
\(\psi_I(I^{I^\Omega}) = \Phi\begin{pmatrix}1 \\ \Omega \end{pmatrix}\)
etc.
With \(I\) in \(\psi_{\Omega_n}\), everything's still the same. I will only do \(\psi\) examples, since it's the most important one, but for others there isn't a lot of difference. Examples:
\(\psi(I) = \psi(\psi_I(I)) = \psi(\Phi(2,0))\)
\(\psi(I2) = \psi(I+\psi_I(I+\psi_I(I+\psi_I(I+\cdots)))) = \psi(I+\psi_I(I2)) = \psi(I+\Phi(2,1))\)
\(\psi(I^2) = \psi(I\psi_I(I\psi_I(I\psi_I(I\cdots)))) = \psi(I\psi_I(I^2)) = \psi(I+\Phi(3,0))\)
\(\psi(I^I) = \psi(I^{\psi_I(I^{\psi_I(I^{\psi_I(I\cdots)})})}) = \psi(I^{\psi_I(I^I)}) = \psi(I^{\Phi(1,0,0)})\)