Overview[]
This notation has a high possibility of being broken.
三 function is defined by p進大好きbot. As you can see, 三 function has the restriction in the definition of \(\textrm{dom}\) in order to define 三 function easier.
In this blog post, I attempt to get rid of the restriction. To do that, I introduce original algorithms, and hence I'm not sure if this work.
I appreciate p進大好きbot and Mrna den helping my work.
I appreciate Naruyoko making Non-restricted 三 function calculator.
Non-restricted 三 function[]
Notation[]
Let \(T\) and \(PT\) are sets of formal strings consisting of \(0\), \(+\), \(\textrm{三}\), \((\), 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\), \(\textrm{三}_a(b) \in PT \cap T\).
Abbreviation[]
\(0\) is abbreviated as \($0\), \(\textrm{三}_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 \(\textrm{三}_0($1)\) is abbreviated as \($\omega\).
Ordering[]
\(2\)-ary relations \(s \leq t\) and \(s < t\) on \(T\) are simultaneously defined in the following recursive way:
- Definition of \(s \leq t\)
- If \(s = t\), then \(s \leq t\) is true.
- If \(s \neq t\), then \(s \leq t\) is equivalent to \(s < t\).
- Definition of \(s < t\)
- If \(t = 0\), then \(s < t\) is false.
- If \(t \neq 0\) and \(s = 0\), then \(s < t\) is true.
- Suppose that \(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 < t\) is equivalent to that either one of the following holds:
- \(a < c\).
- \(a = c\) and \(b < d\).
- If \(t = \textrm{三}_c(d)\) for some \((c,d) \in T^2\), then \(s < t\) is equivalent to \(a < t\).
- If \(t = c+d\) for some \((c,d) \in PT \times (T \setminus \{0\})\), then \(s < t\) is equivalent to that either one of the following holds:
- Suppose that \(t \neq 0\) and \(s = \textrm{三}_a(b)\) for some \((a,b) \in T^2\).
- If \(t = c+d\) for some \((c,d) \in PT \times (T \setminus \{0\})\), then \(s < t\) is equivalent to \(s \leq c\).
- If \(t = \textrm{三}_c(d)\) for some \((c,d) \in T^2\), then \(s < t\) is equivalent to that either one of the following holds:
- \(a < c\).
- \(a = c\) and \(b < d\).
Cofinality[]
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 that \(s = \textrm{三}_a(b)\) for some \((a,b) \in T^2\).
- Suppose that \(\textrm{dom}(b) = 0\).
- If \(\textrm{dom}(a) \in \{0,$1\}\), then \(\textrm{dom}(s) := s\).
- If \(\textrm{dom}(a) \notin \{0,$1\}\), then \(\textrm{dom}(s) := \textrm{dom}(a)\).
- If \(\textrm{dom}(b) = $1\), then \(\textrm{dom}(s) := $\omega\).
- Suppose that \(\textrm{dom}(b) \notin \{0,$1\}\).
- If \(\textrm{dom}(b) \lt s\), then \(\textrm{dom}(s) := \textrm{dom}(b)\).
- If \(s \le \textrm{dom}(b)\), then there is \((c,d) \in T^2\) satisfying that \(\textrm{dom}(b) = \textrm{三}_c(d)\).
- If \(\textrm{dom}(d) = 0\), then \(\textrm{dom}(s) := s\).
- If \(\textrm{dom}(d) \neq 0\), then \(\textrm{dom}(s) := $\omega\).
- Suppose that \(\textrm{dom}(b) = 0\).
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 that \(s = \textrm{三}_a(b)+s'\) for some \((a,b,s') \in T^2 \times (T \setminus \{0\})\).
- If \(t \lt a\), then \(\textrm{BP}(s,t) := s\).
- If \(a \le t\), then \(\textrm{BP}(s,t) := \textrm{BP}(s',t)\).
- Suppose that \(s = \textrm{三}_a(b)\) for some \((a,b) \in T^2\).
- If \(t \lt a\), then \(\textrm{BP}(s,t) := s\).
- Suppose that \(a \le t\).
- If \(b \lt s\), then \(\textrm{BP}(s,t) := s\).
- If \(s \le b\), then \(\textrm{BP}(s,t) := \textrm{BP}(b,t)\).
Fundamental sequence[]
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\).
- If \(b' \neq 0\), then \(s[t] := a+b'\).
- Suppose that \(s = \textrm{三}_a(b)\) for some \((a,b) \in T^2\).
- Suppose that \(\textrm{dom}(b) = 0\).
- If \(\textrm{dom}(a) \in \{0,$1\}\), then \(s[t] := t\).
- If \(\textrm{dom}(a) \notin \{0,$1\}\), then \(s[t] := \textrm{三}_{a[t]}(b)\).
- Suppose that \(\textrm{dom}(b) = $1\).
- If \(t = t[0]+$1\), then \(s[t] := s[t[0]]+s[$1]\).
- If \(t \neq t[0]+$1\), then \(s[t] := \textrm{三}_a(b[0])\).
- Suppose that \(\textrm{dom}(b) \notin \{0,$1\}\).
- If \(\textrm{dom}(b) \lt s\), then \(s[t] := \textrm{三}_a(b[t])\).
- If \(s \le \textrm{dom}(b)\), then there is \((c,d) \in T^2\) satisfying that \(\textrm{dom}(b) = \textrm{三}_c(d)\).
- Suppose that \(\textrm{dom}(d) = 0\).
- If \(t = 0\), then \(s[t] := \textrm{三}_a(b[\textrm{三}_{c[0]}(0)])\).
- If \(t = $i\) for some \(i \in (\mathbb{N} \setminus \{0\})\) and \(s[t[0]] = \textrm{三}_a(\Gamma)\) for some \(\Gamma \in T\), then \(s[t] := \textrm{三}_a(b[\textrm{三}_{c[0]}(\Gamma)])\).
- If neither of above, then \(s[t] := \textrm{三}_a(b[t])\).
- Suppose that \(\textrm{dom}(d) = \textrm{三}_e(0)\) for some \(e \in (T \setminus \{0\})\).
- If \(t = 0\), then \(s[t] := \textrm{三}_a(b[0])\).
- If \(t = $i\) for some \(i \in (\mathbb{N} \setminus \{0\})\) and \(s[t[0]] = \textrm{三}_a(\Gamma)\) for some \(\Gamma \in T\), then \(s[t] := \textrm{三}_a(b[\textrm{三}_{e[0]}(\textrm{BP}(\Gamma,e[0]))])\).
- If neither of above, then \(s[t] := \textrm{三}_a(b[t])\).
- Suppose that \(\textrm{dom}(d) = 0\).
- Suppose that \(\textrm{dom}(b) = 0\).
FGH[]
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 that \(m = 1\).
- If \(\textrm{dom}(s) = 0\), then \(f_s^m(n) := n+1\).
- If \(\textrm{dom}(s) = $1\), then \(f_s^m(n) := f_{s[0]}^n(n)\).
- If \(\textrm{dom}(s) \notin \{0,$1\}\), 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 function[]
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) := \textrm{三}_0(0)\).
- If \(n \neq 0\), then \(\Lambda(n) := \textrm{三}_{\Lambda(n-1)}(0)\).
Standard form[]
A subset \(OT \subset T\) is defined in the following recursive way:
- For any \(n \in \mathbb{N}\), \(\textrm{三}_0(\textrm{三}_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.