>>2228546
>>2228655
Explicitly define a surjective map: CNF: Nε0; iCNF(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: NN; nf(n). From here, the Large Number Garden Number is f^10(101010).