Large Numbers

First page . . . Back to page 8 . . . Forward to page 10 . . . Last page (page 11)

Computation by Formal Logic and Set Theory

Finally we'll spend some time on the third popular way to formulate systems that express large numbers. This is closely related to formal logic (ostensibly still part of the school of philosophy) and its use to establish the foundations of mathematics. This was the approach of Frege, Russell and Whitehead, and Gödel.

It famously led to the downfall of the ambitions of mathematical "completeness", but that did not affect our ability to use it to define large numbers. It is yet more abstract than the functiuonal approach of Church's lambda calculus, and more powerful because now when we assert things, they actualy do get satisfied (or not) "in parallel". A combination of a dozen or so assertions, suitably formulated, can instantly create an infinite set containing all the results of a new operator like tetration.

Set-Theoretic Construction of Arithmetic

As things will be getting somewhat more abstract, it helps to review some of the principles of the foundations of mathematics.

As in any of the methods used so far, asserting the existence of numbers, including googol, Graham's number or the (unknown but nevertheless well-defined) Lin-Rado busy beaver function of 100 "BB(100)", requires a formal language with symbols that are interpreted in a well-defined way.

Agustín Rayo's number, which we'll get to eventually, appears to use a popular and well-studied "structure": a set of objects similar to the von Neumann universe; with finitary operations and relations common in set theory: negation (~), conjuncation (∧), set-membership (∈), equality (=), and existential quantification (∃). Other well-known operations can be defined in terms of these, possibly by implicit definitions, examples of which follow.

The natural numbers can be thought of abstractly as any countably infinite set with a single member analogous to zero and a binary relation (called successor) that uniquely sets an ordering.

Peano Arithmetic

In the late 1900's, Giuseppe Peano presented the Peano axioms which can be used to formalise arithmetic. The original Peano axioms comprise:

Concerning the zero element 0:

0 is a natural number.

Concerning the equality relation =:

For every natural number x, x=x. (Equality is a reflexive relation.)
For any two natural numbers x and y, if x=y then y=x (Equality is a symmetric relation.)
For any three natural numbers *x, *y, and z: if x=y and y=z, then x=z (Equality is a transitive relation.)
For any two things a and b, if a is a natural number and a=b, than b is a natural number (Natural numbers are closed under the equality relation.)

Concerning the successor function S:

For every natural number n, there exists a natural number m such that m=S(N).
For any two natural numbers m and n, m=n if and only if S(M)=S(N) (the successor function is an injective function.)
For every natural number n, S(n) is false: there is no natural number whose successor is 0 (and the successor function is not a bijection.)

The Axiom of Induction:

If K is a set such that [0 is an element of K] and [for any natural number n, if n is an element of K, then S(n) is an element of K], then every natural number is an element of K.

In this last axiom, "membership in in the set K" can equivalently be expressed as "satisfying a unitary predicate φ", that is "x is an element of K" can be expressed instead as "φ(x) is true" with the understanding that for any x, φ(x) is either true or false.

This last axiom is critical because it ensures that all of the natural numbers are connected by the successor relation. Without it, a set like the following:

{ 0, 1, 2, 3, 4, 5, 6, 7, .... , A, B, C }

would saitisfy the first eight axioms if S(x) were defined such that:

S(0)=1; S(1)=2; S(2)=3; S(3)=4; ...
and S(A)=B; S(B)=C; S(C)=A.

the three elements A, B, and C form a cycle that is "disjoint" from the other numbers starting with 0. If you start within this cycle, S(x) is always defined and unique, as it is if you start anywhere in the normal numbers, but there is no way to get from one to the other or back through repeated application of the successor function. This type of situation is eliminated by including the Axiom of Induction.

The induction axiom is second-order, leading to some problems such as Gödel's incompleteness theorems, so it is sometimes replaced with an "axiom schema" which adds a specific induction axiom for every specific predicate.

Regardless of how induction is handled, the Peano axioms can then be used along with suitable definitions of addition and multiplication, and the total ordering that comes from whichever type of induction axiom(s) were used, to develop a theory of arithmetic in which it is possible to prove such things as the fundamental theorem of arithmetic (that every natural number except for 0 and S(0) has a unique factorisation into prime factors; for outlines, see [58] or [63]); a fairly thorough discussion of this sort of thing in [41].

