This is a front-end for the Online Encyclopedia of Integer Sequences, made by Christian Perfect. The idea is to provide OEIS entries in non-ancient HTML, and then to think about how they're presented visually. The source code is on GitHub.
%I A368006 #21 Dec 19 2023 12:51:55 %S A368006 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 %N A368006 Rayo's function: smallest natural number larger than any number uniquely defined by an n-symbol formula in First Order Set Theory. %C A368006 The alphabet consists of the 7 symbols ∈, =, (, ), ~, ∧, ∃, plus infinitely many variables x_i, for i >= 0, each considered one symbol. %C A368006 "x_i∈x_j" and "x_i=x_j" are atomic formulas. %C A368006 If θ is a formula, then "(~θ)" is a formula (the negation of θ). %C A368006 If θ and ξ are formulas, then "(θ∧ξ)" is a formula (the conjunction of θ and ξ). %C A368006 If θ is a formula, then "∃x_i(θ)" is a formula (existential quantification). %C A368006 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. %C A368006 Mexican philosophy professor Agustín Rayo defined a nondecreasing version of this function in a "big number duel" at MIT on 26 January 2007. %C A368006 Its value at n=10^100 is known as Rayo's number. %C A368006 This is a set theoretic analog of the busy beaver function, which it easily outgrows. %H A368006 Googology Fandom, <a href="https://googology.fandom.com/wiki/User_blog:12AbBa/Low-level_Rayo_bounds">Low-level Rayo bounds</a> %H A368006 Googology Fandom, <a href="https://googology.fandom.com/wiki/User_blog:Plain'N'Simple/Proof_that_Rayo(n)_is_1_for_n_between_10_to_19">Proof that Rayo(n) is 1 for n between 10 to 19</a> %H A368006 Wikipedia, <a href="https://en.wikipedia.org/wiki/Rayo%27s_number">Rayo's Number</a> %e A368006 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))". %Y A368006 Cf. A028444. %K A368006 nonn,more %O A368006 0,31 %A A368006 _John Tromp_, Dec 07 2023