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

**by the repetition of successor operations,**

_{L}Denote by ZFCH** _{L}** the theory ZFC

**augmented by the Henkin axiom schema. The new function symbol**

_{L}**Θ**plays a role of "a family of Henkin constants". Please do not confound the base theory ZF

_{L}and the formalized theory ZFCH

_{L}. Denote by U1 the L-formula "For any ordinal α, U(α)⊨ZFCH

_{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 the 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 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

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

**Fish numbers:** Fish number 1 · Fish number 2 · Fish number 3 · Fish number 4 · Fish number 5 · Fish number 6 · Fish number 7**Mapping functions:** S map · SS map · S(n) map · M(n) map · M(m,n) map**By Aeton:** Okojo numbers · N-growing hierarchy**By BashicuHyudora:** Primitive sequence number · Pair sequence number · Bashicu matrix system**By Kanrokoti:** KumaKuma ψ function**By 巨大数大好きbot:** Flan numbers**By Jason:** Irrational arrow notation · δOCF · δφ · ε function**By mrna:** 段階配列表記 · 降下段階配列表記 · 多変数段階配列表記 · SSAN · S-σ**By Nayuta Ito:** N primitive**By p進大好きbot:** **Large Number Garden Number****By Yukito:** Hyper primitive sequence system · Y sequence · YY sequence · Y function**Indian counting system:** Lakh · Crore · Tallakshana · Uppala · Dvajagravati · Paduma · Mahakathana · Asankhyeya · Dvajagranisamani · Vahanaprajnapti · Inga · Kuruta · Sarvanikshepa · Agrasara · Uttaraparamanurajahpravesa · Avatamsaka Sutra · Nirabhilapya nirabhilapya parivarta**Chinese, Japanese and Korean counting system:** Wan · Yi · Zhao · Jing · Gai · Zi · Rang · Gou · Jian · Zheng · Zai · Ji · Gougasha · Asougi · Nayuta · Fukashigi · Muryoutaisuu**Other:** Taro's multivariable Ackermann function · TR function · Arai's \(\psi\) · *Sushi Kokuu Hen*