The von Neumann Construction

As stated so far, we imagined an element "0", and elements "1", "2", "3", etc. without establishing our right to add these symbols to the basic symbols of set theory. Set theory itself includes only the null set ∅ = {} and the ability to construct or define sets that include other sets. This turns out to be enough, if we define the first natural number 0 as being the null set ∅, and the successor function S(a) as a U {a}, the union of a with the set containing a as its only element. The succession of natural numbers becomes:

0 = ∅ = {} ;
1 = ∅ U {∅} = {∅} ;
2 = {∅} U {{∅}} = {∅, {∅}} ;
3 = {∅, {∅}} U {{∅, {∅}}} = {∅, {∅}, {∅, {∅}}} ;
4 = {∅, {∅}, {∅, {∅}}} U {{∅, {∅}, {∅, {∅}}}} = {∅, {∅}, {∅, {∅}}, {∅, {∅}, {∅, {∅}}}} ;
etc.

and the natural numbers are

ℕ = {0, 1, 2, 3, 4, ...}

Each natural number n is represented as a set containing n elements, where those n elements are all of the natural numbers less than n. This also gives us another operator "for free": If a and b are natural numbers under von Neumann's construction, the subset relation can be used as the comparison operation "less than":

a < b ↔ a ∈ b

"a is less than b" if and only if a is a subset of b.

It is also useful to have a set of all natural numbers so that we can use "a ∈ ℕ" to assert that a is a natural number (and not some other thing, like an ordered pair, which will be needed later).

There exists a set ℕ such that, for all n
   n is an element of ℕ if and only if
      n is the null set (there exists no a ∈ n), or
      there exists a p such that
         p is an element of ℕ, and
         p is an element of n, and
            there does not exist a q such that
               p is an element of q, and
               q is an element of n

More Relations and Operations

We have "and" (∧) and "not" (~); from these we get "or" in the standard way. If p and q are predicates, then "p∨q" can be expressed by "~((~p)∧(~q))"; or more formally:

p∨q := ~((~p)∧(~q))

If p and q are predicates, then we can define the conditional predicate "if p then q" by exclusing the one condition in which it would be false (q true with p false):

p→q := ~((~q)∧p)

Similarly the biconditional "p if and only if q" is defined:

*p↔q := (p∧q)∨((~p)∧(~q))

The universal quantifier "∀" can be defined in terms of existence and negation. If p(x) is a predicate that takes a single argument, saying "p(x) is true for all x" is equivalent to saying "there is no y for which p(y) is false":

∀x(p(x)) := ~(∃y(~(p(y))))

If a and b are sets, the their union c=a∪b can be defined, and its existence asserted, with:

∃ C ( ∀d ( (d∈C) ↔ (d∈A ∨ d∈B ) ) )

"There exists (a set) C such that for all d, the statement 'd is an element of C' is true if and only if d is an element of A or of B."

We are given no symbol for the null set, but we can define it and assert its existence:

∃ ∅ ( ∀ a ( ~(a∈∅) ) )

"There exists (a set) ∅ such that for all a, a is not an element of ∅."

Forming Predicates

By whichever specific axioms and means, the methods of set theory and formal logic are used to define more predicates, functions, and relations on the natural numbers. We've already seen a few that are basic to set theory: the equality and element relations, the successor function, the predicate φ indicating membership in a certain set. These naturally give us vary besic number-theory operations of equality, the successor function, and the ordering/comparison operator.

Peano arithmetic proceeds to define addition and multiplication with all the familiar properties such as associativity and commutativity; similar methods can be used to construct more elaborate and faster-growing functions and operators like tetration and the Ackermann function. The existence of a number can then be expressed as a "predicate", e.g.:

τ(x) := x = S(S(0)) + S(S(0))

