Googology Wiki
Register
Googology Wiki
Line 165: Line 165:
   
 
==OCF using a weakly Mahlo cardinal==
 
==OCF using a weakly Mahlo cardinal==
This OCF is very similar to [https://sites.google.com/site/travelingtotheinfinity/the-function-collapsing-weakly-mahlo-cardinals Denis Maksudov's/Hyp_cos's weakly Mahlo OCF]. For more info about collapsing, this is similar to [[User:Hyp_cos/OCF_vs_Array_Notation#Using_weakly_Mahlos|here]]. However, this OCF has \(\psi_\Omega(M(0))\ge\psi_\Omega(M(0)^{M(0)^{M(0)}})\), so I should avoid using it.
+
This OCF is very similar to [https://sites.google.com/site/travelingtotheinfinity/the-function-collapsing-weakly-mahlo-cardinals Denis Maksudov's/Hyp_cos's weakly Mahlo OCF]. For more info about collapsing, this is similar to [[User:Hyp_cos/OCF_vs_Array_Notation#Using_weakly_Mahlos|here]]. However, this OCF has difficult behavior such as \(\psi_\Omega(M(0))\ge\psi_\Omega(\chi(M(0)^{M(0)^{M(0)}}))\) (same problem as June 2020 OCFs), so I should avoid using it.
   
 
Let \(M(0)\) denote the first [[Mahlo cardinal|weakly Mahlo cardinal]], and let \(\textrm{Reg}\) denote the set of uncountable [[Cofinality|regular]] cardinals \(<M(0)\)
 
Let \(M(0)\) denote the first [[Mahlo cardinal|weakly Mahlo cardinal]], and let \(\textrm{Reg}\) denote the set of uncountable [[Cofinality|regular]] cardinals \(<M(0)\)

Revision as of 05:11, 1 September 2021

These OCFs have more restricted notions of reflection encodings. For OCFs with harder definitions but more general reflection encodings, see User_blog:C7X/OCFs/Non_Hyp_cos-style. For ordinal notations, see User_blog:C7X/OCFs/Ordinal_notations.

Edit 2021: Since these reflection encodings are inspired by extensions of Hyp_cos's \(\Pi_4\)-rfl. OCF's, these can be considered to play the role of mapping predicates to predicates as injectively as possible, repeating as few conditions as possible. For analogy with Taranovsky's "Degrees of Reflection" see here

OCF using an uncountable cardinal

This OCF is Bachmann's psi

Theorems

Lemma Ω1: Let \(\alpha_0,\alpha_1\) be two ordinals in the domain of \(\psi\). \(\psi(\alpha_0)\in C(\alpha_1,\psi(\alpha_0))\cap\alpha_1\) implies \(\psi(\alpha_0\)<\psi(\alpha_1)\)??

Proof: For contradiction, assume there exist \(\alpha_0,\alpha_1\in\textrm{dom}(\psi)\) s.t. \(\psi(\alpha_0)\in C(\alpha_1,\psi(\alpha_0))\cap\alpha_1\), but \(\psi(\alpha_0\)\ge\psi(\alpha_1)\).

Theorem Ω2: \(\alpha_0\in C(\alpha_1,\psi(\alpha_0))\cap\alpha_1\) implies \(\psi(\alpha_0\)<\psi(\alpha_1)\)??

Proof: Because \(\alpha_0\in C(\alpha_1,\psi(\alpha_0))\subseteq C(\alpha_1,\psi(\alpha_1))\) and \(\alpha_0\in\alpha_1\), then \(\psi(\alpha_0)\in C(\alpha_1,\psi(\alpha_1))\cap\Omega\) by lemma Ω1 (assumption made here that \(\psi\) has codomain \(\Omega\)?). So "\(C(\alpha_1,\beta)\cap\Omega\subseteq\beta\)" must be false when \(\beta\le\psi(\alpha_0)\) (\(\psi(\alpha_0)\) would be member of LHS but not RHS), so the minimal such \(\beta\) is greater than \(\psi(\alpha_1)\). █

Comparisons

First, here are FSes using base-ω exponents:

\(\omega^{\gamma+1}[\eta]:=\omega^\gamma\eta \\ \textrm{For limit }\gamma,\textrm{ then }\omega^\gamma[\eta]:=\omega^{\gamma[\eta]} \\ \omega^0[\eta]\textrm{ is undefined} \\ (\gamma+\delta)[\eta]=\gamma+(\delta[\eta])\)

For \(\eta<\Omega\), define \(\Omega[\eta]:=\eta\)

Define FSes for Bachmann's OCF ψ:

\(\psi(0)[n]:=\omega\uparrow\uparrow n \\ \psi(\alpha+1)[n]:=\begin{cases}\psi(\alpha)+1\textrm{ if }n=0 \\ \omega^{\psi(\alpha+1)[n-1]}\textrm{ if }n>0\end{cases} \\ \textrm{If }Cof(\alpha)=\omega\textrm{, then }\psi(\alpha)[n]:=\psi(\alpha[n]) \\ \textrm{If }Cof(\alpha)>\omega\textrm{, then }\psi(\alpha)[n]:=\begin{cases}0\textrm{ if }n=0 \\ \psi(\alpha[\psi(\alpha)[n-1]])\textrm{ if }n>0\end{cases}\)

Here are comparisons of Bachmann psi with Veblen varphi:

\(\psi(0)\) \(\varphi(1,0)\)
\(\psi(1)\) \(\varphi(1,1)\)
\(\psi(\omega)\) \(\varphi(1,\omega)\)
\(\psi(\varepsilon_0)=\psi(\psi(0))\) \(\varphi(1,\varphi(1,0))\)
\(\psi(\Omega)\) \(\varphi(2,0)\)
\(\psi(\Omega+1)\) \(\varphi(1,\varphi(2,0)+1)\)
\(\psi(\Omega2)\) \(\varphi(2,1)\)
\(\psi(\omega^{\Omega+1})\) \(\varphi(2,\omega)\)
\(\psi(\omega^{\Omega+1}+\Omega)\) \(\varphi(2,\omega+1)\)
\(\psi(\omega^{\Omega+1}2)\) \(\varphi(2,\omega2)\)
\(\psi(\omega^{\Omega+1}3)\) \(\varphi(2,\omega3)\)
\(\psi(\omega^{\Omega+2})\) \(\varphi(2,\omega^2)\)
\(\psi(\omega^{\Omega+\omega})\) \(\varphi(2,\omega^\omega)\)
\(\psi(\omega^{\Omega+\psi(0)})\) \(\varphi(2,\varepsilon_0)\)
\(\psi(\omega^{\Omega+\psi(\Omega)})\) \(\varphi(2,\varphi(2,0))\)
\(\psi(\omega^{\Omega+\psi(\omega^{\Omega+\psi(\Omega)})})\) \(\varphi(2,\varphi(2,\varphi(2,0)))\)
\(\psi(\omega^{\Omega2})\) \(\varphi(3,0)\)
\(\psi(\omega^{\Omega3})\) \(\varphi(4,0)\)
\(\psi(\omega^{\omega^{\Omega+1}})\) \(\varphi(\omega,0)\)
\(\psi(\omega^{\omega^{\Omega+1}+\Omega})\) \(\varphi(\omega+1,0)\)
\(\psi(\omega^{\omega^{\Omega+1}+\Omega2})\) \(\varphi(\omega+2,0)\)
\(\psi(\omega^{\omega^{\Omega+1}2})\) \(\varphi(\omega2,0)\)
\(\psi(\omega^{\omega^{\Omega+1}2+\Omega})\) \(\varphi(\omega2+1,0)\)
\(\psi(\omega^{\omega^{\Omega+1}2+\Omega2})\) \(\varphi(\omega2+2,0)\)
\(\psi(\omega^{\omega^{\Omega+1}3})\) \(\varphi(\omega3,0)\)
\(\psi(\omega^{\omega^{\Omega+2}})\) \(\varphi(\omega^2,0)\)
\(\psi(\omega^{\omega^{\Omega+\psi(0)}})\) \(\varphi(\varepsilon_0,0)\)
\(\psi(\omega^{\omega^{\Omega+\psi(\omega^{\omega^{\Omega+\psi(0)}})}})\) \(\varphi(\varphi(\varepsilon_0,0),0)\)
\(\psi(\omega^{\omega^{\Omega2}})\) \(\varphi(1,0,0)\)
\(\psi(\omega^{\omega^{\Omega2}}+\Omega)\) \(\varphi(1,\varphi(1,0,0)+1)\)
\(\psi(\omega^{\omega^{\Omega2}}+\omega^{\Omega2})\) \(\varphi(2,\varphi(1,0,0)+1)\)
\(\psi(\omega^{\omega^{\Omega2}}+\omega^{\Omega3})\) \(\varphi(3,\varphi(1,0,0)+1)\)
\(\psi(\omega^{\omega^{\Omega2}}+\omega^{\omega^{\Omega+1}})\) \(\varphi(\omega,\varphi(1,0,0)+1)\)
\(\psi(\omega^{\omega^{\Omega2}}+\omega^{\omega^{\Omega+\psi(0)}})\) \(\varphi(\varepsilon_0,\varphi(1,0,0)+1)\)
\(\psi(\omega^{\omega^{\Omega2}}+\omega^{\omega^{\Omega+\psi(\omega^{\omega^{\Omega+\psi(0)}})}})\) \(\varphi(\varphi(\varepsilon_0,0),\varphi(1,0,0)+1)\)
\(\psi(\omega^{\omega^{\Omega2}}+\omega^{\omega^{\Omega+\psi(\omega^{\omega^{\Omega2}})}})\) \(\varphi(\varphi(1,0,0),1)\)
\(\psi(\omega^{\omega^{\Omega2}}+\omega^{\omega^{\Omega+\psi(\omega^{\omega^{\Omega2}})}}2)\) \(\varphi(\varphi(1,0,0),2)\)
\(\psi(\omega^{\omega^{\Omega2}}+\omega^{\omega^{\Omega+\psi(\omega^{\omega^{\Omega2}})}+1})\) \(\varphi(\varphi(1,0,0),\omega)\)
\(\psi(\omega^{\omega^{\Omega2}}2)\) \(\varphi(1,0,1)\)
\(\psi(\omega^{\omega^{\Omega2}+1})\)

\(\varphi(1,0,\omega)\)

OCF up to the ωth uncountable cardinal

For an ordinal \(\gamma\), let \(\gamma^+\) denote the next uncountable regular cardinal after \(\gamma\), and let \(\textrm{Reg}\) denote the set of uncountable regular cardinals less than \(\Omega_\omega\). For \(\alpha,\beta\in\textrm{Ord}\), define \(C(\alpha,\beta)\in\mathcal P(\textrm{Ord})\) by transfinite recursion in \(\alpha\):

  • \(C_0(\alpha,\beta)\ :=\ \beta\cup\{0\}\)
  • \(C_{i+1}(\alpha,\beta)\ :=\ C_i(\alpha,\beta)\cup\{\gamma+\delta,\omega^\gamma,\gamma^+:\gamma,\delta\in C_i(\alpha,\beta)\} \\ \phantom{C_{i+1}(\alpha,\beta)\ :=\ }\cup\{\psi_\kappa(\eta):\kappa,\eta\in C_i(\alpha,\beta)\land\kappa\in\textrm{Reg}\land\eta\in\alpha\}\)

For \(\pi\in\textrm{Reg}\) and \(\alpha\in\textrm{Ord}\), define \(\psi_\pi(\alpha)\in\textrm{Ord}\):

  • \(\psi_\pi(\alpha)\ :=\ \textrm{min}(\{\beta:C(\alpha,\beta)\cap\pi\subseteq\beta\}\cup\{\pi\})\)

Note that \(\psi_{\Omega_2}(1)=\varepsilon_{\Omega+2}\)

Exercises

These are exercises to help learn this OCF:

  1. What is \(\psi_\Omega(0)\)?
  2. What is \(\psi_\Omega(\zeta_0+1)\)?
  3. What is \(\psi_{\Omega_2}(0)\)?
  4. Why doesn't \(\psi_{\Omega_2}(0)\le\Omega+\omega_1^{CK}\) hold? (Related/alternative, why doesn't \(\psi_{\Omega_2}(\omega_1^{CK})=\psi_{\Omega_2}(\Omega)\)?)
  5. What is \(\psi_{\Omega_2}(\Omega)\)?

OCF using a weakly Mahlo cardinal

This OCF is very similar to Denis Maksudov's/Hyp_cos's weakly Mahlo OCF. For more info about collapsing, this is similar to here. However, this OCF has difficult behavior such as \(\psi_\Omega(M(0))\ge\psi_\Omega(\chi(M(0)^{M(0)^{M(0)}}))\) (same problem as June 2020 OCFs), so I should avoid using it.

Let \(M(0)\) denote the first weakly Mahlo cardinal, and let \(\textrm{Reg}\) denote the set of uncountable regular cardinals \(<M(0)\)

For \((\alpha,\beta)\in\varepsilon_{M(0)+1}\times\textrm{Ord}\), define \(B(\alpha,\beta)\subseteq\textrm{Ord}\):

  • \(B_0(\alpha,\beta)\ :=\ \beta\cup\{0,M(0)\}\)
  • \(B_{i+1}(\alpha,\beta)\ :=\ B_i(\alpha,\beta)\cup\{\gamma+\delta,\omega^\gamma,\psi_\kappa(\gamma):\gamma,\delta,\kappa\in B_i(\alpha,\beta)\} \\ \phantom{B_{i+1}(\alpha,\beta)\ :=\ B_i(\alpha,\beta)}\cup\{\chi(\eta):\eta\in C_i(\alpha,\beta)\land\eta\in\alpha\}\)
  • \(B(\alpha,\beta)\ :=\ \bigcup\{B_i(\alpha,\beta):i\in\mathbb{N}\}\)

For \(\alpha\in\varepsilon_{M(0)+1}\), define \(\chi(\alpha)\ :=\ \textrm{min}\{\beta\in\textrm{Reg}\ :\ B(\alpha,\beta)\cap M(0)\subseteq\beta\}\cup\{M(0)\}\)

For \((\alpha,\beta)\in\varepsilon_{M(0)+1}\times\textrm{Ord}\), define \(C(\alpha,\beta)\subseteq\textrm{Ord}\) by transfinite recursion in \(\alpha\):

  • \(C_0(\alpha,\beta)\ :=\ \beta\cup\{0,M(0)\}\)
  • \(C_{i+1}(\alpha,\beta)\ :=\ C_i(\alpha,\beta)\cup\{\gamma+\delta,\omega^\gamma,\chi(\gamma):\gamma,\delta\in C_i(\alpha,\beta)\} \\ \phantom{C_{i+1}(\alpha,\beta)\ :=\ C_i(\alpha,\beta)}\cup\{\psi_\kappa(\eta) :\kappa,\eta\in C_i(\alpha,\beta)\;\land\;\kappa\in\textrm{Reg}\land\eta\in\alpha\}\)
  • \(C(\alpha,\beta)\ :=\ \bigcup\{C_i(\alpha,\beta):i\in\mathbb{N}\}\)

For \(\alpha\in\textrm{Ord}\) and \(\pi\in\textrm{Reg}\), define \(\psi_\pi(\alpha)\ :=\ \textrm{min}\{\beta:C(\alpha,\beta)\cap\pi\subseteq\beta\}\cup\{\pi\}\)

This can be defined using only C instead of B and C, but the resulting OCF will have degenerate values. Also note that \(\Omega_{\Phi(1,0)+1}=\chi(\Phi(1,0)+2)\)

Theorems

Theorem: For any \(\pi,\alpha\in\textrm{Ord}\), then \(\psi_\pi(\alpha)\) has cofinality \(\omega\).

Proof: For contradiction, assume that \(\beta\) such that \(C(\alpha,\beta)\cap\pi\subseteq\beta\) has cofinality greater than \(\omega\), and there is no such \(\beta\) less than it that has cofinality \(\omega\). Apply Bachmann-style OCF lemma, then does [1] apply?

Theorem: \(\chi(M(0))\) is a limit cardinal

Proof: For contradiction, assume that \(\exists\gamma(\chi(M(0))=\Omega_{\gamma+1})\) (i.e. \(\chi(M(0))\) isn't a limit cardinal). If so, then \(\Omega_\gamma\) is in \(B(M(0),\beta)\), so \(\gamma\) is in there, so \(\chi(\gamma+1)\) is in there, which is a contradiction. (This logic can't be replicated for \(\chi(\omega)\) because \(\gamma+1\) isn't less than \(\omega\) in that case, so "\(\chi(\gamma+1)\in B(\omega,\beta)\)" wouldn't follow from the assumption)

Lemma: Given \((\pi,\alpha),(\pi,\beta)\in\textrm{dom}(\psi)\), then "exists \(\eta\) in the interval \((\beta,\alpha)\) such that \(\eta\in C(?,\beta\)" implies \(\psi_\pi(\beta)<\psi_\pi(\alpha)\)?

Theorem: \(\psi_\Omega(\omega^{M(0)+1})<\psi_\Omega(\psi_{\chi(\omega^{\omega^{M(0)+1}})}(0))\)

Proof: For contradiction, assume that \(\psi_\Omega(\omega^{M(0)+1})\ge\psi_\Omega(\psi_{\chi(\omega^{\omega^{M(0)+1}})}(0))\), and in this proof we will set \(\psi_\Omega(\omega^{M(0)+1})=\gamma_0\) and \(\psi_\Omega(\psi_{\chi(\omega^{\omega^{M(0)+1}})}(0))=\gamma_1\). If \(\gamma_0=\gamma_1\), then \(C(\omega^{M(0)+1},\gamma_0)\cap\Omega\subseteq\gamma_0\) and \(C(\psi_{\chi(\omega^{\omega^{M(0)+1}})}(0),\gamma_0)\cap\Omega\subseteq\gamma_0\) both hold. WIP

OCF using a weakly compact cardinal

This is similar to the above OCF, and is inspired by Denis Maksudov's KOCF2. However, this OCF has degenerate values (e.g. \(\psi^0_{\Omega_2}(0)=\varepsilon_0\)), but it uses Buchholz's and Hyp_cos's method of using degenerate values to the OCF's advantage to solve problems with infinite descent (e.g. using \(\lambda\eta.\psi^\eta_{K(0)}(0)\) similarly to Rathjen's \(\Xi\) function). It also avoids problems with "normal-looking" terms like \(\psi^0_\Omega(M(0))\), which older OCFs by me contained, such as those designed around June 2020. Thanks to Hyp_cos for fixing a problem with the A function

For \(\alpha\in\textrm{Ord}\) and \(A\in\mathcal P(\textrm{Ord})\), define a function \(S:\mathcal P(\textrm{Ord})\rightarrow\mathcal P(\textrm{Ord})\):

  • \(S(A)\ :=\ \{\alpha\in K(0):\forall(g:\alpha\rightarrow\alpha)(\exists(\alpha'\in A\cap\alpha)(\alpha'\textrm{ is closed under }g))\}\)

For \(\alpha,\beta\in\textrm{Ord}\), define \(C(\alpha,\beta)\in\mathcal P(\textrm{Ord})\) by transfinite recursion in \(\alpha\):

  • \(C_0(\alpha,\beta)\ :=\ \beta\cup\{0,K(0)\}\)
  • \(C_{i+1}(\alpha,\beta)\ :=\ C_i(\alpha,\beta)\cup\{\gamma+\delta,\omega^\gamma:\gamma,\delta\in C_i(\alpha,\beta)\} \\ \phantom{C_{i+1}(\alpha,\beta)\ :=\ C_i(\alpha,\beta)}\cup\{\psi^\xi_\kappa(\eta):\xi,\kappa,\eta\in C_i(\alpha,\beta)\land\eta\in\alpha\land\xi\in\alpha\}\)
  • \(C(\alpha,\beta)\ :=\ \bigcup\{C_i(\alpha,\beta);i\in\mathbb{N}\}\)

For \(\theta\in\varepsilon_{K(0)+1}\), define \(A(\theta)\subseteq K(0)\):

  • \(A(\theta)\ :=\ \{\gamma\in K(0)\ :\ \forall(\xi\in C(\theta,\gamma)\cap\theta)(\gamma\in S(A(\xi)))\}\)

For \(\theta,\alpha\in\textrm{Ord}\) and \(\pi\in A(\theta+1)\cup\{K(0)\}\), define \(\psi^\theta_\pi(\alpha)\in K(0)\):

  • \(\psi^\theta_\pi(\alpha)\ :=\ \textrm{min}\{\beta\in A(\theta):C(\alpha,\beta)\cap\pi\subseteq\beta\}\cup\{\pi\}\)

Note that values such as \(\psi^1_{K(0)}(1)\) are defined and are very large, however they can be considered degenerate and they don't affect non-degenerate values.

OCF using a Π_4-reflecting ordinal

This is Hyp_cos's OCF for \(\Pi_4\)-reflecting ordinals. Personal communication with Hyp_cos has given these intentions for the behavior of the \(A\) function:

  • Let \(\textrm{RI}\) be the set of reflection instances, and here restrict blackboard bold letters to \(\textrm{RI}\). For \(\mathbb X\) of the form \((\alpha,\beta,\mathbb Y)\), then \(A_\pi{\mathbb X}\) is intended to be the set of all ordinals below \(\pi\) that are " "\(\Pi_3\)-rfl. on"\(\alpha\) \(\textrm{Ord}\) and \(\Pi_2\)-rfl. on"\(\beta\) the set \(A_\pi\mathbb Y\).
  • For \(\mathbb X\) of the form \((\alpha)\), then \(A_\pi{\mathbb X}\) is intended to be the set of all ordinals below \(\pi\) that are "\(\Pi_3\)-rfl. on"\(\alpha\) \(\textrm{Ord}\).

To my knowledge these intentions haven't been proven to hold. For defintions of these reflection operators, see this page.

This OCF has an interesting correspondence with Taranovsky's Degrees of Reflection. Let \(\textrm{SD}\) denote the set of standard degrees from DoR, and let \(a,b,b'\in\textrm{SD}\). A predicate characterized by reflection instance \((o(a),o(b),\mathbb X)\) in Hyp_cos's OCF seems to correspond to the predicate of being of degree \(d_b=\textrm{sup}_<\{\Omega^{\Omega^a}\times d_{b'}:b'<b\}\) in DoR (where is \(\mathbb X\) here??), where \(o(y)\) denotes the ordinal corresponding to term \(y\) (leaving gaps/not necessarily recursive, as Taranovsky mentioned). So Hyp_cos's reflection instances superficially behave like a weakened sort of "Taranovsky/Stegert addition" (e.g. \(\lambda(\alpha,\beta).\beta+\omega^\alpha\)) on Taranovsky's degrees. "Weakened" because of this reason:

  • Degrees such as \(\Omega^{\Omega^\Omega}\) are closed under \((\lambda(a,b).\Omega^{\Omega^a}\times d_{b'})\upharpoonright(\textrm{Terms }<\Omega)\times\textrm{SD}\), along with \((\lambda a.\Omega^{\Omega^a})\upharpoonright(\textrm{Terms }<\Omega)\) because of its lack of ability to add to exponents high up a power tower (compare with the equality \(\Omega^{\Omega^a}\times\Omega^c=\Omega^{\Omega^a+c}\), where \(c\in\textrm{SD}\)). So it doesn't have the "shifting" ability that Taranovsky addition has, in which within a power tower, multiplication can be performed no matter how high up a power tower the multiplicands are.

OCF up to a nonrecursive analog of (*2)-stb

Since I don't understand enough proof theory to know if the elements of \(\textrm{RI}\) correspond to instances of a reflection rule, what plays the role of what Hyp_cos calls "reflection instances" I call "reflection encodings". Credit to Hyp_cos's blog post for some of this from the next OCFs, the reflection encodings are very similar as well. The definition of \(f\textrm{-shrewd}\) cardinals is here

Here we work in ZFC+"given \(\delta\in\textrm{Ord}\), \(\forall(\beta\in\,\)\(\textrm{Ord}\)\(-\{0\})\exists(\kappa>\delta)(\kappa\textrm{ is }(+\beta)\text{-shrewd on Ord})\)".

Here let \(\Upsilon\) denote \(\textrm{sup}(\{\textrm{min}\{\gamma:\gamma\textrm{ is }(+\delta)\textrm{-shrewd}\}):\delta<\Upsilon\}\).

Define a set of ordered tuples \(\textrm{RI}\):

  • \(()\in\textrm{RI}\)
  • For \(\mathbb X,\mathbb Y\in\textrm{RI}\), \(\beta\in\textrm{Ord}-\{0\}\), \(\alpha\in\textrm{Ord}\), then \((\mathbb X,\beta,\alpha,\mathbb Y)\in\textrm{RI}\)

Define a function \(\textrm{V}:\textrm{RI}\rightarrow\mathcal P(\textrm{Ord})\), called "ordinals":

  • \(\textrm{V}():=\varnothing\)
  • \(\textrm{V}(\mathbb X,\beta,\alpha,\mathbb Y):=\{\alpha,\beta\}\cup\textrm{V}\mathbb X\cup\textrm{V}\mathbb Y\)

Define a function \(\textrm{IO}:\textrm{RI}\rightarrow\mathcal P(\textrm{Ord})\), called "iteration ordinals":

  • \(\textrm{IO}():=\varnothing\)
  • \(\textrm{IO}(\mathbb X,\beta,\alpha,\mathbb Y):=\{\alpha\}\cup\textrm{IO}\mathbb X\cup\textrm{IO}\mathbb Y\)

Note that \(\forall(\mathbb X\in\textrm{RI})(\textrm{IO}\mathbb X\subseteq\textrm{V}\mathbb X)\)

Let \(\textrm{SC}\) denote the set of (+1)-shrewd cardinals \(\le\Upsilon\), let \(\pi,\kappa\) range over \(\textrm{SC}\), and let \(\mathbb X,\mathbb Y\) range over \(\textrm{RI}\).

For \(\alpha,\beta\in\textrm{Ord}\), define \(C(\alpha,\beta)\in\mathcal P(\textrm{Ord})\) by transfinite recursion in \(\alpha\):

  • \(C_0(\alpha,\beta)\ :=\ \beta\cup\{0,\Upsilon\}\)
  • \(C_{i+1}(\alpha,\beta)\ :=\ \{\gamma+\delta,\omega^\gamma:\gamma,\delta\in C_i(\alpha,\beta)\} \\ \phantom{C_{i+1}(\alpha,\beta)\ :=}\cup\{\psi^{\mathbb Y}_\kappa(\eta):\kappa,\gamma\in C_i(\alpha,\beta)\land\eta\in\alpha\land\textrm{V}\mathbb{Y}\subseteq C_i(\alpha,\beta)\land \textrm{IO}\mathbb{Y}\subseteq\alpha\}\) (might not work)
  • \(C(\alpha,\beta)\ :=\ \bigcup\{C_i(\alpha,\beta):i\in\mathbb{N}\}\)

For \(\pi\in\textrm{SC}\) and \(\mathbb X\in\textrm{RI}\), define \(A_\pi\mathbb X\subseteq\Upsilon\):

  • \(A_\pi()\ :=\ \pi\)
  • \(A_\pi(\mathbb X,\beta,0,\mathbb Y)\ :=\ A_\pi\mathbb Y\)
  • \(\text{For }\alpha>0:\ A_\pi(\mathbb X,\beta,\alpha,\mathbb Y)\ :=\ \{\gamma\in A_\pi\mathbb X:C(\alpha,\gamma)\cap\pi\subseteq\gamma\;\land \\ \phantom{\{\gamma\in A_\pi\mathbb{X}:}\;\forall(\xi\in C(\alpha,\gamma)\cap\alpha)(\gamma\textrm{ is }(+\beta)\textrm{-shrewd on }A_\pi(\mathbb X,\beta,\xi,\mathbb Y))\}\)

For \(\alpha\in\textrm{Ord}\), \(\pi\in\textrm{SC}\), and \(\mathbb X\in\textrm{RI}\), define \(\psi^{\mathbb X}_\pi(\alpha)\in\Upsilon\):

  • \(\psi^{\mathbb X}_\pi(\alpha)\ :=\ \textrm{min}\{\beta\in A_\pi\mathbb X:C(\alpha,\beta)\cap\pi\subseteq\beta\}\cup\{\pi\}\)

Explanation

This is very similar to Hyp_cos's OCF, but with large cardinal properties instead of reflecting ordinals. \((\mathbb X,\beta,\alpha,\mathbb Y)\) is intended to represent the condition " "\(\mathbb X\) condition and \((+\beta)\)-shrewd on"\(^\alpha\) \(\mathbb Y\) condition", and the entries of the reflection encoding appear in the same order as a mnemonic.

This OCF skips cardinals like \(\Omega\) and \(I(0)\), and uses functionally-shrewd cardinals instead. Here's a table of some small shrewd cardinals and the roles they would play if this OCF were restricted to the limit of the previous weakly compact OCF:

Role in WC OCF Cardinal in functionally-shrewd OCF
\(\Omega\) Least (+1)-shrewd
\(\Omega_2\) 2nd (+1)-shrewd
\(\Omega_\omega\) Least limit of (+1)-shrewds below
\(I(0)\) (+1)-shrewd and limit of (+1)-shrewds below
1-inaccessible cardinal (+1)-shrewd and limit of "(+1)-shrewd and limit of (+1)-shrewds below" below
Mahlo (+1)-shrewd on set of (+1)-shrewd below
1-Mahlo (+1)-shrewd on set of "(+1)-shrewd on set of (+1)-shrewd below" below
Weakly compact (+2)-shrewd

OCF using a nonrecursive analog of (α^+)-stb

Let \(\gamma^+\) denote the first (+1)-shrewd cardinal after \(\gamma\), and here let \(\Xi\) denote the least \((\lambda\gamma.\gamma^+)\textrm{-shrewd}\) cardinal. The definition of \(f\textrm{-shrewd}\) cardinals is here

Here we work in ZFC+"given \(\delta\in\textrm{Ord}\), \(\forall(\beta\in\,\)\(\textrm{Ord}\)\(-{0})\exists(\kappa>\delta)(\kappa\textrm{ is }(+\beta)\text{-shrewd on Ord})\)".

Define a set of ordered tuples \(\textrm{RI}\):

  • \(()\in\textrm{RI}\)
  • For \(\mathbb X,\mathbb Y\in\textrm{RI}\), \(\beta\in\textrm{Ord}\), \(\alpha\in\textrm{Ord}\), then \((\mathbb X,\beta,\alpha,\mathbb Y)\in\textrm{RI}\)

Define a function \(\textrm{V}:\textrm{RI}\rightarrow \mathcal P(\textrm{Ord})\), called "ordinals":

  • \(\textrm{V}():=\varnothing\)
  • \(\textrm{V}(\mathbb X,\beta,\alpha,\mathbb Y):=\{\alpha,\beta\}\cup\textrm{V}\mathbb X\cup\textrm{V}\mathbb Y\)

Define a function \(\textrm{IO}:\textrm{RI}\rightarrow \mathcal P(\textrm{Ord})\), called "iteration ordinals":

  • \(\textrm{IO}():=\varnothing\)
  • \(\textrm{IO}(\mathbb X,\beta,\alpha,\mathbb Y):=\{\alpha\}\cup\textrm{IO}\mathbb X\cup\textrm{IO}\mathbb Y\)

Note that \(\forall(\mathbb X\in\textrm{RI})(\textrm{IO}\mathbb X\subseteq\textrm{V}\mathbb X)\)

Let \(\textrm{SC}\) denote the set of (+1)-shrewd cardinals \(\le\Xi\), let \(\pi,\kappa\) range over \(\textrm{SC}\), and let \(\mathbb X,\mathbb Y\) range over \(\textrm{RI}\).

For \(\alpha,\beta\in\textrm{Ord}\), define \(C(\alpha,\beta)\in\mathcal P(\textrm{Ord})\) by transfinite recursion in \(\alpha\):

  • \(C_0(\alpha,\beta)\ :=\ \beta\cup\{0,\Xi\}\)
  • \(C_{i+1}(\alpha,\beta)\ :=\ \{\gamma+\delta,\omega^\gamma:\gamma,\delta\in C_i(\alpha,\beta)\} \\ \phantom{C_{i+1}(\alpha,\beta)\ :=}\cup\{\psi^{\mathbb Y}_\kappa(\eta):\kappa,\gamma\in C_i(\alpha,\beta)\land\eta\in\alpha\land\textrm{V}\mathbb{Y}\subseteq C_i(\alpha,\beta)\cap\alpha\land\textrm{IO}\mathbb Y\subseteq\alpha\}\)
  • \(C(\alpha,\beta)\ :=\ \bigcup\{C_i(\alpha,\beta):i\in\mathbb{N}\}\)

For \(\pi\in\textrm{SC}\) and \(\mathbb X\in\textrm{RI}\), define \(A_\pi\mathbb X\subseteq\Xi\):

  • \(A_\pi()\ :=\ \pi\)
  • \(A_\pi(\mathbb X,\beta,0,\mathbb Y)\ :=\ A_\pi\mathbb Y\)
  • \(\text{For }\alpha>0:\ A_\pi(\mathbb X,\beta,\alpha,\mathbb Y)\ :=\ \{\gamma\in A_\pi\mathbb X:C(\alpha,\gamma)\cap\pi\subseteq\gamma\;\land \\ \phantom{\{\gamma\in A_\pi\mathbb{X}:}\;\forall(\xi\in C(\alpha,\gamma)\cap\alpha)(\gamma\textrm{ is Shr-}\beta\textrm{ on }A_\pi(\mathbb X,\beta,\xi,\mathbb Y))\}\)

For \(\alpha\in\textrm{Ord}\), \(\pi\in\textrm{SC}\), and \(\mathbb X\in\textrm{RI}\), define \(\psi^{\mathbb X}_\pi(\alpha)\in\Xi\):

  • \(\psi^{\mathbb X}_\pi(\alpha)\ :=\ \textrm{min}\{\beta\in A_\pi\mathbb X:C(\alpha,\beta)\cap\pi\subseteq\beta\}\cup\{\pi\}\)

Restrict \(f\) to inflationary functions (\(f\) is inflationary iff \(\forall(\beta\in\textrm{Domain of }f)(\beta<f(\beta))\)).

For \(\beta\in\Xi\) and \(\delta\in\textrm{Ord}\) and \(s\subset\textrm{Ord}\), "\(\beta\text{ is Shr-}\delta\text{ on }s\)" is defined as this condition:

  • \(\forall(\delta'\in C(\delta,\beta)\cap\delta) \\ \phantom{\forall}(\exists(f:\Xi\rightarrow\Xi)(\text{Least }f\text{-shrewd on }s >\textrm{min}\{\gamma:\gamma \text{ is Shr-}\delta'\text{ on }s\} \\ \phantom{\forall(\exists(f:\Xi\rightarrow\Xi)}\,\land\beta \text{ is }f\text{-shrewd on }s))\)

OCF up to a nonrecursive analog of (α^(+^ω))-stb

Since I don't understand enough proof theory to know if the elements of \(\textrm{RI}\) correspond to instances of a reflection rule, what plays the role of what Hyp_cos calls "reflection instances" I call "reflection encodings". Is "ωth (^+)-shrewd" equal to \(\psi^{(\,)}_{0^{**}}(1)\) due to ordinals such as \(((0^*+\omega^0)^*+\omega^0)^*+\omega^0\in C(1,\beta)\)?


Here we work in ZFC+"given \(\delta\in\textrm{Ord}\), \(\forall(\beta\in\,\)\(\textrm{Ord}\)\(-{0})\exists(\kappa>\delta)(\kappa\textrm{ is }(+\beta)\text{-shrewd on Ord})\)". The definition of \(f\textrm{-shrewd}\) cardinals is here

Let \(\gamma^+\) denote the next (+1)-shrewd cardinal after \(\gamma\).

For an operation \(O:\textrm{Ord}\rightarrow\textrm{Ord}\), let \(\gamma^{(O^\delta)}\) denote the operation \(O\) applied \(\delta\) times to \(\gamma\).

For \(\gamma\in\textrm{Ord}\), let \(\textrm{GSU}(\gamma):=\textrm{max}(\{\delta:\gamma\textrm{ is }(\lambda\xi.\delta)\textrm{-shrewd}\}\cup\{0\})\) (GSU stands for "greatest shrewd up to", and the function used here is a constant function)

For \(\gamma\in\textrm{Ord}\), here define \(\gamma^*:=\textrm{min}\{\delta >\gamma:\textrm{max}\{\xi:\exists\delta'(\textrm{GSU}(\delta)=\delta'^{(+^\xi)})\}>\textrm{max}\{\theta:\exists\gamma'(\textrm{GSU}(\gamma)=\gamma'^{(+^\theta)})\}\}\)

Here let \(\Upsilon\) denote \(\textrm{sup}(\{0^{(*^i)}:i\in\mathbb{N}\})\)

Define a set of ordered tuples \(\textrm{RI}\):

  • \(()\in\textrm{RI}\)
  • For \(\mathbb X,\mathbb Y\in\textrm{RI}\), \(\kappa\in\{\gamma<\Upsilon:\gamma\textrm{ is }(\gamma^+)\textrm{-shrewd}\}\), \(\beta\in\textrm{Ord}\), and \(\alpha\in\textrm{Ord}\), then \((\mathbb X,\kappa,\beta,\alpha,\mathbb Y)\in\textrm{RI}\)

The members of \(\textrm{RI}\) are called "reflection encodings".

Define a function \(\textrm{V}:\textrm{RI}\rightarrow \mathcal P(\textrm{Ord})\), called "ordinals":

  • \(\textrm{V}():=\varnothing\)
  • \(\textrm{V}(\mathbb X,\kappa,\beta,\alpha,\mathbb Y):=\{\alpha,\kappa,\beta\}\cup\textrm{V}\mathbb X\cup\textrm{V}\mathbb Y\)

Define a function \(\textrm{IO}:\textrm{RI}\rightarrow \mathcal P(\textrm{Ord})\), called "iteration ordinals":

  • \(\textrm{IO}():=\varnothing\)
  • \(\textrm{IO}(\mathbb X,\kappa,\beta,\alpha,\mathbb Y):=\{\alpha\}\cup\textrm{IO}\mathbb X\cup\textrm{IO}\mathbb Y\)

Note that \(\forall(\mathbb X\in\textrm{RI})(\textrm{IO}\mathbb X\subseteq\textrm{V}\mathbb X)\)

Let \(\textrm{SC}\) denote the set of (+1)-shrewd cardinals \(\le\Upsilon\), let \(\pi,\kappa\) range over \(\textrm{SC}\), and let \(\mathbb X,\mathbb Y\) range over \(\textrm{RI}\).

For \(\alpha,\beta\in\textrm{Ord}\), define \(C(\alpha,\beta)\in\mathcal P(\textrm{Ord})\) by transfinite recursion in \(\alpha\):

  • \(C_0(\alpha,\beta)\ :=\ \beta\cup\{0,\Upsilon\}\)
  • \(C_{i+1}(\alpha,\beta)\ :=\ \{\gamma+\delta,\omega^\gamma,\gamma^*:\gamma,\delta\in C_i(\alpha,\beta)\} \\ \phantom{C_{i+1}(\alpha,\beta)\ :=}\cup\{\psi^{\mathbb Y}_\kappa(\eta):\kappa,\gamma\in C_i(\alpha,\beta)\land\eta\in\alpha\land\textrm{V}\mathbb{Y}\subseteq C_i(\alpha,\beta)\land\textrm{IO}\mathbb Y\subseteq\alpha\}\)
  • \(C(\alpha,\beta)\ :=\ \bigcup\{C_i(\alpha,\beta):i\in\mathbb{N}\}\)

For \(\pi\in\textrm{SC}\) and \(\mathbb X\in\textrm{RI}\), define \(A_\pi\mathbb X\subseteq\Upsilon\):

  • \(A_\pi()\ :=\ \pi\)
  • \(A_\pi(\mathbb X,\kappa,\beta,0,\mathbb Y)\ :=\ A_\pi\mathbb Y\)
  • \(\text{For }\alpha>0:\ A_\pi(\mathbb X,\kappa,\beta,\alpha,\mathbb Y)\ :=\ \{\gamma\in A_\pi\mathbb X:C(\alpha,\gamma)\cap\pi\subseteq\gamma\;\land \\ \phantom{\{\gamma\in A_\pi\mathbb{X}:}\;\forall(\xi\in C(\alpha,\gamma)\cap\alpha)(\gamma\textrm{ is Shr}_\kappa\textrm{-}\beta\textrm{ on }A_\pi(\mathbb X,\kappa,\beta,\xi,\mathbb Y))\}\)

For \(\alpha\in\textrm{Ord}\), \(\pi\in\textrm{SC}\), and \(\mathbb X\in\textrm{RI}\), define \(\psi^{\mathbb X}_\pi(\alpha)\in\Upsilon\):

  • \(\psi^{\mathbb X}_\pi(\alpha)\ :=\ \textrm{min}\{\beta\in A_\pi\mathbb X:C(\alpha,\beta)\cap\pi\subseteq\beta\}\cup\{\pi\}\)

Restrict \(f\) to inflationary functions (\(f\) is inflationary iff \(\forall(\beta\in\textrm{Domain of }f)(\beta<f(\beta))\)).

For \(\beta\in\Upsilon\) and \(\delta\in\textrm{Ord}\) and \(s\subset\textrm{Ord}\), "\(\beta\text{ is Shr}_\kappa\textrm{-}\delta\text{ on }s\)" is defined as this condition:

  • \(\forall(\delta'\in C(\delta,\beta)\cap\delta) \\ \phantom{\forall}(\exists(f:\Upsilon\rightarrow\Upsilon)(\text{Least }f\text{-shrewd on }s >\textrm{min}\{\gamma:\gamma \text{ is Shr}_{\kappa}\textrm{-}\delta'\text{ on }s\} \\ \phantom{\forall(\exists(f:\Xi\rightarrow\Xi)}\,\land\beta \text{ is }f\text{-shrewd on }s) \\ \phantom{\forall}\land C(\delta,\beta)\cap\kappa\subseteq\beta)\)

Note that \(\textrm{min}(A((),0^{**},1,1,())\ )\) is \((\lambda\gamma.\gamma^++1)\textrm{-shrewd}\). \(\textrm{min}(A((),0^{**},0,1,())\ )\) would have been \((\lambda\gamma.\gamma^+)\textrm{-shrewd}\), but that ordered tuple isn't a member of \(\textrm{RI}\) (the 3rd entry must be nonzero)

OCF using a nonrecursive analog of (next rec. Mahlo after α)-stb

Since I don't understand enough proof theory to know if the elements of \(\textrm{RI}\) correspond to instances of a reflection rule, what plays the role of what Hyp_cos calls "reflection instances" I call "reflection encodings".

For inflationary \(f:\textrm{Ord}\rightarrow\textrm{Ord}\) and \(s\subseteq\textrm{Ord}\), an ordinal \(\alpha\) is "\(f\)-shrewd on s" if for all \(A\subseteq V_\alpha\) and for all \(\{\in\}\)-formulae \(\phi\) with exactly one free variable, (is this definition too messy?)

\(((V_{f(\alpha)},\in,A)\vDash\phi)\rightarrow\exists(\alpha'\in s\cap\alpha )\exists\eta'(\alpha+\eta'<f(\alpha)\land(V_{\alpha'+\eta'},\in,A\cap\alpha')\vDash\phi)\)

Also an ordinal is called "\(f\textrm{-shrewd}\)" if it's \(f\textrm{-shrewd on Ord}\).

Let \(\gamma^+\) denote the next (+1)-shrewd cardinal after \(\gamma\), and here define \(\Xi\) as the least \((\lambda\gamma.\textrm{Next (}(+1)\textrm{-shrewd on class of }(+1)\textrm{-shrewds) after }\gamma)\textrm{-shrewd}\) cardinal, and here restrict \(m\) to \(\{0,1\}\).

Here we work in ZFC+"given \(\delta\in\textrm{Ord}\), \(\forall(\beta\in\,\)\(\textrm{Ord}\)\(-\{0\})\exists(\kappa>\delta)(\kappa\textrm{ is }(+\beta)\text{-shrewd on Ord})\)".

Define a set of ordered tuples \(\textrm{RI}\):

  • \(()\in\textrm{RI}\)
  • For \(\mathbb X,\mathbb Y\in\textrm{RI}\), \(m\in\{0,1\}\), \(\kappa\in\{\gamma\le\Xi:\gamma\textrm{ is }(\lambda\theta.\theta^+)\textrm{-shrewd}\}\), \(\beta\in\textrm{Ord}\), and \(\alpha\in\textrm{Ord}\), then \((\mathbb X,m,\kappa,\beta,\alpha,\mathbb Y)\in\textrm{RI}\)

The members of \(\textrm{RI}\) are called "reflection encodings".

Define a function \(\textrm{V}:\textrm{RI}\rightarrow \mathcal P(\textrm{Ord})\), called "ordinals":

  • \(\textrm{V}():=\varnothing\)
  • \(\textrm{V}(\mathbb X,m,\kappa,\beta,\alpha,\mathbb Y):=\{\alpha,\kappa,\beta\}\cup\textrm{V}\mathbb X\cup\textrm{V}\mathbb Y\)

Define a function \(\textrm{IO}:\textrm{RI}\rightarrow \mathcal P(\textrm{Ord})\), called "iteration ordinals":

  • \(\textrm{IO}():=\varnothing\)
  • \(\textrm{IO}(\mathbb X,m,\kappa,\beta,\alpha,\mathbb Y):=\{\alpha\}\cup\textrm{IO}\mathbb X\cup\textrm{IO}\mathbb Y\)

Note that \(\forall(\mathbb X\in\textrm{RI})(\textrm{IO}\mathbb X\subseteq\textrm{V}\mathbb X)\)

Let \(\textrm{SC}\) denote the set of (+1)-shrewd cardinals \(\le\Xi\), let \(\pi,\kappa\) range over \(\textrm{SC}\), and let \(\mathbb X,\mathbb Y\) range over \(\textrm{RI}\).

For \(\alpha,\beta\in\textrm{Ord}\), define \(C(\alpha,\beta)\subset\textrm{Ord}\) by transfinite recursion in \(\alpha\):

  • \(C_0(\alpha,\beta)\ :=\ \beta\cup\{0,\Xi\}\)
  • \(C_{i+1}(\alpha,\beta)\ :=\ \{\gamma+\delta,\omega^\gamma:\gamma,\delta\in C_i(\alpha,\beta)\} \\ \phantom{C_{i+1}(\alpha,\beta)\ :=}\cup\{\psi^{\mathbb Y}_\kappa(\eta),:\kappa,\gamma\in C_i(\alpha,\beta)\land\eta\in\alpha\land\textrm{V}\mathbb Y\subseteq C_i(\alpha,\beta)\land\textrm{IO}\mathbb Y\subseteq\alpha\}\)
  • \(C(\alpha,\beta)\ :=\ \bigcup\{C_i(\alpha,\beta):i\in\mathbb{N}\}\)

For \(\pi\in\textrm{SC}\) and \(\mathbb X\in\textrm{RI}\), define \(A_\pi\mathbb X\subseteq\Xi\):

  • \(A_\pi()\ :=\ \pi\)
  • \(A_\pi(\mathbb X,m,\kappa,\beta,0,\mathbb Y)\ :=\ A_\pi\mathbb Y\)
  • \(\text{For }\alpha>0:\ A_\pi(\mathbb X,m,\kappa,\beta,\alpha,\mathbb Y)\ :=\ \{\gamma\in A_\pi\mathbb X:C(\alpha,\gamma)\cap\pi\subseteq\gamma\;\land \\ \phantom{\{\gamma\in A_\pi\mathbb{X}:}\;\forall(\xi\in C(\alpha,\gamma)\cap\alpha)(\gamma\textrm{ is Shr}^m_\kappa\textrm{-}\beta\textrm{ on }A_\pi(\mathbb X,m,\kappa,\beta,\xi,\mathbb Y))\}\)

For \(\alpha\in\textrm{Ord}\), \(\pi\in\textrm{SC}\), and \(\mathbb X\in\textrm{RI}\), define \(\psi^{\mathbb X}_\pi(\alpha)\in\Xi\):

  • \(\psi^{\mathbb X}_\pi(\alpha)\ :=\ \textrm{min}\{\beta\in A_\pi\mathbb X:C(\alpha,\beta)\cap\pi\subseteq\beta\}\cup\{\pi\}\)

Restrict \(f\) to inflationary functions (\(f\) is inflationary iff \(\forall(\beta\in\textrm{Domain of }f)(\beta<f(\beta))\)).

For \(\beta\in\Xi\) and \(\delta\in\textrm{Ord}\) and \(s\subseteq\textrm{Ord}\), "\(\beta\text{ is Shr}^m_\kappa\textrm{-}\delta\text{ on }s\)" is defined as this condition:

  • \(\forall(\delta'\in C(\delta,\beta)\cap\delta) \\ \phantom{\forall}(\exists(f:\Xi\rightarrow\Xi)(\text{Least }f\text{-shrewd on }s >\textrm{min}\{\gamma:\gamma \text{ is Shr}^m_{\kappa}\textrm{-}\delta'\text{ on }s\} \\ \phantom{\forall(\exists(f:\Xi\rightarrow\Xi)}\,\land\beta \text{ is }f\text{-shrewd on }s) \\ \phantom{\forall}\land C(\delta,\beta)\cap\kappa\subseteq\beta \\ \phantom{\forall}\land(m=1\rightarrow f(\beta)\in\textrm{SC}\cap\Xi))\)

Theorems

Theorem: Let \(\textrm{Cl}(A)\) denote \(A\cup\{\alpha:\alpha=\textrm{sup}(A\cap\alpha)\}\), and let \(\textrm{Enum}(A)\) denote the unique strictly increasing function with domain exactly \(A\). If \(\beta\) is \(\textrm{Shr}^1_\Xi\textrm{-}\Xi\) on \(\textrm{Ord}\), then \(\beta\) is shrewd up to a maximal ordinal \(\beta'\) that is (+1)-shrewd and \(\exists !\gamma(\textrm{Enum}(\textrm{Cl}(\textrm{SC}))(\gamma)=\beta'\land\gamma\textrm{ is a limit ordinal})\).

Proof:

First we prove that the "\(\textrm{Shr}^1_\Xi\textrm{-}\Xi\) on \(\textrm{Ord}\)" condition implies (+1)-shrewdness of \(\beta'\). Because \(m=1\), then \(f(\beta)\in\textrm{SC}\) (i.e. it's (+1)-shrewd) and \(\beta\) is \(f\textrm{-shrewd}\), so by the definition of functional-shrewdness, \(\beta\) is shrewd up to a (maximal) (+1)-shrewd ordinal.

Is this correct? How is it guaranteed that \(f(\beta)\) is maximal (i.e. \(\beta'\))?

Next we prove the second condition. \(\gamma\) is unique because \(\textrm{Enum}(\textrm{Cl}(\textrm{SC}))\) is strictly increasing. The rest of the proof of this condition is by contradiction:

Assume that \(\exists \gamma(\textrm{Enum}(\textrm{Cl}(\textrm{SC}))(\gamma+1)=\beta')\) (i.e. this condition is false). \(\textrm{Enum}(\textrm{Cl}(\textrm{SC}))(\gamma+1)\in C(\Xi,\beta)\) by the definition of \(\textrm{Shr}\) conditions, because \(\beta\) is shrewd up to \(\beta'\). Also \(\textrm{Enum}(\textrm{Cl}(\textrm{SC}))(\gamma+1)\) is of the form \(\psi^{((),0,\textrm{Least }(^+)\textrm{-shrewd},1,1,())}_\kappa(\eta)\) with \(\eta<\Xi\). So also \(\textrm{Enum}(\textrm{Cl}(\textrm{SC}))(\gamma+2)\) is of the form \(\psi^{((),0,\textrm{Least }(^+)\textrm{-shrewd},1,1,())}_\kappa(\eta+1)\), and note that \(\eta+1<\Xi\).

Therefore, \(\textrm{Enum}(\textrm{Cl}(\textrm{SC}))(\gamma+2)\in C(\Xi,\beta)\) , so \(\beta\) is shrewd up to \(\textrm{Enum}(\textrm{Cl}(\textrm{SC}))(\gamma+2)\). However, this contradicts the maximality of \(\beta'\), which is a contradiction.

OCF up to a nonrecursive analog of ω-ply-(+1)-stb

Since I don't understand enough proof theory to know if the elements of \(\textrm{RI}\) correspond to instances of a reflection rule, what plays the role of what Hyp_cos calls "reflection instances" I call "reflection encodings". This might seem like a large jump from analogs of (next rec. Mahlo)-stability, but the definition is similar (except for some behavior of degenerate reflection encodings ). Note that there are intentionally degenerate reflection encodings (e.g. \(((),(),\Upsilon,1,1,())\)) in order to prevent infinite nesting.

For inflationary \(f:\textrm{Ord}\rightarrow\textrm{Ord}\) and \(s\subseteq\textrm{Ord}\), an ordinal \(\alpha\) is "\(f\)-shrewd on s" if for all \(\{\in\}\)-formulae \(\phi\) with exactly one free variable, (is this too messy?)

\(\forall(A\subseteq V_\alpha)(((V_{f(\alpha)},\in)\vDash\phi(A))\rightarrow\exists(\alpha'\in s\cap\alpha) \exists\eta'(\alpha+\eta'<f(\alpha)\land(V_{\alpha'+\eta'},\in)\vDash\phi(A \cap\alpha')))\)

Also a cardinal is called "\(f\textrm{-shrewd}\)" if it's \(f\textrm{-shrewd on Ord}\).

Here we work in ZFC+"given \(\delta\in\textrm{Ord}\), \(\forall(\beta\in\,\)\(\textrm{Ord}\)\(-{0})\exists(\kappa>\delta)(\kappa\textrm{ is }(+\beta)\text{-shrewd on Ord})\)".

Let \(\gamma^+\) denote the next (+1)-shrewd cardinal after \(\gamma\).

Here let \(\Upsilon\) denote \(\textrm{sup}(\{\textrm{min}\{\gamma:\exists((\gamma_i)_{0\le i\le k}\in\textrm{Ord}^{k+1})(\gamma_0=\gamma\land\forall(i\in k)(\gamma_i\textrm{ is }(\lambda\xi.\gamma_{i+1})\textrm{-shrewd}))\}):k\in\mathbb{N}\}\) (this definition uses constant functions in the functional-shrewdness)

Define a set of ordered tuples \(\textrm{RI}\):

  • \(()\in\textrm{RI}\)
  • For \(\mathbb X,\mathbb Y,\mathbb Z\in\textrm{RI}\), \(\kappa\in\{\gamma\in\Upsilon:\gamma\textrm{ is }(\gamma^+)\textrm{-shrewd}\}\), \(\beta\in\textrm{Ord}\), and \(\alpha\in\textrm{Ord}\), then \((\mathbb X,\mathbb Z,\kappa,\beta,\alpha,\mathbb Y)\in\textrm{RI}\)

Define a function \(\textrm{V}:\textrm{RI}\rightarrow \mathcal P(\textrm{Ord})\), called "ordinals":

  • \(\textrm{V}():=\varnothing\)
  • \(\textrm{V}(\mathbb X,\mathbb Z,\kappa,\beta,\alpha,\mathbb Y):=\{\alpha,\kappa,\beta\}\cup\textrm{V}\mathbb X\cup\textrm{V}\mathbb Y\cup\textrm{V}\mathbb Z\)

Let \(\textrm{SC}\) denote the set of (+1)-shrewd cardinals \(\le\Upsilon\), let \(\pi,\kappa\) range over \(\textrm{SC}\), and let \(\mathbb X,\mathbb Y\) range over \(\textrm{RI}\).

For \(\alpha,\beta\in\textrm{Ord}\), define \(C(\alpha,\beta)\subset\textrm{Ord}\) by transfinite recursion in \(\alpha\):

  • \(C_0(\alpha,\beta)\ :=\ \beta\cup\{0,\Upsilon\}\)
  • \(C_{i+1}(\alpha,\beta)\ :=\ \{\gamma+\delta,\omega^\gamma:\gamma,\delta\in C_i(\alpha,\beta)\} \\ \phantom{C_{i+1}(\alpha,\beta)\ :=}\cup\{\psi^{\mathbb Y}_\kappa(\eta):\kappa,\gamma\in C_i(\alpha,\beta)\land\eta\in\alpha\land\textrm{V}\mathbb Y\subseteq C_i(\alpha,\beta)\cap\alpha\}\)
  • \(C(\alpha,\beta)\ :=\ \bigcup\{C_i(\alpha,\beta):i\in\mathbb{N}\}\)

For \(\pi\in\textrm{SC}\) and \(\mathbb X\in\textrm{RI}\), define \(A_\pi\mathbb X\subseteq\Upsilon\):

  • \(A_\pi()\ :=\ \pi\)
  • \(A_\pi(\mathbb X,\mathbb Z,\kappa,\beta,0,\mathbb Y)\ :=\ A_\pi\mathbb Y\)
  • \(\text{For }\alpha>0:\ A_\pi(\mathbb X,\mathbb Z,\kappa,\beta,\alpha,\mathbb Y)\ :=\ \{\gamma\in A_\pi\mathbb X:C(\alpha,\gamma)\cap\pi\subseteq\gamma\;\land \\ \phantom{\{\gamma\in A_\pi\mathbb{X}:}\;\forall(\xi\in C(\alpha,\gamma)\cap\alpha)(\gamma\textrm{ is Shr}^{\mathbb Z}_\kappa\textrm{-}\beta\textrm{ on }A_\pi(\mathbb X,\mathbb Z,\kappa,\beta,\xi,\mathbb Y))\}\)

For \(\alpha\in\textrm{Ord}\), \(\pi\in\textrm{SC}\), and \(\mathbb X\in\textrm{RI}\), define \(\psi^{\mathbb X}_\pi(\alpha)\in\Upsilon\):

  • \(\psi^{\mathbb X}_\pi(\alpha)\ :=\ \textrm{min}\{\beta\in A_\pi\mathbb X:C(\alpha,\beta)\cap\pi\subseteq\beta\}\cup\{\pi\}\)

Restrict \(f\) to inflationary functions (\(f\) is inflationary iff \(\forall(\beta\in\textrm{Domain of }f)(\beta<f(\beta))\)).

For \(\beta\in\Upsilon\) and \(\delta\in\textrm{Ord}\) and \(s\subseteq\textrm{Ord}\), "\(\beta\text{ is Shr}^{\mathbb Z}_\kappa\textrm{-}\delta\text{ on }s\)" is defined as this condition:

  • \(\forall(\delta'\in C(\delta,\beta)\cap\delta) \\ \phantom{\forall}(\exists(f:\Upsilon\rightarrow\Upsilon)(\text{Least }f\text{-shrewd on }s >\textrm{min}\{\gamma:\gamma \text{ is Shr}^{\mathbb Z}_{\kappa}\textrm{-}\delta'\text{ on }s\} \\ \phantom{\forall(\exists(f:\Upsilon\rightarrow\Upsilon)}\,\land\beta \text{ is }f\text{-shrewd on }s) \\ \phantom{\forall}\land C(\delta,\beta)\cap\kappa\subseteq\beta \\ \phantom{\forall}\land f(\beta)\in A_\Upsilon\mathbb Z)\)

Theorems

Theorem: Let \(\textrm{Cl}(A)\) denote \(A\cup\{\alpha:\alpha=\textrm{sup}(A\cap\alpha)\}\), and let \(\textrm{Enum}(A)\) denote the unique strictly increasing function with domain exactly \(A\). Let \(\nu\) denote the least cardinal that is (next ((+1)-shrewd on (+1)-shrewds) after _)-shrewd. If \(\beta\) is \(\textrm{Shr}^{((),(),\Upsilon?,1,1,())}_\nu\textrm{-}\nu\) on \(\textrm{Ord}\), then \(\beta\) is shrewd up to a maximal ordinal \(\beta'\) that is (+1)-shrewd and \(\exists !\gamma(\textrm{Enum}(\textrm{Cl}(\textrm{SC}))(\gamma)=\beta'\land\gamma\textrm{ is a limit ordinal})\).

Proof: Analogous to here

Proposition: \(\gamma\in A_\Upsilon\mathbb W\) implies \(\gamma\) is (+1)-shrewd and \(<\Upsilon\). This will be used in the proof of the following theorem

Theorem: \(A_\pi((),\mathbb W,\Upsilon,1,1,())\) is exactly the set of doubly-(+1)-shrewd ordinals (i.e. ordinals that are (next (+1)-shrewd after _)-shrewd) less than \(\pi\), where \(\mathbb W\) denotes the reflection encoding \(((),(),\Upsilon,1,1,())\).

Proof: This is equivalent to the statement "\(\gamma\in A_\pi((),\mathbb W,1,())\leftrightarrow\gamma\in\pi\land\gamma\textrm{ is doubly-(+1)-shrewd}\)". Let \(\gamma\in A_\pi((),\mathbb W,1,())\). We now analyze the condition \(\textrm{Shr}^{\mathbb W}_\Upsilon\textrm -1\):

  • Ordinal \(\gamma\) has condition \(\textrm{Shr}^{\mathbb W}_\Upsilon\textrm -0\) if it's \(<\Upsilon\) by vacuous truth,
  • Ordinal \(\gamma\) has condition \(\textrm{Shr}^{\mathbb W}_\Upsilon\textrm -1\) if it's \(<\Upsilon\) and shrewd up to an ordinal that is (+1)-shrewd (because \(f(\gamma)\in A_\Upsilon\mathbb W\) for such existentially quantified \(f\))

Since \(\delta\)-shrewdness implies \(\delta'\)-shrewdness for all \(\delta'\in\delta\)[2], then \(\gamma\) must be (next (+1)-shrewd after γ)-shrewd. So it's doubly-(+1)-shrewd.

Conversely, assume that \(\gamma\) is (next (+1)-shrewd after γ)-shrewd. WIP

OCF up to a nonrecursive analogue of a Σ_2-admissible ordinal

Possible future project

Sources