To everyone: I would really appreciate if you check my work and point out any errors.
In this blog post I'll construct a Rayo string that returns 65536. With minor adjustments, this constructions can also be used to show that:
Rayo(835+96n) > 2↑↑n
Rayo(714+87n) > 2↑↑n
This will be done by the following steps:
1. Writing shortcuts for several simple logical expressions in Rayo's language.
2. Constructing an expression for "x is the powerset of y".
3. Constructing an expression for "x is an ordinal".
4. Constructing an expression for "z=(x,y)" where (x,y) is the ordered pair {{x},{x,y}}.
5. Using #4 to check when two sets have a one-to-one correspondence, and to construct an expression for "x and y have the same number of elements".
6. Bringing it all together, and writing the expression for "x is an ordinal which has the same number of elements as P(P(P(2)))" One last remark before we begin: In order to keep track of the number of symbols, I will use L(X) to denote the number of symbols in the expression X. This will be needed because some of our constructions will allow the use of arbitrary expressions within them.
And now, without further ado, let us begin:
Step 1: Some Simple Logical and Set Theoretic Constructs
| Ref Point | Shortcut | Meaning | String | Length | Use of previous ref points |
|---|---|---|---|---|---|
| r0 | (Sub(e,x,q)) | The expressions e where every instance of x is replaced with q | ... | L(e) | None |
| r1 | (e⇒f) | if e then f | (¬(e∧(¬f))) | L(e)+L(f)+9 | None |
| r2 | (e⇔f) | iff e then f | ((e⇒f)∧(f⇒e)) | 2L(e)+2L(f)+21 | r1 |
| r3 | ∀x(e) | For all x, e is true | (¬∃x((¬e)) | L(e)+9 | None |
| r(π) | ∃!x(e) | The exists a single x such that e is true |
(∃x(e)∧((Sub(e,x,q))⇒x=q)) |
2L(e)+19 | r0,r1 |
| r4 | x≠y | x not equal to y | (¬x=y) | 6 | None |
| r5 | x∉y | x not a member in y | (¬x∈y) | 6 | None |
| r6 | x⊆y | x is a subset of y | ∀z(z∈x⇒z∈y) | (3+3+9)+9=24 | r1,r3 |
Step 2: Powersets and Defining a 65536-Element Set
| Ref Point | Shortcut | Meaning | String | Length | Use of previous ref points |
|---|---|---|---|---|---|
| r7 | x=𝒫(y) | x is the powerset of y | (∀z(z∈x⇔z⊆y)) | (2·3+2·24+21)+9=84 | r2,r3,r6 |
| r8 | x6=2 | the ordinal 2 |
(∃x7(∃x8(((x7∈x6∧x8∈x6)∧(¬x7=x8))))∧ (¬∃x7((x7∈x6∧∃x8(∃x9((x8∈x7∧x9∈x8))))))) |
59 | GWiki Rayo article |
| r9 | (e∧f) | e and f | (not a shortcut. just a reference for length calculation) | L(e)+L(f)+3 | None |
| r10 | unused | ||||
| r11 | x4=𝒫(2) | (4 elements) | (x4=𝒫(x6)∧x6=2) | 84+3+59=147 | r7,r8,r9 |
| r12 | x3=𝒫2(2) | (16 elements) | (x3=𝒫(x4)∧x4=𝒫2(1)) | 84+3+147=234 | r7,r9,r11 |
| r13 | x2=𝒫3(2) | (65536 elements) | (x2=𝒫(x3)∧x3=𝒫3(1)) | 84+3+234=321 | r7,r9,r12 |
Steps 3 and 4: Ordinals and Ordered Pairs
| Ref Point | Shortcut | Meaning | String | Length | Use of previous ref points |
|---|---|---|---|---|---|
| r14 | (Mutex(x,y)) | Niether x or y is an element of the other | (x∉y∧y∉x) | 6+3+6=15 | r1,r3,r6 |
| r14.1 | x1∈On | x1 is an ordinal |
∀z((z∈x1⇒(z⊆x1∧(¬∃y((y∈x1∧(Mutex(y,z)))))))) |
76 | r1,r3,r6 |
| r15 | (Noelex(t,x,y)) | There are no elements in t except (perhaps) x and y. |
∀z((z≠x∧z≠y)⇒(z∉t)) |
((6+6+3)+6+9)+9=39 | r1,r3,r4,r5,r9 |
| r16 | z=(x,y) | z={{x},{x,y}} | ∀t(t∈z⇔(x∈t∧(Noelex(t,x,y)))) | ((3·2+(3+39+3)·2)+21)+9=126 | r2,r3,r9,r15 |
Step 5: One-to-one Correspondences
The most natural way to proceed here, would be to begin with defining "z is a function from x to y".
However, it turns out that the full definition of a function is not necessary here. Specifically, we do not care whether z contains elements that are not members of x×y. The only thing we will require here, is that z∩(x×y) is a function from x to y. This sounds like a cumbersome choice, but the Rayo-language definition for this idea is actually simpler then the Rayo-language definition of an ordinary function from x to y.
| Ref Point | Shortcut | Meaning | String | Length | Use of previous ref points |
|---|---|---|---|---|---|
| r17 | xZy | (x,y)∈z | ∃t((t=(x,y)∧t∈z)) | 3+(126+3+3)+1=136 | r9,r16 |
| r18 | (func(x,y,z)) | z∩(x×y) is a function from x to y | ∀t((t∈x⇒(∃!u((u∈y∧tZu)))))) | (5+((3+136+3)·2+19))+9+9=326 | r2,r3,r-π,r9,r18 |
| r19 | (cunf(x,y,z)) | z∩(x×y) is a relation whose inverse is a function from y to x | ∀u((u∈y⇒(∃!t((t∈x∧tZu)))))) | (5+((3+136+3)·2+19))+9+9=326 | r2,r3,r-π,r9,r18 |
| r20 | (biject(x,y,z)) | z∩(x×y) is a bijection from x to y | ((func(x,y,z))∧(cunf(x,y,z))) | 326+326+3=655 | r9,r17,r19 |
Step 6: Defining the number 65536
| Ref Point | Shortcut | Meaning | String | Length | Use of previous ref points |
|---|---|---|---|---|---|
| r21 | Cx=Cy | x and y have the same cardinality | ∃z((biject(x,y,z))) | 655+4=659 | r20 |
| r22 | Cx1=65536 | x1 has 65536 elements | (Cx1=Cx2∧x2=𝒫3(2)) | 659+321+3=983 | r9,r13,r21 |
| r23 | x1=65536 | x1 is the ordinal 65536 | (Cx1=65536∧x1∈On) | 983+76+3=1062 | r14.1,r22 |
And the final line means that:
Rayo(1219) > 65536
Rayo(1062) > 65536 (updated after learning Rayo's precise syntax requirements, which tend to make the strings a bit shorter)
Moreover, we can repeat the powerset step any arbitrary number of times, right after step r13. Every such step adds a "price" of another 87 symbols to our string, so we can write:
Rayo(714+87n) > 2↑↑n for all n.
Further improvements based on work by others:
1. 12AbBa spotted that the powerset definition has 3 redundant double negatives, which saves a total 12 symbols per powerset operation. This lowers the symbol count by 36 for 65536, and 12(n-1) for the general case:
Rayo(1026) > 65536
Rayo(726+75n) > 2↑↑n for all n.
2. P進大好きbot found a more compact way to describe subsets: (¬∃z((z∈x∧z∉y))). Putting that in place of r6 above, we get a reduction of 5 symbols (24 to 19) for subsets and a reduction of 10 symbols for the powerset. 12AbBa's double negatives still apply (since both expressions for subsets begin with "(¬∃")), and therefore this is a net additional reduction.
This means that we can define powersets with 62 instead of 72 symbols, and Ordinals with 71 instead of 76 symbols. The total additional reduction is therefore 10x3+5=35 for 65536, plus 10 more for every n:
Rayo(991) > 65536
Rayo(731+65n) > 2↑↑n for all n.