Which roughly states, "τ(x) is a predicate equivalent to the assertion that x=2+2". It is true only for one value of x, namely S(S(S(S(0)))) which is 4. If we had defined an Ackermann function, we could construct a predicate equivalent to "x=A(27,143)" and that predicate would "define" a very large number.

Not So Fast!

As I mentioned above ("by whichever specific axioms and means..."), there are mutiple approaches to this type of work. The approach I just outlined is probably more familiar with readers, due to the relative prominence of Peano arithmetic. It has been used in many set-theory constructions of mathematics, most notoriously including Whitehead & Russell's efforts which were ultimately refuted by Gödel; all memorialised in Gödel, Escher, Bach [41] and other popular works.

Peano arithmetic, in the forms that use the induction axiom of the second order (i.e. the single axiom covering all possible predicates φ) might be avoided for various reasons, including Gödelian incompleteness or because they simply aren't needed for constructing the desired result.

Rayo's Calculus

To really surmount the Busy Beaver function, we'll go to the winner of the rather colourfully-advertised Big Number Duel at MIT in 2007. It was described by Agustín Rayo and has been called "Rayo's number" ever since.

Formulas

The coded formula is constrained to obey a number of conditions that force the formula to be a combination of five formal logic operations:

a ∈ b          (set-membership)
a = b          (equality)
~ a             (negation)
a ∧ b          (conjunction)
∃ a : b       (satisfiability)

Before we get to Rayo's construction, which is about as intricate and elaborate as the incompleteness theorems of Gödel, Turing, or Church, we will first show how to use this limited symbol set to express numbers in a traditional "imperative computation" sort of way.

Direct Declaration of the Existence of a Number

When we get to Rayo's number there will be the concept of "being able to name a number m in a certain number n of symbols".

All numbers are nameable: at the very least, one can assert that the number is equal to one of the von Neumann cardinals like 1={∅}; this assertion is done by the rather awkward construction:

1 exists ↔ (
   (~∃x₃: (x₃∈x₂) ) ∧    "x₂={}"
   x₂∈x₁ ∧                   "x₂<x₁"
   (~∃x₃: (x₃∈x₁ ∧ (~x₃=x₂)) ) "there is no x₃ such that x₃<x₂ and x₃<x₁"
)

The only way for that to be true is for x₁ to have the value "{∅}"=1: the first part is a sub-assertion forcing x₂ to be "{}"=0 ; the next part says that x₁ is bigger than x₂ (so must be 1 or higher); and the third part says that x₁ is not bigger than 1.

(I'll note here that it must seem unusual to some readers that it takes so many symbols to assert the fact that the number 1 exists. But far more symbols can be used, as seen in Whitehead and Russell's programme of metamathematics "Principia Mathematica".)

The fact that all numbers are namable this way is of little use; we're trying to get a specific, well-defined large number. We'll use a Rayo-like approach, and define a predicate that says "a certain number is nameable in an assertion of this type, with a limited number of symbols":

ST-namable-in(m, n) ↔
   ∃Φ(x₁): {
      Φ has fewer than n symbols ∧
      ∃s: s = Assign(m, x₁) ∧
      (∀t: Sat([Φ(x₁)],t) → t = Assign(m, x₁))
   )

Let's evauate the ST-namable-in() function for various values of m and n. That unwieldy expression asserting the existence of 1 has 36 symbols (10 for the "(~∃x₃(x₃∈x₂))" part that means "x₂={}", 23 for the longer part, and 3 more for the (, ∧, ) that joins those together). So we can say that:

ST-namable-in(1, 35) = false
ST-namable-in(1, 36) = false
ST-namable-in(1, 37) = true
ST-namable-in(1, 38) = true

(It turns true at 37 because the definition of ST-namable-in(m, n) requires that we can do it in "fewer than n symbols").

We can say the same thing in a different way by changing the first argument:

ST-namable-in(0, 37) = true
ST-namable-in(1, 37) = true
ST-namable-in(2, 37) = false
ST-namable-in(3, 37) = false

Using the type of "existence of n" formula just shown, where we invoke only the existence of zero and the successor function, is very inefficient. With each successive assertion of "c is less than b but not enough that another number d can get inbetween" we need more subexpressions than we did the last time. To assert the existence of the number n requires (9n²+43n+20)/2 symbols. If a googol symbols were allowed, the largest number we could assert would be about 4.714×10⁴⁹:

