A bounded-length Rayo function assigns to a nonnegative integer 
the least nonnegative integer exceeding every
nonnegative integer specified by a sentential
formula of at most 
symbols in first-order logic in the language
of set theory. Fix the following syntax. For 
, the atomic formulas
are 
and 
. From formulas 
and 
, 
,
, and 
can be formed. Each occurrence of 
, 
, 
,
, 
, either parenthesis,
or a variable name counts as one symbol, with spaces
ignored. In particular, 
counts as one symbol regardless of its subscript.
Here nonnegative integers are identified with finite ordinal numbers
in their standard von Neumann representation. Let 
be the set of nonnegative
integers 
for which a sentential formula of at most 
symbols has 
as its only free variable
and is true iff 
in the intended interpretation
of set theory. Define 
when 
, and 
otherwise. Only finitely many sentential
formula patterns of bounded length remain after renaming bound
variables, so 
is finite. Since 
, 
. This uses semantic satisfaction,
rather than provability in an arbitrarily chosen axiomatic
system.
An exact-length variant 
instead uses formulas of exactly 
symbols and has values 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0,
... for 
,
1, ... (OEIS A368006). It uses the same syntax
and interpretation, with value 0 when no nonnegative
integer is definable. The two conventions are related by
 |
Thus the exact-length values can decrease even though their running maximum cannot. The strict-length convention for Rayo's number gives
.
