In my previous attempt to create a record Rayo name for 65536, I've used classic definition of ordered pairs ((x,y)={{x},{x,y}}.
Ordered pairs are quite symbol-extensive, so it would be nice if we could find a way to circumnavigate their use. This can indeed be done, by replacing (x,y) with the ordinary doubleton {x,y} and using other means to ensure that this doesn't lead to ambiguity.
The idea is simple:
1. When seeking a bijection from set A to set B, we will notate the ordered pairs as {x,y} where x∈A and y∈B.
2. If x∈A and x∉B then the meaning of {x,y} is non-ambigious: x must be the representative of A and y must be the representative of B.
3. If x∈A⋂B the we will always pair it with itself. In other words, we will only be interested in bijections that map the members of A⋂B to themselves. The relevant "ordered" pair here will then be {x,x}={x} which is - again - not ambigous.
We will call such unambigous pairs good pairs. A set of such pairs, will be called a good relation form A to B.
Let f be a good relation from A to B. If for every x in A there's exactly one good pair in f containing x, and if for every y in B there's exactly one good pair in f containing y, then we will call f a good bijection.
These concepts are, of-course, an analogue to ordinary ordered pairs, relations, functions and bijections. They have precisely the same purpose (even though they are formally different, as they represent different sets).
Moreover, it's easy to see that if |A|=|B| and if A and B are finite then there's always a good bijection between A and B. Hence these concepts can be used to check the cardinality of finite sets, instead of using fully-fledged bijections.
In short, we can use these simplified "ordered pairs" and "functions" to repeat the process that was done in my previous blog post step-by-step, while cutting off many symbols from the final tally. The results are given in this table (which was designed to be completely self-sufficient for easy reading):
| Ref Point | Shortcut | Meaning | String | Length | Use of previous ref points |
|---|---|---|---|---|---|
| 1 | x is equal to y | x=y | 3 | basic Rayo string | |
| 2 | x is a member of y | x∈y | 3 | basic Rayo string | |
| 3 | A and B are both true | (A∧B) | L(A)+3+L(B) | basic Rayo construction | |
| 4 | There is a set x such that A is true | ∃x(A) | 4+L(A) | basic Rayo construction | |
| 5 | A is false | (¬A) | 3+L(A) | basic Rayo construction | |
| 6 | x≠y | x and y are different sets | (¬x=y) | 3+3=6 | 1,5 |
| 7 | x∉y | x is not a member of y | (¬x∈y) | 3+3=6 | 2,5 |
| 8 | ∄x(A) | There's no set x for which A is true | (¬∃x(A)) | 7+L(A) | 4,5 |
| 9 | a∈b⋂c | a is an element of both in b and c | (a∈b∧a∈c) | 3+3+3=9 | 2,3 |
| 10 | A∨B | Either A or B (or both) are true | (¬((¬A)∧(¬B))) | L(A)+12+L(B) | 3,5 |
| 11 | x⊄y | x is not a subset of y | ∃z(z∈x∧z∉y) | 4+3+3+6=16 | 2,3,4,7 |
| 12 | x⊆y | x is a subset of y | (¬x⊄y) | 3+16=19 | 5,12 |
| 13 | y=𝒫(x) | y is the powerset of x | (∄t((t⊆x∧t∉y)))∧(∄t((t⊄x∧t∈y))) | (7+(19+3+6))+3+(7+(16+3+3))=67 | 2,3,7,8,11,12 |
| 14 | x∉Tran | x is not a transitive set | ∃y(∃z(z∈y∧y∈x∧z∉x)) | 4+(4+(3+3+3+3+6)))=26 | 2,3,4,7 |
| 15 | x∈Tran | x is a transitive set | (¬x∉Tran) | 26+3=29 | 14 |
| 16 | x∈Ord | x is an ordinal | (x∈Tran∧(∄y(y∈x∧y∉Tran))) | 29+3+(7+3+3+26)=71 | 2,3,8,14,15 |
| 17 | z⊆{x,y} | z has no elements other than x and y | ∄t(t∈z∧t≠x∧t≠y) | 7+(3+3+6+3+6)=28 | 2,3,6,8 |
| 18 | z={x,y} | (z⊆{x,y}∧x∈z∧y∈z) | 28+3+3+3+3=40 | 2,3,17 | |
| 19 | u={x,y}a,b | u={x,y} where x∈a and y∈b |
(u={x,y}∧x∈a∧y∈b) |
40+3+3+3+3=52 | 2,3,9,18 |
| 20 | u=(x,y)a,b | u={x,y} is a good pair taken from a,b |
(u={x,y}a,b∧(x=y∨(x∉b∧y∉a)) |
52+3+(6+12+(3+3+6))=85 |
1,3,7,10,19 |
| 21 | uc=t | the element taken from c in the good pair u | t∈c⋂u | 9 | 9 |
| 22 | GRel(f,a,b) | f is a good relation from a to b | ∄u(u∈f∧∄x(∃y(u=(x,y)a,b))) | 7+(3+3+7+(4+52))=109 | 2,3,4,8,20 |
| 23 | DmUnq(f,a,x) | f(x) exists and is unique |
∃u(u∈f∧ua=x∧∄v(v∈f∧va=x∧v≠u)) |
4+(3+3+9+3+(7+3+3+9+3+6)=53 | 2,3,4,6,8,21 |
| 24 | ImUnq(f,b,y) | f -1(y) exists and is unique | ∃u(u∈f∧ub=y∧∄v(v∈f∧vb=y∧v≠u)) | 4+(3+3+9+3+(7+3+3+9+3+6)=53 | 2,3,4,6,8,21 |
| 25 | ∀a∈b(A) | For every a in b, A is true | ∄a(a∈b∧(¬A)) | L(A)+16 | 2,3,5,8 |
| 26 | GBjc(f,a,b) | f is a good bijection from a to b |
GRel(a,b)∧∀x∈a(DmUnq(f,a,x))∧ ∀y∈b(ImUnq(f,b,y)) |
109+3+(53+16)+3+(53+16)=253 | 3,22,23,24,25 |
| 27 | IsEmkFour(x) | using Emk's trick to create a 4-member set |
∃b∃c∃d∃e(b∈y∧c∈b∧d∈c∧e∈d∧ c∈y∧d∈y∧e∈y∧¬∃f(f≠b∧f≠c∧ f≠d∧f≠e∧f∈y) |
104 | (credit for this trick goes to Emk) |
| 28 | Set16(x) | A set that has 16 elements | ∃y(x=𝒫(y)∧IsEmkFour(y)) | 4+(67+3+104)=178 | 3,4,13,27 |
| 29 | Set65536(x) | Has 65536 elements | ∃y(x=𝒫(y)∧Set16(y)) | 4+(67+3+178)=252 | 3,4,13,28 |
| 30 | |x|=|y| | x and y have the same number of elements | ∃f(GBjc(f,x,y)) | 4+253=257 | 4,26 |
| 31 | x=|y| | x is the number of elements in y | (x∈Ord∧x=|y|) | 71+3+257=331 | 3,16,30 |
| 32 | x=65536 | Rayo name for 65536 | ∃y(x=|y|∧Set65536(y)) | 4+331+3+252=590 | 3,4,29,31 |
So Rayo(590)>65536 and Rayo(294+74n)>2↑↑n
We could also define sets of 3 or 5 elements instead of 4 in step 27, with 79 and 129 symbols respectively.
This leads to the following lower bounds:
Rayo(516)>16
Rayo(531)>32
Rayo(565)>256
Rayo(590)>65536
Rayo(615)>4294967296
Rayo(639)>2256
Rayo(664)>265536
and so on.