ST-namable-in(4.714×10⁴⁹, 10¹⁰⁰) = true
ST-namable-in(4.715×10⁴⁹, 10¹⁰⁰) = false (for now)

But the subset of set theory and formal logic that Agustín Rayo chose can do more than just string together a bunch of a∈b relations. It is, in fact "Gödel-complete" in the sense that an entire Peano arithmetic can be built upon it.

Doing Maths in First-Order-Logic and Set Theory

(I might move the next several paragraphs up to an earlier place titled "doing arithmetic in set theory and formal logic". As we get near the end of the section, the parts about placing functions in a fast growing hierarchy will need to be summarised in the earlier section, and repeated/expanded here.)

Since we're using set theory, functions and relations can be expressed as (infinite) sets, and set-membership asserts a relation. For example, the set P (for "Plus") would be the set of all valid addition relations, consisting of ordered triples; and it might start out: Plus = { (0,0,0), (0,1,1), (1,0,1), (0,2,2), (1,1,2), (2,0,2), (0,3,3), ...} where each of those digits is a von Neumann cardinal like 2={{},{{}}}. We don't have to spend an infinite number of symbols to define P expicitly, we could "just" say:

There exists a set P such that, for all a
   a is an element of P if and only if
      a is an ordered-triple such that either
         a consists of three zeros (0,0,0), or
         there is another b that is also an element of P where
            b₃+1=a₃, and
               b₁+1=a₁ ∧ b₂=a₂, or
               b₁=a₁ ∧ b₂+1=a₂

It's unwieldy, but it works (and again, it's very close to how addition is built up in the Gödel construction for demonstrating incompleteness.) We used things like "for all" (∀) and "if and only if" (↔) that are not in the allowed 7 symbols, but that's okay because these can be defined in terms of the others. (For example, ∀x:P(x) is equivalent to ~(∃x:~P(x)} ).

I've skipped over how we make ordered triples: we have parentheses but have no comma "," to construct ordered-tuple literals like this; instead "(*a,b,c)" is shorthand for a set like {{*a},{a,{b}},{a,{b},{{c}}}}. Things like "the second item of b" have to be expressed in terms of more temporary variables.

With such a definition of P containing all triples of valid addition relations, a statement like "a+b=c" is expressed as

a+b=c ⋛ {a,{b,{c}}}∈P

This also cannot be done directly, because our language has no { } symbols: we cannot construct set literals. Instead we must do something like:

there exists a t such that
   a is the first element of t ∧
      a is a natural number ∧
   b is the second element of t ∧
      b is a natural number ∧
   c is the third element of t ∧
      c is a natural number ∧
   t ∈ P

Once addition is defined, a similar set M (for Multiplication) can be defined and a similar iterative definition used to assert that all ordered triples in M consist of items that can be related to other elements of M by the successor relationship combined with addition (i.e. membership in P).

If you look back through these pages, you can see that all of the fast-growing functions have been defined this way: from tetration to the Ackermann function to chained arrow notation to the Bowers Extended Array notation, everything is defined by subtracting 1 from one number and applying an operation (either the one being defined, or a previously-defined operation) to another number.

So, this gives us a more efficient way to prove numbers are ST-namable in a googol symbols. Suppose that the definition of P outlined above took 1000 symbols, and we didn't define M or any other "operators". Given the primtive (as above) assertion that "2 exists" we can combine it with the definition and application of addition as follows:

(there exists an x₁ such that (x₁ is the number 2) ) ∧
(there exists a P such that for all a ... (define P as above)) ∧
(there exists an x₂ such that x₁+x₁=x₂ ) ∧
(there exists an x₃ such that x₂+x₂=x₃ ) ∧
(there exists an x₄ such that x₃+x₃=x₄ ) ∧
...

