This is a summary of my Japanese blog post submitted to a Japanese googological event. I created a large function, which is expected to be much stronger than my system defined in an extension of \(\textrm{MK}\) set theory, which is expected to be much stronger than Rayo's function.
Abstract[]
In order to define an uncomputable large number, I need to specify the formally axiomised theory \(T\) in which I work. Here is a rough sketch of how I defined \(T\) and an uncomputable large number in \(T\).
- I defined a language \(L\) for \(T\) by adding a \(1\)-ary function symbol \(U\) to an explicit language of first order set theory.
- I formalised \(L\) and \(\textrm{ZFC}\) set theory in \(\textrm{ZF}\) set theory described by \(L\).
- I constructed explicit axioms on \(U\) by using the formalised \(\textrm{ZFC}\) set theory, and defined \(T\) as \(\textrm{ZF}\) set theory augmented by the axioms on \(U\).
- I embedded and higher order set theories together with explicit models into \(T\).
- I defined a truth predicate for set theoretic formulae as the satisfaction relation at the models in \(T\), and use it to define an uncomputable function \(f\) diagonalising set theories in \(T\).
I note that the phenomenon that set theories can be embedded into \(T\) with explicit models is similar to the one that \(\textrm{PA}\) can be embedded into \(T\) with the standard model \(\mathbb{N}\). As many uncomputable functions in \(\textrm{ZFC}\) set theory go beyond functions which in some sense diagonalise \(\textrm{PA}\), \(f\) is expected to go beyond functions which in some sense diagonalise set theories.
Theory[]
In this section, I explain how I defined the theory \(T\), in which I worked in order to define an uncomputable large number.
Construction[]
I defined the language \(L\) by adding a \(1\)-ary function symbol \(U\) to the language of first order set theory with countably many variable term symbols and the set-membership relation symbol \(\in\). I denoted by \(\textrm{ZF}_L\) the set of \(L\)-formulae belonging to the axiom of \(\textrm{ZF}\) set theory. Here, the axiom schema of comprehension and replacement in \(\textrm{ZF}_L\) are parametrised by all \(L\)-formulae, i.e. formulae which can include \(U\).
To begin with, I worked in \(\textrm{ZF}_L\). I defined a formal language \(\ulcorner L \urcorner\) of first order logic by adding countably many constant term symbols, countably many function symbols, countably many relation symbols, and a new \(1\)-ary function symbol \(\ulcorner \Theta \urcorner\) to an explicit formalisation of \(L\) using an explicit Goedel correspondence. I denoted by \(\textrm{ZFC}_{\ulcorner L \urcorner}\) the set of \(\ulcorner L \urcorner\)-formulae belonging to the axiom of \(\textrm{ZFC}\) set theory, Here, the axiom schema of comprehension and replacement in \(\textrm{ZFC}_{\ulcorner L \urcorner}\) are parametrised by all \(\ulcorner L \urcorner\)-formulae, i.e. formulae which can include the formalisation of \(U\), additional constant term symbols, additional function symbols, additional relation symbols, and \(\ulcorner \Theta \urcorner\).
I note that I did not have to add constant term symbols, function symbols other than \(\ulcorner \Theta \urcorner\), or relation symbols in the construction of \(T\). I just prepared them in order to ensure that set theories can be embedded into \(T\) with specific models even if their languages have symbols other than standard minimal ones. The definition of the resulting uncomputable large number did not require them.
I explicitly encoded ordinals below \(\varepsilon_0\) and \(\ulcorner L \urcorner\)-formulae into natural numbers in \(\textrm{ZF}_L\). I formalised the Henkin axiom "If there exists an \(x\) satisfying \(P\), then \(\ulcorner \Theta \urcorner(n)\) satisfies \(P\)", for each variable term symbol \(x\), each \(\ulcorner L \urcorner\)-formula \(P\) with code \(n\) formalised into \(\textrm{ZFC}_{\ulcorner L \urcorner}\) by the repetition of successor operations,
I denoted by \(\overline{\textrm{ZFC}}_{\ulcorner L \urcorner}\) the theory \(\textrm{ZFC}_{\ulcorner L \urcorner}\) augmented by the Henkin axiom schema. Now you understand that the new function symbol \(\ulcorner \Theta \urcorner\) plays a role of "a family of Henkin constants".
I recall that I am explaining how to define \(T\). I am still working in \(\textrm{ZF}_L\). Please do not confound the base theory \(\textrm{ZF}_L\) and the formalised theory \(\overline{\textrm{ZFC}}_{\ulcorner L \urcorner}\). I denoted by \(\textrm{U}1\) the \(L\)-formula "For any ordinal \(\alpha\), \(U(\alpha) \models \overline{\textrm{ZFC}}_{\ulcorner L \urcorner}\)".
Under \(\textrm{ZF}_L\) augmented by \(\{\textrm{U}1\}\), \(U(\alpha)\) forms a model of \(\textrm{ZFC}_{\ulcorner L \urcorner}\), and hence forms an \(\ulcorner L \urcorner\)-structure for any ordinal \(\alpha\). I denoted by \(\ulcorner U \urcorner^{U(\alpha)}\) the interpretation of \(\ulcorner U \urcorner\) at \(U(\alpha)\). I denoted by \(\textrm{U}2\) the \(L\)-formula "For any ordinal \(\alpha\) and any \(\beta \in \alpha\), \(\ulcorner U \urcorner^{U(\alpha)}(\beta) = U(\beta)\)", and by \(\textrm{U}3\) the \(L\)-formula "For any ordinal \(\alpha\), there exists an ordinal \(\beta\) such that \(|U(\alpha)| = V_{\beta}\) and for any \(x \in V_{\beta}\) and any \(y \in V_{\beta}\), \(x \ulcorner \in \urcorner^{U(\alpha)} y\) is equivalent to \(x \in y\)", where \(V_{\beta}\) denotes von Neumann hierarchy.
I defined \(T\) as the set \(\textrm{ZF}_L \cup \{\textrm{U}1,\textrm{U}2,\textrm{U}3\}\) of \(L\)-formulae.
Embedding[]
Although the theory \(T\) can be regarded as \(\textrm{ZF}\) set theory by \(\textrm{ZF}_L \subset T\), I defined another way to embed set theory into \(T\).
By assigning to each atomic formula \(x_i \in x_j\) in \(\textrm{ZFC}\) set theory the \(L\)-formula \((x_i \in x_j) \land (x_j \in U(0))\), the theory \(T\) can be regarded as an extension of \(\textrm{ZFC}\) set theory. In particular, the set \(\mathbb{N}\) defined in \(\textrm{ZFC}\) set theory is interpreted at \(U(0)\) as a term of \(T\), which coincides with the term \(\mathbb{N}\) defined under \(\textrm{ZF}_L\) because \(U(0)\) is a transitive model of \(\textrm{ZFC}_{\ulcorner L \urcorner}\). Therefore a large number definable in \(\textrm{ZFC}\) set theory is also definable in \(T\), and forms a term which is a large number. Moreover, since \(\ulcorner L \urcorner\) admits countably infinitely many constant term symbols, function symbols, and relation symbols, even a closed formula in a theory given by adding countably many constant term symbols, function symbols, and relation symbols to \(\textrm{ZFC}\) set theory can be interpreted at \(U(0)\) as a closed formula in \(T\).
Further, by assigning to each atomic formula \(x_i \in x_j\) in unsorted \(\textrm{MK}\) set theory the \(L\)-formula \((x_i \in x_j) \land (x_j \subset U(0))\), the theory \(T\) can be regarded as an extension of \(\textrm{MK}\) set theory. Furthermore, I defined an explicit way to embed the extension "\(\textrm{MK}_{+}\) set theory" of \(\textrm{MK}\) set theory defined here into \(T\).
Roughly speaking, \(U(0)\) formally plays a role of the universe of the first order set theory, the power set of \(U(0)\) formally plays a role of the universe of the second order set theory and the first order class theory, and its power set formally plays a role of the universe of the third order set theory. Since all of them are included in \(U(1)\), \(U\) formally plays a role of a strictly increasing sequence of the universes of higher order set theories. I note that the existence of such a strictly increasing sequence can be constructed in \(\textrm{ZFC}\) set theory augmented by Grothendieck universe axiom, which appears in usual mathematics.
The most important point is not the existence of the hierarchy of the universes, but \(T\) has much stronger definability than usual set theories because the images of \(U\) has an interpretation of Henkin extension on each \(\exists\)-formula as the universe of \(\textrm{MK}_{+}\) does. Since we often construct truth predicates in uncomputable googology, what we should care about is not the provalibity but the definability and the the presentability.
For example, the fact that I used \(\textrm{ZF}_L\) first is not essential, and I could use a weaker set theory such as \(\textrm{BS}\) set theory or a stronger set theory such as \(\textrm{ZFC}\) set theory augmented by rank-into-rank cardinal axiom without changing the size of the resulting uncomputable large number. It is good to remember that the definition of Little Bigeddon required the axiom \(V = \textrm{HOD}\) not for the provability but for the definability of a well-ordering on the universe \(V\) of \(\textrm{ZFC}\) set theory. I note that a well-ordering on the universe \(V\) of the first order set theory, which is interpreted as the domain of \(U(0)\), is definable in the theory \(T\).
Large Number[]
I explain the definition of an uncomputable large number in \(T\).
Large Function[]
I explicitly defined a surjective map \begin{eqnarray*} \textrm{CNF} \colon \mathbb{N} & \to & \varepsilon_0 \\ i & \mapsto & \textrm{CNF}(i) \end{eqnarray*} using Cantor normal forms. For an \(\ulcorner L \urcorner\)-formula \(P\), I denoted by \(\textrm{IsDefinition}(P)\) the \(\ulcorner L \urcorner\)-formula "There exists an \(x\) such that \(P\) and for any \(i\), \((P)[i/x]\) implies \(i = x\)". I denoted by \(\textrm{Definable}(m,i,P)\) the \(L\)-formula "\(i \in \mathbb{N}\), \(P\) is an \(\ulcorner L \urcorner\)-formula, \(U(\textrm{CNF}(i)) \models \textrm{IsDefinition}(P)\), and \(U(\textrm{CNF}(i)) \models (P)[m/x]\)", where \(m\) in \((P)[m/x]\) is regarded as a parameter in an explicit way.
For an \(n \in \mathbb{N}\), I denoted by \(f(n)\) the sum of \(m \in \mathbb{N}\) satisfying \(i \in n\), \(P \in n\), and \(\textrm{Definable}(m,i,P)\), In this way, I obtained an uncomputable large function \begin{eqnarray*} f \colon \mathbb{N} & \to & \mathbb{N} \\ n & \mapsto & f(n). \end{eqnarray*} Since the theory \(T\) includes the second order \(\textrm{ZFC}\) set theory, \(f\) is expected to be significantly stronger than \(\textrm{Rayo}\)(n)
Definition[]
I submitted the uncomputable large number \(f^{10}(10 \uparrow^{10} 10)\) defined in \(T\) to the event. Since the theory \(T\) includes \(\textrm{MK}_{+}\) set theory, this number is expected to be significantly greater than the corresponding uncomputable large number given by diagonalising \(\textrm{MK}_{+}\) set theory.