Overview[]
Side nesting is one of the nesting structure concept introduced by Mrna den, and explained in 横ネストについて. Now(2020～2021) in Japanese community, side nesting is one of the main object of study for nesting/array notation.
My thought about side nesting in dom-type notation is highly based on what I know, and hence it may be different from actual side nesting/dom-type notation. So, take my thought with a pinch of salt.
dom-type notation[]
The term "dom-type notation" (or dom-type/dom-type definition/dom-type nesting notation) was introduced by p進大好きbot in Japanese community. "norm-type" is the counterpart of dom-type. Notation \(T\) is dom-type if a map \begin{eqnarray*} \textrm{dom} \colon T & \to & T \\ s & \mapsto & \textrm{dom}(s) \end{eqnarray*} outputs cofinality on \(T\) is defined. As far as a map returns cofinality on \(T\), there is no need to use \(\textrm{dom}\) as name or being one variable.
Since side nesting is not defined for dom-type, it is difficult to say what is the element of side nesting in dom-type.
In this blog post, we call \(s \in T\) regular cardinal if \(s\) satisfies \(\textrm{dom}(s) = s\).
The element of side nesting in the definition of dom[]
First, we fix the notation \(T\) as follows:
Let \(T\) and \(PT\) are sets of formal strings consisting of \(0\), \(+\), \(\psi\), \((\), and \()\), which are simultaneously defined in the following recursive way:
- \(0 \in T\).
- For any \((a,b) \in PT \times (T \setminus \{0\})\), \(a+b \in T\).
- For any \((a,b) \in T^2\), \(\psi_a(b) \in PT \cap T\).
On notation \(T\), we use \($0\), \($1\), \($\omega\) which are expected to be ordinals \(0\), \(1\), \(\omega\). In this time, we set \($0 = 0\), \($1 = \psi_0(0)\), \($\omega = \psi_0(\psi_0(0)) = \psi_0($1)\). Also, we assume that the magnitude relationship on \(T\), or 2-ary relations \(\lt\) on \(T\) is defined.
0-stage side nesting[]
Notation \(T\) is 0-stage side nesting notation if
- Regular cardinal \(s \in T\) is \($0,$1,$\omega\) only.
holds.
We call \($0,$1,$\omega\) 0-stage regular cardinal, and we denote by \(R_0 \subset T\) the set of 0-stage regular cardinals, meaning \(R_0 = \{$0,$1,$\omega\}\).
1-stage side nesting[]
Notation \(T\) is 1-stage side nesting notation if
- There is a regular cardinal \(s \in T\) satisfying \(s \notin R_0\). We call this 1-stage regular cardinal, and we denote by \(R_1 \subset T\) the set of 1-stage regular cardinals.
- For any \(s \in R_1\), there is an \(a \in (T \setminus \{0\})\) satisfying \(s = ψ_a(0)\).
holds.
For example in Ordinal Notation Associated to Extended Buchholz's OCF, \(ψ_a(0)\) satisfying \(\textrm{dom}(a) = $1\) is a 1-stage regular cardinal.
2-stage side nesting[]
Notation \(T\) is 2-stage side nesting notation if
- There is a regular cardinal \(s \in T\) satisfying \(s \notin (R_0 \cup R_1)\). We call this 2-stage regular cardinal, and we denote by \(R_2 \subset T\) the set of 2-stage regular cardinals.
- For any \(s \in R_2\), there is a \((a,b) \in T^2\) satisfying \(s = ψ_a(b)\) and \(s \lt \textrm{dom}(b)\) and \(\textrm{dom}(b) \in R_1\).
holds.
3-stage side nesting[]
Notation \(T\) is 3-stage side nesting notation if
- There is a regular cardinal \(s \in T\) satisfying \(s \notin (R_0 \cup R_1 \cup R_2)\). We call this 3-stage regular cardinal, and we denote by \(R_3 \subset T\) the set of 3-stage regular cardinals.
- For any \(s \in R_3\), there is a \((a,b) \in T^2\) satisfying \(s = ψ_a(b)\) and \(s \lt \textrm{dom}(b)\) and \(\textrm{dom}(b) \in R_2\).
holds.
4-stage side nesting[]
Notation \(T\) is 4-stage side nesting notation if
- There is a regular cardinal \(s \in T\) satisfying \(s \notin (R_0 \cup R_1 \cup R_2 \cup R_3)\). We call this 4-stage regular cardinal, and we denote by \(R_3 \subset T\) the set of 4-stage regular cardinals.
- For any \(s \in R_4\), there is a \((a,b) \in T^2\) satisfying \(s = ψ_a(b)\) and \(s \lt \textrm{dom}(b)\) and \(\textrm{dom}(b) \in R_3\).
holds.
If we only see the definitions of dom, I think TSS-ψ Function and Hyper Primitive psi Function are at least ω-stage side nesting notations.
For more details, see Japanese version.