We are iterating addition in the same way that our previous approach iterated the succssor function. If the definitions needed to set up ordered triples and P take 1000 symbols, and each "a+b=c" takes another 1000 symbols, then the number 2ⁿ could be expressed in a bit over 1000n+1000 symbols. With a googol symbols, we can now assert the existence of numbers as high as 2^{(googol/1000)} ≈ 10^{3.01×10⁹⁶}. We've made it to class 3! Woo hoo!!

Of course, we continue, using all our old tricks to define ever-faster-growing functions with more and more arguments. We could just methodically follow one of the well-defined fast growing hierarchies, and every time we add a new iteration paradigm we use up 1000 or 10,000 or even a million symbols. It's easy to see we can get through all the stuff we've already discussed on these pages (except the uncomputable Busy Beaver function) without putting a dent into our budget of a googol symbols.

But we don't have to figure out what techniques to use to define an optimum fast growing hierarchy: "ST-namable-in()" is defined as the biggest thing anyone could accomplish with a given number of symbols (or fewer). It is effectively the "busy beaver function" of the computation-schema built on first-order set theory.

How do we coerce our propositional calculus to do the magic for us and compute this result instantly? One way to do it would be to apply the infinite parallelism of set theory: define a set that contains all possible predicates in the Rayo 7-symbol calculus, linked to variables whose values are sets containing all things (including any natural numbers) that satisfy those predicates. We can't do that directly, but we can employ the completeness property of our formal system to get the system to compute the results of its own predicates, using the methods of Gödel-numbering.

Truth and Uniqueness

One issue that must be addressed is how to determine (given a definition a number) that it actually does define a single specific number. Suppose we formulated the following statement:

Φ(x) := x is greater than 10^10¹⁰⁰ and is a Mersenne prime.

Does this define a single number x? We don't know. The largest Mersenne prime is less than 10^10¹⁰ and probably will be for some time. There might or might not be a finite number of Mersenne primes (that's an unproven conjecture), but if there are a finite number of them there is a largest one, and if that largest one were the only one greater than 10^10¹⁰⁰, then Φ(x) would be true for only one x. The trouble is that, given the difficulty of proving the conjecture, it might take an infinite amount of computation to confirm that there is only one such value.

This issue is addressed in the Busy Beaver function by assuring that only halting Turing machines are allowed to be considered as candidates: the number x must be computed in a finite number of steps and the machine must then stop and not consider any higher values for x.

In formal logic, we need the formula Φ(x) to be true for some x, and we also need the system to somehow verify this, through a finite number of deductive steps.

I'm not going to try to explain all the concepts and methods fully, but several articles in the Stanford Encyclopedia of Philosophy should be helpful:

The basic terminology and smbols of formal logic are described in the Classical Logic article.

Tarski's Truth Definitions discusses the task of expressing "truth predicate" True(x) in terms of a formula Φ(x). It also discusses "variable assignments that satisfy formulas". The entries on model theory and on quantifiers and quantification discuss these ideas more generally, and the latter links them to the definition of truth.

Agustín Rayo refers to "second order" and plural quantification in the definition of Sat([Φ],s).

Working Towards Rayo's Number

I still don't understand quite how this works, though most of the needed explanation is in the links I gave at the end of the previous section, and in the further readings list at the bottom of the Big Number Duel page at MIT. My general impression is that most of Agustín Rayo's definition is explained by the need to use methods of model theory to formalise the definition of a "namable number" and ensure that the (second-order) system determines the truth of the existence and uniqueness of any number that is so namable, through arithmetisation of the first-order formulas, and variable-assignments, formulas and satisfiability predicates in the second-order system. I will describe the building blocks of Rayo's number as nearly as I can.

Variable Assignments

A variable assignment isn't just a single number or set, but an infinite set of objects. Since we're operating within set theory, these "objects" could be finite numbers using the von Neumann Construction, which are sets with a finite number of elements each of which are sets; but they could also be sets that are not in ℕ. With a suitable construction like that of von Neumann, we could encapsulate the entire state of a Turing machine at any particilar step: its state machine, current state, and tape contents (all of which can be expressed in a finite number of bits). Then the objects in the variable assignment could represent successive steps in the execution of a Turing machine. Just as in the definition of the P set containing all valid addition-triples, we can define the set's contents by induction.

