Successor OCF Based on Weakly Compact Cardinals

This is an English translation of my Japanese blog post submitted to a Japanese googological event. Usually, I hesitate to submit a large number defined by an OCF without an associated ordinal notation, because it should be classified in the realm of uncomputable googology, in which OCFs are not as powerful as other standard tools. On the other hand, this event is a competition on ”how impressive”, and the rule accepts any numbers greater than or equal to \(1000000\). Therefore I do not have to care about the uncomputability of my OCF, which is a variant of Rathjen's OCF based on the least weakly compact cardinal.

By the way, could someone tell me who asked me questions on a successor OCF? The motivation of my OCF is derived from our discussion about how strong a successor OCF can be, and hence I would like to tell the user my work. Unfortunately, I forgot where we discussed it.

See also my study on a similar attempt: an implementation of Extended Weak Buchholz's OCF, which is an OCF based on no function created by a Japanese googologist Gaoji. It does not use even the successor function as a portion of the OCF.

Characters

🍰

It stands for 埴安神袿姫 (Haniyasushin Cake). She is a Japanese Goddess, whose skill is to create an animated idol. One of the most famous idols in ancient Japan is a doll called "埴輪 (haniwa)", which is made from dirt and water.

┌|∵|┘

It stands for 杖刀偶磨弓 (Johtohgu Mayumi). She is a haniwa-servant of 🍰, whose skill is to directly convert her loyalty into strength.

Prologue

🍰「I've completed a new spell to create \(n\) haniwae for any specific number \(n\) ! But it can be activated only once. So \(n\) should be defined to be as large as possible.」

🍰「...Dear me! I can't think of anything greater than \(999999\) !」

┌|∵|┘「Excuse me. I have heard that it suffices to use a strong function in order to create a large number.」

🍰「Thanks. But I don't know a strong function.」

┌|∵|┘「I... also do not know a function other than the successor function...」

🍰「Then I order you to strengthen a function by your skill to convert your loyalty.」

┌|∵|┘「Sure!」

┌|∵|┘「...Pardon me?」

└|∵|┘「URYYYYYYYYYYYY!!!!」

How to Play

┌|∵|┘oO(　)

It exhibits her loyalty toward 🍰.

The more times ┌|∵|┘ prays for 🍰, the more her loyalty grows.

Since she is ordered to strive for strength, praying for strength also raises her loyalty a little.

└|∵|┘(　)

It exhibits the Loyalty Collapsing Function. It raises strenth, and also converts her loyalty into strength.

In order to make 🍰's wish come true, ┌|∵|┘ strengthens a function until her loyalty is exhausted.

Convention

I denote by \(\textrm{Ord}\) the class of ordinals, by \(\textrm{Reg} \subset \textrm{Ord}\) the subclass of uncountable regular cardinals, and by \(\textrm{Cmp} \subset \textrm{Reg}\) the subclass of weakly compact cardinals.

For a class \(X\), I denote by \(\mathcal{P}(X)\) the class of subsets of \(X\), and by \(S(X) \subset \textrm{Ord}\) the subclass of ordinals \(\pi\) satisying the following:

1. \(\pi \in \textrm{Reg}\).
2. \(C \cap X \neq \emptyset\) for any club set \(C \subset \pi\).

I work in \(\textrm{ZFC}\) augmented by \(\bigcap_{n \in \mathbb{N}} S^n(\textrm{Cmp}) \neq \emptyset\), and put \(\textrm{🍰} := \min \bigcap_{n \in \mathbb{N}} S^n(\textrm{Cmp})\).

Loyalty Collapsing Function

I simultaneously define maps \begin{eqnarray*} \begin{array}{ccrcl} C & \colon & \textrm{Ord}^2 & \to & \mathcal{P}(\textrm{Ord}) \\ & & (\alpha,\beta) & \mapsto & C(\alpha,\beta) \\ & & & & \\ M & \colon & \textrm{Ord} & \to & \mathcal{P}(\textrm{🍰}) \\ & & \alpha & \mapsto & M(\alpha) \\ & & & & \\ \textrm{┌|∵|┘oO} & \colon & \textrm{Ord} & \to & \textrm{🍰}+1 \\ & & \alpha & \mapsto & \textrm{┌|∵|┘oO}(\alpha) \\ & & & & \\ \textrm{└|∵|┘} & \colon & \textrm{Ord}^3 & \to & \textrm{🍰} \\ & & (\pi,\xi,\alpha) & \mapsto & \textrm{└|∵|┘}(\pi,\xi,\alpha) \end{array} \end{eqnarray*} in the following transfinitely inductive way on \(\alpha\):

Definition of \(C(\alpha,\beta)\)

