*Please clean up this article. Thank you.*

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

### Theory

First, 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 ZF_{L} as the set of L-formulae belonging to the axiom of ZF set theory. Here, the axiom schema of comprehension and replacement in ZF_{L} 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 ZFC_{┌L┐} the set of ┌L┐-formulae belonging to the axiom of ZFC set theory, Here, the axiom schema of comprehension and replacement in ZFC_{┌L┐} 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 ZFC_{┌L┐} by the repetition of successor operations,

Denote by ZFC¯¯¯_{┌L┐}the theory ZFC_{┌L┐} 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 ZF_{L} and the formalized theory ZFC¯¯¯_{┌L┐}. I denoted by U1 the L-formula "For any ordinal α, U(α)⊨ZFC¯¯¯_{┌L┐}". Under ZF_{L} augmented by {U1}, U(α) forms a model of ZFC_{┌L┐}, and hence forms an ┌L┐-structure for any ordinal α. I denoted by ┌U┐^{U(α)} the interpretation of ┌U┐ at U(α). I denoted by U2 the L-formula "For any ordinal α and any β∈α, ┌U┐^{U(α)}(β)=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 von Neumann hierarchy. Define T as the set ZF_{L}∪{U1,U2,U3} of L-formulae.

### Embedding

By assigning to each atomic formula x_{i}∈x_{j} in ZFC set theory the L-formula (x_{i}∈x_{j})∧(x_{j}∈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 ZF_{L} because U(0) is a transitive model of ZFC_{┌L┐}. 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 x_{i}∈x_{j} in unsorted MK set theory the L-formula (x_{i}∈x_{j})∧(x_{j}∈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

Explicitly define a surjective map: CNF: N→ε_{0}; i↦CNF(i) using Cantor normal forms.
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

- ↑ 高階集合論を超えた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)