This isn't quite what Rayo's construction does, but it's conceptually similar.

Gödel-Coding

Rayo's number relies on Gödel-numbering to relate a formula to a variable assignment that is linked with it through the R() relation. Gödel-coding is simply turning a formula into a number. For example, the formula 'x₁∈x₂' has three symbols; recall that there are seven pre-defined symbols, so the variables start with the 8^th prime number. Rayo's Gödel-numbering might use the assignments:

'∈' = 2, '=' = 3, '(' = 5, ')' = 7, '~' = 11, '∧' = 13, '∃' = 17 ; x₁ = 19, x₂ = 23, x₃ = 29, ...

And so the Gödel-number of 'x₁∈x₂' would be

2¹⁹3²5²¹

where the exponents {19, 2, 21} correspond to the three symbols {x₁, ∈, x₂}.

Agustín Rayo represents the Gödel number of a formula by putting the formula inside square brackets:

[x₁∈x₂] = 2¹⁹3²5²¹

Assignment

Variable assignments are so-called because they are the result of taking a set of expressions with a free variable and replacing that free variable with something that has a specific definition. (This is type of thing is also used in Gödel's incompleteness proofs)

Assign(m, x₁) = s ↔ s is a variable assignment in which every x₁ is changed to m

Rayo's R() Relation

The definition of Sat([Φ],s) invokes a mysterious relation R(), which always appears with two arguments; the first is a Gödel number of a formula represented as a Greek letter, like '[ψ]', and the second is a variable-assignment represented as a letter s or t.

This relation is a temporary definition, and it is a relation forming a bijection between Gödel-coded formulae and assertions in Rayo's 7-symbol subset of first-order logic; as a bijection is a set of ordered pairs of items, R() encapsulates all such pairs.

R() has to be infinite set of ordered pairs, but let's give a finite example and call it r().

r() := { ( 2¹⁹3²5²¹, ({}, {{},{{}}}, {{},{{}}}) ), ( 2²¹3³5²³, ({}, {{},{{}}}, {{},{{}}}) ) }

r(α, b) ↔ ( (α = 'x_i=x_j') ∧ (b_i = b_j) ) ∧
( (α = 'x_i∈x_j') ∧ (b_i ∈ b_j) )

The first ordered-pair in r() has '2¹⁹3²5²¹', which is the Gödel-number of the formula 'x₁∈x₂', and it has '({}, {{},{{}}}, {{},{{}}})', an ordered-triple containing the von Neumann numerals (0, 2, 2). Notice that the first number (0) is less than the second number (2). The definition of r(α, b) is satisfied here, because if x₁ and x₂ are taken to be the first and second elements of the ordered triple (0, 2, 2), then x₁ = 0 = {} and x₂ = 2 = {{},{{}}}, and indeed x₁∈x₂ because {} is a subset of {{},{{}}}.

Two-Way Existence-Equivalence Assertion

The definition of Sat([Φ],s) and of Rayo-namability both use a construct like this:

(∃ a : P(a)) ∧ (∀ b : Q(b) → P(b))

where P() and Q() are predicates. It states that there is at least one thing with the property P(), and all things with the property Q() also have the property P().

Since predicates can also be thought of as set-membership, the existence-equivalence assertion can also be expressed:

(∃ a : a∈P) ∧ (∀ b : b∈Q → b∈P)

where P and Q are sets. It states that P is a non-empty set and that Q is a subset of P.

Definition of Sat()

Where φ is a formula and [φ] is its Gödel number, use "Sat([φ],s)" to abbreviate the following second-order formula (where the second-order quantifier is understood plurally):

Sat([φ],s) :=
∀ R {
   {for any (coded) formula [ψ] and any variable assignment t
      (R([ψ],t) ↔
         ([ψ] = 'x_i ∈ x_j' ∧ t(x_i) ∈ t(x_j)) ∨
         ([ψ] = 'x_i = x_j' ∧ t(x_i) = t(x_j)) ∨
         ([ψ] = '(~θ)' ∧ ~R([θ],t)) ∨
         ([ψ] = '(θ∧ξ)' ∧ R([θ],t) ∧ R([ξ],t)) ∨
         ([ψ] = '∃x_i (θ)' and, for some an x_i-variant t' of t, R([θ],t'))
      )
   } →
R([φ],s) }

