Japanese version: https://googology.wikia.org/ja/wiki/%E3%83%A6%E3%83%BC%E3%82%B6%E3%83%BC%E3%83%96%E3%83%AD%E3%82%B0:Kanrokoti/2%E9%87%8D%CF%88%E9%96%A2%E6%95%B0
Overview[]
We define Double-psi Function. This notation extends Ordinal Notation Associated to Extended Buchholz's OCF to 3 variables.
This notation has a high possibility of being broken.
Double-psi Function calculator by Naruyoko
Special thanks: p進大好きbot C7X Mrna den
Difference from Kumakuma 3 variables ψ[]
Unlike Kumakuma 3 variables ψ, this notation is defined \(\textrm{dom}(\psi_0(\psi_1(0,0),0)) = \psi_0(\psi_1(0,0),0)\). This setting generates the element of 2-stage side nesting in the definition of dom. Because of this, \(\psi_0(\psi_1(0,0),0)\) in Double-psi Function plays the role of \(\psi_1(0,0)\) in Kumakuma 3 variables ψ.
Since Double-psi Function is 2-stage side nesting notation of 3 variables ψ, the element of 2-stage side nesting appears only in the relationship between the first and second variables unlike 3 variableized 2-stage side nesting notation. 3 variableized 2-stage side nesting notation would have the element of 2-stage side nesting in the relationship between the second and third variables, the first and second variables, and the first and third variables. Therefore, we can expect that Double-psi Function is weaker than 3 variableized 2-stage side nesting notation.
Double-psi Function[]
Notation[]
Here, we define character strings used for the notation.
Let \(T\) and \(PT\) are sets of formal strings consisting of \(0\), \(+\), \(\psi\), \((\), \()\), and a comma "\(,\)", 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,c) \in T^3\), \(\psi_a(b,c) \in PT \cap T\).
Abbreviation[]
\(0\) is abbreviated as \($0\), \(\psi_0(0,0)\) is abbreviated as \($1\), for \(n \in (\mathbb{N} \setminus \{0,1\})\), \(\underbrace{$1+ \dots +$1}_{n ~ $1's}\) is abbreviated as \($n\), and \(\psi_0(0,$1)\) is abbreviated as \($\omega\).
Ordering[]
Here, we define a magnitude relationship on \(T\) in the dictionary order.
\(2\)-ary relations \(s \le t\) and \(s \lt t\) on \(T\) are simultaneously defined in the following recursive way:
- Definition of \(s \le t\)
- If \(s = t\), then \(s \le t\) is true.
- If \(s \neq t\), then \(s \le t\) is equivalent to \(s \lt t\).
- Definition of \(s \lt t\)
- If \(t = 0\), then \(s \lt t\) is false.
- If \(t \neq 0\) and \(s = 0\), then \(s \lt t\) is true.
- Suppose \(t \neq 0\) and \(s = a+b\) for some \((a,b) \in PT \times (T \setminus \{0\})\).
- If \(t = c+d\) for some \((c,d) \in PT \times (T \setminus \{0\})\), then \(s \lt t\) is equivalent to that either one of the following holds:
- \(a \lt c\).
- \(a = c\) and \(b \lt d\).
- If \(t = \psi_c(d,e)\) for some \((c,d,e) \in T^3\), then \(s \lt t\) is equivalent to \(a \lt t\).
- If \(t = c+d\) for some \((c,d) \in PT \times (T \setminus \{0\})\), then \(s \lt t\) is equivalent to that either one of the following holds:
- Suppose \(t \neq 0\) and \(s = \psi_a(b,c)\) for some \((a,b,c) \in T^3\).
- If \(t = d+e\) for some \((d,e) \in PT \times (T \setminus \{0\})\), then \(s \lt t\) is equivalent to \(s \le d\).
- If \(t = \psi_d(e,f)\) for some \((d,e,f) \in T^3\), then \(s \lt t\) is equivalent to that either one of the following holds:
- \(a \lt d\).
- \(a = d\) and \(b \lt e\).
- \(a = d\) and \(b = e\) and \(c \lt f\).
Cofinality[]
Here, we define cofinality on \(T\).
A computable total map \begin{eqnarray*} \textrm{dom} \colon T & \to & T \\ s & \mapsto & \textrm{dom}(s) \end{eqnarray*} is defined in the following recursive way:
- If \(s = 0\), then \(\textrm{dom}(s) := 0\).
- If \(s = a+b\) for some \((a,b) \in PT \times (T \setminus \{0\})\), then \(\textrm{dom}(s) := \textrm{dom}(b)\).
- Suppose \(s = \psi_a(b,c)\) for some \((a,b,c) \in T^3\).
- Suppose \(\textrm{dom}(c) = 0\).
- Suppose \(\textrm{dom}(b) = 0\).
- If \(\textrm{dom}(a) \in \{0,$1\}\), then \(\textrm{dom}(s) := s\).
- Otherwise, then \(\textrm{dom}(s) := \textrm{dom}(a)\).
- If \(\textrm{dom}(b) = $1\), then \(\textrm{dom}(s) := s\).
- Suppose \(\textrm{dom}(b) \notin \{0,$1\}\).
- If \(\textrm{dom}(b) \lt s\), then \(\textrm{dom}(s) := \textrm{dom}(b)\).
- Otherwise, then there is \((d,e) \in T^2\) satisfying \(\textrm{dom}(b) = \psi_d(e,0)\).
- If \(\textrm{dom}(e) = 0\), then \(\textrm{dom}(s) := s\).
- Otherwise, then \(\textrm{dom}(s) := $\omega\).
- Suppose \(\textrm{dom}(b) = 0\).
- If \(\textrm{dom}(c) = $1\), then \(\textrm{dom}(s) := $\omega\).
- Suppose \(\textrm{dom}(c) \notin \{0,$1\}\).
- If \(\textrm{dom}(c) \lt s\), then \(\textrm{dom}(s) := \textrm{dom}(c)\).
- Otherwise, then \(\textrm{dom}(s) := $\omega\).
- Suppose \(\textrm{dom}(c) = 0\).
Search Function[]
Here, we define Search Function.
A computable total map \begin{eqnarray*} \textrm{BP} \colon T^2 & \to & T \\ (s,t) & \mapsto & \textrm{BP}(s,t) \end{eqnarray*} is defined in the following recursive way:
- If \(s = 0\), then \(\textrm{BP}(s,t) := 0\).
- Suppose \(s = \psi_a(b,c)+s'\) for some \((a,b,c,s') \in T^3 \times (T \setminus \{0\})\).
- If \(t \lt a\), then \(\textrm{BP}(s,t) := s\).
- Otherwise, then \(\textrm{BP}(s,t) := \textrm{BP}(s',t)\).
- Suppose \(s = \psi_a(b,c)\) for some \((a,b,c) \in T^3\).
- If \(t \lt a\), then \(\textrm{BP}(s,t) := s\).
- Suppose \(a \le t\).
- If \(b \lt s\), then \(\textrm{BP}(s,t) := s\).
- Otherwise, then \(\textrm{BP}(s,t) := \textrm{BP}(b,t)\).
Fundamental Sequence[]
Here, we define a fundamental sequence on \(T\).
A computable total map \begin{eqnarray*} [ \ ] \colon T^2 & \to & T \\ (s,t) & \mapsto & s[t] \end{eqnarray*} is defined in the following recursive way:
- If \(s = 0\), then \(s[t] := 0\).
- If \(s = a+b\) for some \((a,b) \in PT \times (T \setminus \{0\})\), then put \(b' := b[t]\).
- If \(b' = 0\), then \(s[t] := a\).
- Otherwise, then \(s[t] := a+b'\).
- Suppose \(s = \psi_a(b,c)\) for some \((a,b,c) \in T^3\).
- Suppose \(\textrm{dom}(c) = 0\).
- Suppose \(\textrm{dom}(b) = 0\).
- If \(\textrm{dom}(a) \in \{0,$1\}\), then \(s[t] := t\).
- Otherwise, then \(s[t] := \psi_{a[t]}(b,c)\).
- If \(\textrm{dom}(b) = $1\), then \(s[t] := t\).
- Suppose \(\textrm{dom}(b) \notin \{0,$1\}\).
- If \(\textrm{dom}(b) \lt s\), then \(s[t] := \psi_a(b[t],c)\).
- Otherwise, then there is \((d,e) \in T^2\) satisfying \(\textrm{dom}(b) = \psi_d(e,0)\).
- Suppose \(\textrm{dom}(e) = 0\).
- If \(t = 0\), then \(s[t] := \psi_a(b[\psi_{d[0]}(e,0)],c)\).
- If \(t = $i\) for some \(i \in (\mathbb{N} \setminus \{0\})\) and \(s[t[0]] = \psi_a(\Gamma,c)\) for an unique \(\Gamma \in T\), then \(s[t] := \psi_a(b[\psi_{d[0]}(\Gamma,0)],c)\).
- If neither of above, then \(s[t] := \psi_a(b[t],c)\).
- Suppose \(\textrm{dom}(e) = $1\).
- If \(t = $i\) for some \(i \in (\mathbb{N} \setminus \{0\})\) and \(s[t[0]] = \psi_a(\Gamma,c)\) for an unique \(\Gamma \in T\), then \(s[t] := \psi_a(b[\psi_d(e[0],\Gamma)],c)\).
- Otherwise, then \(s[t] := \psi_a(b[\psi_d(e[0],0)],c)\).
- Suppose \(\textrm{dom}(e) = \psi_f(0,0)\) for some \(f \in (T \setminus \{0\})\).
- If \(t = 0\), then \(s[t] := \psi_a(b[0],c)\).
- If \(t = $i\) for some \(i \in (\mathbb{N} \setminus \{0\})\) and \(s[t[0]] = \psi_a(\Gamma,c)\) for an unique \(\Gamma \in T\), then \(s[t] := \psi_a(b[\psi_{f[0]}(\textrm{BP}(\Gamma,f[0]),0)],c)\).
- If neither of above, then \(s[t] := \psi_a(b[t],c)\).
- Suppose \(\textrm{dom}(e) = 0\).
- Suppose \(\textrm{dom}(b) = 0\).
- Suppose \(\textrm{dom}(c) = $1\).
- If \(t = t[0]+$1\), then \(s[t] := s[t[0]]+s[$1]\).
- Otherwise, then \(s[t] := \psi_a(b,c[0])\).
- Suppose \(\textrm{dom}(c) \notin \{0,$1\}\).
- If \(\textrm{dom}(c) \lt s\), then \(s[t] := \psi_a(b,c[t])\).
- Otherwise, then there is \((d,e) \in T^2\) satisfying \(\textrm{dom}(c) = \psi_d(e,0)\).
- Suppose \(\textrm{dom}(e) = 0\).
- If \(t = $i\) for some \(i \in (\mathbb{N} \setminus \{0\})\) and \(s[t[0]] = \psi_a(b,\Gamma)\) for an unique \(\Gamma \in T\), then \(s[t] := \psi_a(b,c[\psi_{d[0]}(\Gamma,0)])\).
- Otherwise, then \(s[t] := \psi_a(b,c[\psi_{d[0]}(e,0)])\).
- Suppose \(\textrm{dom}(e) = $1\).
- If \(t = $i\) for some \(i \in (\mathbb{N} \setminus \{0\})\) and \(s[t[0]] = \psi_a(b,\Gamma)\) for an unique \(\Gamma \in T\), \(s[t] := \psi_a(b,c[\psi_d(e[0],\Gamma)])\).
- Otherwise, then \(s[t] := \psi_a(b,c[\psi_d(e[0],0)])\).
- Suppose \(\textrm{dom}(e) = \psi_f(0,0)\) for some \(f \in (T \setminus \{0\})\).
- If \(t = 0\), then \(s[t] := \psi_a(b,c[0])\).
- If \(t = $i\) for some \(i \in (\mathbb{N} \setminus \{0\})\) and \(s[t[0]] = \psi_a(b,\Gamma)\) for an unique \(\Gamma \in T\), then \(s[t] := \psi_a(b,c[\psi_{f[0]}(\textrm{BP}(\Gamma,f[0]),0)])\).
- If neither of above, then \(s[t] := \psi_a(b,c[t])\).
- Suppose \(\textrm{dom}(e) = 0\).
- Suppose \(\textrm{dom}(c) = 0\).
FGH[]
Here, we define FGH using \(T\).
A computable partial map \begin{eqnarray*} f \colon T \times \mathbb{N}^2 & \to & \mathbb{N} \\ (s,m,n) & \mapsto & f_s^m(n) \end{eqnarray*} is defined in the following recursive way:
- If \(m = 0\), then \(f_s^m(n) := n\).
- Suppose \(m = 1\).
- If \(s = 0\), then \(f_s^m(n) := n+1\).
- Suppose \(s \neq 0\).
- If \(\textrm{dom}(s) = $1\), then \(f_s^m(n) := f_{s[0]}^n(n)\).
- Otherwise, then \(f_s^m(n) := f_{s[$n]}^1(n)\).
- If \(m \notin \{0,1\}\), then \(f_s^m(n) := f_s^1(f_s^{m-1}(n))\).
Limit of the notation[]
Here, we define a limit of the notation.
A computable total map \begin{eqnarray*} \Lambda \colon \mathbb{N} & \to & PT \\ n & \mapsto & \Lambda(n) \end{eqnarray*} is defined in the following recursive way:
- If \(n = 0\), then \(\Lambda(n) := \psi_0(0,0)\).
- Otherwise, then \(\Lambda(n) := \psi_{\Lambda(n-1)}(0,0)\).
Standard Form[]
Here, we define a standard form of the notation.
A subset \(OT \subset T\) is defined in the following recursive way:
- For any \(n \in \mathbb{N}\), \(\psi_0(0,\Lambda(n)) \in OT\).
- For any \((s,n) \in OT \times \mathbb{N}\), \(s[$n] \in OT\).
My expectation is that \((OT,\lt)\) is an ordinal notation, or \(OT\) is recursive and the restriction of \(\lt\) to \(OT\) is well-ordered.
Naming[]
A computable total map \begin{eqnarray*} F \colon \mathbb{N} & \to & \mathbb{N} \\ n & \mapsto & F(n) \end{eqnarray*} is defined as \(F(n) = f_{\psi_0(0,\Lambda(n))}(n)\).
I name \(F^{10^{100}}(10^{100})\) "Double-psi Number".
I name an ordinal which correspond to the limit of Double-psi Function "Double-psi ordinal" (DPO).