I assume that axiom of extensibility, axiom of empty set, axiom of pairing, and axiom of regularity.
All possible Rayo strings whose length is 10 are:
- ∃x_i(¬x_j∈x_k)
- ∃x_i(¬x_j=x_k)
- ¬∃x_i(x_j∈x_k)
- ¬∃x_i(x_j=x_k)
i≠1 because a valid Rayo name must have a free occurence of x_1.
j=1 or k=1 (or both) for the same reason as above.
if i≠j and i≠k, the quantifier is redundant and therefore it reduces to the case of length 6.
So the all possible patterns are:
- ∃x_i(¬x_i∈x_1): holds whenever s(x_1)=s(x_i).
- ∃x_i(¬x_1∈x_i): holds whenever s(x_1)=s(x_i).
- ∃x_i(¬x_i=x_1): holds whenever s(x_1)={s(x_i)}.
- ¬∃x_i(x_i∈x_1): names 0.
- ¬∃x_i(x_1∈x_i): contradicts with axiom of pairing.
- ¬∃x_i(x_i=x_1): contradiction (counter example: s(x_1)=s(x_i))
Plain'N'Simple has shown that Rayo(n)=0 for all n < 10.
∴Rayo(10)=1.