Rayo-nameability

The definition of Agustín Rayo's number depends on being able to find a number that can be "computed" by a sequence of steps represented by the variable-assignment according to a formula in first-order set theory, as verified by a Godel-type emulation asserted by putting the formula and the variable-assignment together in a Sat() function. The ability to do this for a number is called "Rayo-nameability".

m is Rayo-namable if and only if:
   there is a formula Φ(x₁) in the language of first-order set-theory (as presented in the definition of 'Sat') with x₁ as its only free variable such that:
      (a.) there is a variable assignment s assigning m to x₁ such that Sat([Φ(x₁)],s), and
      (b) for any variable assignment t, if Sat([Φ(x₁)],t), then t assigns m to x₁.

Using more notation, this would be:

Rayo-namable(m) ↔
   ∃Φ(x₁): {
      ∃s: s = Assign(m, x₁) ∧
      (∀t: Sat([Φ(x₁)],t) → t = Assign(m, x₁))
   )

But the fact that all numbers are namable this way is of little use; we're trying to get a specific, well-defined large number. So Rayo expresses "the largest number that satisfies an assertion of this type, but with a limited number of symbols":

Rayo-namable-in(m, n) ↔
   ∃Φ(x₁): {
      Φ has fewer than n symbols ∧
      ∃s: s = Assign(m, x₁) ∧
      (∀t: Sat([Φ(x₁)],t) → t = Assign(m, x₁))
   )

This is the fully powerful version of the toy ST-namable-in() function that we explored above.

Agustín Rayo's Number

Having gotten all that out of the way, the rest is simple. The "busy beaver function" for this assertion-schema in von Neumann universe, is a function FOST(x), named after the initials of "first order set theory".

FOST(x) = The smallest number n for which Rayo-namable-in(n, x) is false.

Then Rayo's number is FOST(10¹⁰⁰).

BIG FOOT

In the years since the Big Number Duel, an online wiki / forum has built up, centred around the "Googology wiki" on wikia.com.

Not satisfied with Rayo's number, the self-named "googologists" have made several attempts to top it. Re-use of earlier ideas does not count; any of these:

FOST(10¹⁰⁰) + 1
10^{FOST(10¹⁰⁰)}
FOST(10^10¹⁰⁰)
FOST(Mega)
FOST(Graham)
FOST(googol→googol→googol→googol→googol)
FOST(Bowers{googol,googol,(googol),googol})
FOST(BB(googol))
FOST(FOST(googol))
FOST¹⁰(googol)

would not considered a new champion, because (under the rules of the Big Number Duel that spawned Rayo's number), every new champion must use a significantly new technique.

In 2014 October, googologist Wojowu (a.k.a. "LittlePeng9") described something called "first order oodinal theory" (deliberate misspelling of "ordinal") as an attempt to increase the "strength" of the first order logic used by Rayo. They then defined a function "FOOT(n)" similarly to the definition of the Rayo FOST(n) function, then defined "BIG FOOT" to be the result of ten iterations of FOOT(n) starting with n=10¹⁰⁰. However, the underlying formal system was shown to contradict itself, by googologist p進大好きbot in 2018 August.

The Frontier

As of this writing (last checked in 2016), this seems to be the frontier of development for the expression of large finite numbers. Of course, many people try, but everything seen so far appears to duplicate or fall short of the results shown here so far. At the very least, it seems one now needs to be proficient in computation theory, set theory, and formal logic to stand a chance of creating a new champion.

If you're interested in defining larger functions, go right ahead, please check your new function carefully to see if it really pushes the limits a significant amount. If you only use the methods described on these pages, then your new function will not push the limits a significant amount.

First page . . . Back to page 8 . . . Forward to page 10 . . . Last page (page 11)

Japanese readers should see: 巨大数論 (from @kyodaisuu on Twitter)

If you like this you might also enjoy my numbers page.

s.30