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

Author

John Tromp, Dec 07 2023

Keywords

• nonn
• more

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.

Examples

			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))".
		

Links

• Googology Fandom, Low-level Rayo bounds
• Googology Fandom, Proof that Rayo(n) is 1 for n between 10 to 19
• Wikipedia, Rayo's Number

Crossrefs

Cf. A028444.