Complete definition of Rayo(n)

First, we are going to create a "language", which I'll call FOST (first-order set theory). It works as the following:

- We have "formulas": these are "sentences" of the FOST language, and they have a truth: "true", or "false".

- We have parenthesis to delimitate formulas

- We have "sets": they starts with a "{" and end with a "}". A set must be empty of contain another set.
- We have the equality symbol "=". "A = B" means that sets A and B have the same elements in the same order
- We have infinitely many variables x₁, x₂, x₃, etc... These are sets. (e.g. "x₁₉ = {0,5,7}")
- We have membership "∈". "A∈B" means "A is an element of B".

- We have the quantifier "for all": "∀x(φ)" is a formula that is true if the formula φ is true no matter that the set x is.
- We have the quantifier "there exists": "∃x(φ)" is a formula that is true if there exists a set x such that the formula φ is true
- We have the logical "and": "A ∧ B" (where A and B are both formulas) is a formula that is true if A and B are both true
- We have the logical "or": "A ∨ B" is a formula that is false if A and B are both false
- We have the logical "if ... then ...": "A → B" is a formula that is false if A is false but B is true
- We have the logical "if and only if": "A ↔ B" is a formula that is true if A and B have the same truth
- We have the logical "not": "¬A" is a formula that is false if A is true

- If a formula isn't true, it is false. If it isn't false, it is true.

We define a natural number as following:
- The empty set is 0
- The successor of the natural number x is the set with the same elements than x, but with x appended at its end
For example:
{} = 0
{{}} = {0} =1
{{},{{}}} = {0,1} = 2
{{},{{}},{{},{{}}}} = {0,1,2} = 3
{0,1,2,3} = 4
{0,1,2,3,4} = 5
...
{0,1,2,...,n} = n+1

Then, Rayo(n) is the smallest number bigger than all numbers definable by FOST in at most n symbols

Since the FOST language can define Graham's Function, BEAF, BAN, n(k), TREE(k), SCG(k), BH(k), D(k), Σ(k), Ξ(k) and most of other functions currently defined, Rayo(n) grows faster than all these functions. Thus, a number such as Rayo(10¹⁰⁰) is far bigger than everything we could imagine!

Note that the FOOT function is even faster, but is basically a (strong) extension of the FOST language