1. For each \(n \in \mathbb{N}\), define \(C_n(\alpha,\beta) \in \mathcal{P}(\textrm{Ord})\) in the following inductive way：
   1. If \(n = 0\), then \(C_n(\alpha,\beta) := \beta \cup \{0,\textrm{🍰}\}\).
   2. If \(n \neq 0\), then \(C_n(\alpha,\beta)\) is the union of the following four sets:
      1. \(C_{n-1}(\alpha,\beta)\)
      2. \(\{\gamma+1 \mid \gamma \in C_{n-1}(\alpha,\beta)\}\)
      3. \(\{\textrm{┌|∵|┘oO}(\gamma) \mid \gamma \in C_{n-1}(\alpha,\beta) \cap \alpha\}\)
      4. \(\{\textrm{└|∵|┘}(\pi,\xi,\gamma) \mid (\pi,\xi,\gamma) \in C_{n-1}(\alpha,\beta)^3 \land \pi \in \textrm{Reg} \cap \textrm{🍰} \land \xi \subset \gamma \in \alpha\}\)
2. Set \(C(\alpha,\beta) := \bigcup_{n \in \mathbb{N}} C_n(\alpha,\beta)\).

Definitions of \(M(\alpha)\), \(\textrm{┌|∵|┘oO}(\alpha)\), and \(\textrm{└|∵|┘}(\pi,\xi,\alpha)\)

1. If \(\alpha \neq \textrm{🍰}\), then \(M(\alpha) := \{\pi \in \textrm{🍰} \mid C(\alpha,\pi) \cap \textrm{🍰} = \pi \land \forall \xi \in C(\alpha,\pi) \cap \alpha, \pi \in S(M(\xi))\}\).
2. If \(\alpha = \textrm{🍰}\), then \(M(\alpha) := \textrm{Cmp}\).
3. Set \(\textrm{┌|∵|┘oO}(\alpha) := \min (M(\alpha) \cup \{\textrm{🍰}\})\).
4. If \(\pi \in \textrm{Reg} \cap \textrm{🍰}\) and \(\xi \subset \alpha\), then \(\textrm{└|∵|┘}(\pi,\xi,\alpha) := \min (\{\beta \in M(\xi) \cap \pi \mid C(\alpha,\beta) \cap \pi = \beta \land (\pi,\alpha) \in C(\alpha,\beta)^2\} \cup \{\pi\})\).
5. If \(\pi \notin \textrm{Reg} \cap \textrm{🍰}\) or \(\alpha \in \xi\), then \(\textrm{└|∵|┘}(\pi,\xi,\alpha) := 0\).

Haniwa Hanierarchy

I define a map \begin{eqnarray*} [ \ ] \colon C(\textrm{🍰} + \textrm{┌|∵|┘oO}(0),0) \times \mathbb{N} & \to & C(\textrm{🍰} + \textrm{┌|∵|┘oO}(0),0) \\ (\alpha,n) & \mapsto & \alpha[n] \end{eqnarray*} in the following way:

1. If \(\alpha = 0\), then \(\alpha[n] := 0\).
2. If \(\alpha\) is a successor ordinal, then \(\alpha[n] := \max \alpha\).
3. If \(\alpha\) is a non-zero limit ordinal, then \(\alpha[n] := \max (C_n(\textrm{🍰} + \textrm{┌|∵|┘oO}(0),0) \cap \alpha)\).

I note that if \(\alpha\) satisfies \(C(\textrm{🍰} + \textrm{┌|∵|┘oO}(0),0) \cap \alpha = \alpha\), then \(\alpha\) is a countable ordinal, and in addition if \(\alpha\) is a non-zero limit ordinal, then \(\alpha[n]\) forms a fundamental sequence of \(\alpha\). On the other hand, \(\alpha[n]\) is defined even if \(\alpha\) is uncountable or even of uncountable cofinality, and forms an unbounded sequence of the countable well-ordered set \((C(\textrm{🍰} + \textrm{┌|∵|┘oO}(0),0) \cap \alpha,\in)\), i.e. a fundamental sequence of \(\alpha\) as a valid expression in this system.

I define a map \begin{eqnarray*} \textrm{埴埴} \colon C(\textrm{🍰} + \textrm{┌|∵|┘oO}(0),0) \times \mathbb{N} & \to & \mathbb{N} \\ (\alpha,n) & \mapsto & \textrm{埴埴}(\alpha,n) \end{eqnarray*} in the following transfinitely inductive way on \(\alpha\):

1. If \(\alpha = 0\), then \(\textrm{埴埴}(\alpha,n) := n+1\).
2. If \(\alpha \neq 0\), then \(\textrm{埴埴}(\alpha,n) := \textrm{埴埴}(\alpha[n],n+1)\).

By the well-foundedness of \((C(\textrm{🍰} + \textrm{┌|∵|┘oO}(0)),\in)\) and the decreasing property of \([ \ ]\) with respect to \(\in\), \(\textrm{埴埴}\) is well-defined on \(C(\textrm{🍰} + \textrm{┌|∵|┘oO}(0)) \times \mathbb{N}\).

Epilogue

┌|∵|┘「I HAVE DONE!」

🍰「Excellent. Let's activate the spell.」

┌|∵|┘「OKAY!」

🍰「...」

┌|∵|┘「...」

🍰「...」

┌|∵|┘「...?」

🍰「Since the number is too large, the spell seems to have required unrealistic amount of dirt and water. It terminated with an error. It created no haniwa.」

┌|∵|┘「...」

└|∵|┘「URYYYYYYYYYYYY!!!!」