The Large Number Garden Number (Japanese: 巨大数庭園数) is the abbreviated name of the large number equal to \(f^{10}(10 \uparrow^{10} 10)\), where \(f\) is the function defined in First Order Theory beyond Higher Order Set Theory. [1][2] The term was coined by Googology Wiki user P進大好きbot.
This number can be considered to be the largest well-defined googologism which is not a salad number.
Definition
editTheory
editFirst, a language L is defined 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 ∈. Define ZFL as the set of L-formulae belonging to the axiom of ZF set theory. Here, the axiom schema of comprehension and replacement in ZFL are parametrized by all L-formulae, i.e. formulae which can include U. Define a formal language L 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 Θ to an explicit formalization of L using an explicit Gödel correspondence. I denoted by ZFCL the set of L-formulae belonging to the axiom of ZFC set theory, Here, the axiom schema of comprehension and replacement in ZFCL are parametrized by all L-formulae, i.e. formulae which can include the formalization of U, additional constant term symbols, additional function symbols, additional relation symbols, and Θ. Explicitly encode ordinals below ε0 and L-formulae into natural numbers in ZFL. Formalize the Henkin axiom "If there exists an x satisfying P, then Θ(n) satisfies P", for each variable term symbol x, each L-formula P with code n formalized into ZFCL by the repetition of successor operations,
Denote by ZFCHL the theory ZFCL augmented by the Henkin axiom schema. The new function symbol Θ plays a role of "a family of Henkin constants". Please do not confound the base theory ZFL and the formalized theory ZFCHL. Denote by U1 the L-formula "For any ordinal α, U(α)⊨ZFCHL". Under ZFL augmented by {U1}, U(α) forms a model of ZFCL, and hence forms an L-structure for any ordinal α. I denoted by UU(α) the interpretation of U at U(α). I denoted by U2 the L-formula "For any ordinal α and any β∈α, UU(α)(β)=U(β)", and by U3 the L-formula "For any ordinal α, there exists an ordinal β such that |U(α)|=Vβ and for any x∈Vβ and any y∈Vβ, x∈U(α)y is equivalent to x∈y", where Vβ denotes the von Neumann hierarchy. Define T as the set ZFL∪{U1,U2,U3} of L-formulae.
Embedding
editBy assigning to each atomic formula xi∈xj in ZFC set theory the L-formula (xi∈xj)∧(xj∈U(0)), the theory T can be regarded as an extension of ZFC set theory. In particular, the set N defined in ZFC set theory is interpreted at U(0) as a term of T, which coincides with the term N defined under ZFL because U(0) is a transitive model of ZFCL. Therefore a large number definable in ZFC set theory is also definable in T, and forms a term which is a large number. Moreover, since L 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 ZFC set theory can be interpreted at U(0) as a closed formula in T. Further, by assigning to each atomic formula xi∈xj in unsorted MK set theory the L-formula (xi∈xj)∧(xj∈U(0)), the theory T can be regarded as an extension of MK set theory. 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 ZFC set theory augmented by Grothendieck universe axiom, which appears in usual mathematics.
Large Number
editExplicitly define a surjective map: CNF: N→ε0; i↦CNF(i) using Cantor normal form. For an L-formula P, denote by IsDefinition(P) the L-formula "There exists an x such that P and for any i, (P)[i/x] implies i=x". Denote by Definable(m,i,P) the L-formula "i∈N, P is an L-formula, U(CNF(i))⊨IsDefinition(P), and U(CNF(i))⊨(P)[m/x]", where m in (P)[m/x] is regarded as a parameter in an explicit way. For an n∈N, define f(n) as the sum of m∈N satisfying i∈n, P∈n, and Definable(m,i,P), In this way, there is finally an uncomputable large function f: N→N; n↦f(n). From here, the Large Number Garden Number is \(f^{10}(10 \uparrow^{10} 10)\).
Sources
edit- ^ 高階集合論を超えた1階述語論理 by p進大好きbot (the Japanese first source of the definition)
- ^ First Order Theory beyond Higher Order Set Theory by P進大好きbot (the English summary of the first source)