A368006 Rayo's function: smallest natural number larger than any number uniquely defined by an n-symbol formula in First Order Set Theory.

0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 1, 0, 1, 1, 1, 0, 1, 1, 1, 1, 1, 1, 1, 1, 2

Offset

0,31

Comments

The alphabet consists of the 7 symbols ∈, =, (, ), ~, ∧, ∃, plus infinitely many variables x_i, for i >= 0, each considered one symbol.

"x_i∈x_j" and "x_i=x_j" are atomic formulas.

If θ is a formula, then "(~θ)" is a formula (the negation of θ).

If θ and ξ are formulas, then "(θ∧ξ)" is a formula (the conjunction of θ and ξ).

If θ is a formula, then "∃x_i(θ)" is a formula (existential quantification).

A formula having x_0 as its only free variable defines a number m if it has a satisfying assignment, and all such assignments assign m to x_0.

Mexican philosophy professor Agustín Rayo defined a nondecreasing version of this function in a "big number duel" at MIT on 26 January 2007.

Its value at n=10^100 is known as Rayo's number.

This is a set theoretic analog of the busy beaver function, which it easily outgrows.

Links

Table of n, a(n) for n=0..30.

Googology Fandom, Low-level Rayo bounds

Googology Fandom, Proof that Rayo(n) is 1 for n between 10 to 19

Wikipedia, Rayo's Number

Example

a(30)=2, since the 30 symbol formula "(∃x_1(x_1∈x_0)∧(¬∃x_1(∃x_2((x_2∈x_1∧x_1∈x_0)))))" uniquely defines the number 1, while smaller formulae can only define the number 0, the smallest being the 10 symbol "(¬∃x_1(x_1∈x_0))".

Crossrefs

Cf. A028444.

Sequence in context: A353418 A361161 A364420 * A374061 A374276 A037281

Adjacent sequences: A368003 A368004 A368005 * A368007 A368008 A368009

Keyword

nonn,more

Author

John Tromp, Dec 07 2023

Status

approved