Introduction[]
The basic insight on which this proof is based, is that we can safely ignore any substrings which are either tautologies or contradictions. It's easy to show that such substrings either has no effect on the compound string, or they turn the compound string itself into a tautology/contradiction:
Let A,B be tautologies.
Let C,D be contradictions.
Let E be any other expression.
Then using Rayo's rules, we can build the following 9 statements (and only them):
(a) (¬A) which is a contradiction.
(b) (¬C) which is a tautology.
(c) (A∧B) which is a tautology.
(d) (A∧C) / (C∧A) which is a contradiction.
(e) (C∧D) which is a contradiction.
(f) (A∧E) / (E∧A) which is equivalent to E.
(g) (C∧E) / (E∧C) which is a contradiction.
(h) ∃xi(A) which is a tautology (if A is always true, then there definitely exists an xi for which A is true).
(i) ∃xi(C) which is a contradition (if C is always false, then there can't be an xi for which C is true).
So now we can start building a list of Rayo expressions of increasing length, while ignoring all expressions which are:
(a) tautologies.
(b) contradictions.
(c) logically equivalent to a shorter string we've already arrived at.
And for ease of typing, I will use the lower case letters a,b,c,... instead of x's with subscripts.
The List[]
Length 3:
1. a=b
2. a∈b
(both a=a and a∈a are ignored. The first one is a tautology and the second one is a contradiction)
Length 6:
can only be formed by negation of a length 3 expression, so:
3. a≠b
4. a∉b
Length 7:
Can only be formed by adding a existence qualifier to a length 3 expression, so:
5i. There exists a (or there exists b) for which a=b.
5ii. There exists a for which a∈b
5iii. There exists b for which a∈b
Of these, 5i and 5iii are tautologies. 5ii, on the other hand, is equivalent to:
5. a≠∅
Length 9:
Can be formed by either negating a length 6 expression, or conjucting two length 3 expression. Negating #3 and #4 gives us #1 and #2 again, so we can ignore these. Conjucting 1 and 2, gives us the following possible statements:
6. a=b=c
7. a=b, c=d
8. (a=b)∈c
9. c∈(a=b)
10. a=b, c∈d
11. a∈b∩c
12. a∈b∈c
13. a∈b, c∈b
14. a∈b, c∈d
Length 10:
Can be formed by negating a length 7 expression or by adding an existence qualifier to a length 6 expression. The latter will always result in a tautology (for any set X, there's always a set which isn't a member of X as well as a set that isn't equal to X). So we are left with the negation of #5:
15. a=∅ (which is - of course - the Rayo Name for 0)
Length 12:
can be formed by either negating a length 9 expression, or conjucting a length 3 expression with a length 6 expression.
So we get #16-#24 by negating #6-#14:
16. ¬(a=b=c)
17. (a≠b) or (c≠d)
18. (a≠b) or (a∉c)
19. (a≠b) or (c∉a)
20. (a≠b) or (c∉d)
21. a∉b∩c
22. ¬(a∈b∈c)
23. (a∉b) or (c∉b)
24. (a∉b) or (c∉d)
And we get #25-#39 by conjucting #1/#2 with #3/#4:
25. (a=b∧a≠c)
26. (a=b∧c≠d)
27. (a=b∧a∉c)
28. (a=b∧c∉a)
29. (a=b∧c∉d)
30. (a∈b∧a≠c)
31. (a∈b∧b≠c)
32. (a∈b∧c≠d)
33. a∈b – c
34. (a∈b∧c∉a)
35. (a∈b∧b∉c)
36. (a∈b∧c∉b)
37. (a∈b∧c∉d)
The reader can verify that all other combinations (such as (a=b∧a∉b)) are either contradictions, tautologies or equivalent to an earlier string.
Length 13:
There are three kinds of expressions of this form: (¬10), ∃x(9) or (3∧7) (where the numbers represent expressions of the relevant length).
Since things are beginning to get confusing at this point, I'm going to write down every single combination this time
The only length 10 statement is #12, and negating it gets us back to #5.
The format ∃x(9) gives gives rise to the following expressions.
∃a(a=b=c) ≅ ∃b(a=b=c) ≅ ∃c(a=b=c) ≅ a=b (#1)
∃a(a=b∧c=d) ≅ ∃b(a=b∧c=d) ≅ ∃c(a=b∧c=d) ≅ ∃d(a=b∧c=d) ≅ a=b (#1)
∃a((a=b)∈c) ≅ b∈c ≅ a∈b (#2)
∃c((a=b)∈c) ≅ a=b (#1)
∃a(c∈(a=b)) ≅ c∈b ≅ a∈b (#2)
∃c(c∈(a=b)) ≅ c∈b ≅ a∈b (#2)
38. ∃c(c∈(a=b)) ≅ (a=b∧a≠∅)
∃a(a=b∧c∈d) ≅ ∃b(a=b∧c∈d) ≅ c∈d ≅ a∈b (#2)
39. ∃c(a=b∧c∈d) ≅ (a=b∧d≠∅) ≅ (a=b∧c≠∅)
∃d(a=b∧c∈d) ≅ a=b (#1)
40. ∃a(a∈b∩c) ≅ (b∩c≠∅) ≅ (a∩b≠∅)
∃b(a∈b∩c) ≅ a∈c ≅ a∈b (#2)
41. ∃a(a∈b∈c) ≅ (b∈c∧b≠∅) ≅ (a∈b∧a≠∅)
42. ∃b(a∈b∈c) (there's no simpler way to write this one)
∃c(a∈b∈c) ≅ a∈b (#2)
∃a(a∈b, c∈b) ≅ c∈b ≅ a∈b (#2)
∃b(a∈b, c∈b) is a tautology
43. ∃a(a∈b, c∈d) ≅ (c∈d∧b ≠∅) ≅ (a∈b∧c ≠∅)
∃b(a∈b, c∈d) ≅ c∈d ≅ a∈b (#2)
And the format of (3∧7) gives us the following possibilities:
(a=b∧a≠∅) (equivalent to #38)
(a=b∧b≠∅) (equivalent to #38)
(a=b∧c≠∅) (equivalent to #39)
(a=b∧a≠∅) (equivalent to #38)
(a∈b∧a≠∅) (equivalent to #41)
(a∈b∧b≠∅) ≅ a∈b (equivalent to #2)
(a∈b∧c≠∅) (equivalent to #43)
And that's it for Rayo expressions which has 13 characters or less. As will be shown in the next section, this is all we need to prove that Rayo(n)=1 for 10 ≤ n ≤ 19.
Proof that Rayo(n)=1 for 10 ≤ n ≤ 19.[]
A Rayo Name must have exactly one free variable. We will show that all such expressions, if they name a number at all, name the number 0.
First of all, for n ≤ 13, we can check the 43 expressions we've found directly. Only #5 and #15 have exactly 1 free variable. Expression #5 is not a Rayo Name at all. Expression #15 names the number 0.
For n>13, we will only list the possible formats (the numbers representing the length of the Rayo substrings) and possible number of free variables of each:
Length 15
1. (3∧9): At least 3 (since all length-9 expressions have at least 3 free variables)
2. (6∧6): At least 2 (since all length-6 expressions have exactly 2 free variables)
3. (¬12): At least 3 (since all length-12 expressions have at least 3 free variables)
Length 16
4. (3∧10): At least 2 (since all length-3 expressions have exactly 2 free variables)
5. (6∧7): At least 2 (since all length-6 expressions have exactly 2 free variables)
6. (¬13): At least 2 (since all length-13 expressions have has at least 2 free variables)
7. ∃x(12): At least 2 (since all length-12 expressions have at least 3 free variables)
Length 17
8. (a≠∅∧a≠0) - equivalent to #5
9. (a≠∅∧b≠0) - has two free variables.
10. ∃x(13): At least one less free variable than the (13).
Length 18
11. (3∧12) - at least 3 free variables (due to the 12)
12. (6∧9) - at least 3 variables (due to the 9)
13. (¬15): At least 2 (since all length-15 expressions have has at least 2 free variables)
Length 19
14. (3∧13) - at least 2 free variables (due to the 3)
15. (6∧10) - at least 2 free variables (due to the 6)
16. (7∧9) - at least 3 free variables (due to the 9)
17. (¬16): At least 2 (since all length-16 expressions have has at least 2 free variables)
18. ∃x(3∧9): At least 2 free variables.
19. ∃x(6∧6): At least one less free variable than the (6∧6)
Of these, only formats #10 and #19 can have exactly 1 free variable and therefore have the potential of being a valid Rayo name.
We'll know show that niether can name any number (except zero):
First class of cases (length 17):
∃x(13) where "13" is an expression that has exactly two free variables. The only possibilities here are:
1. ∃a(a=b∧a≠∅) ≅ b≠∅ ≅ a≠∅ (equivalent to #5)
2.∃b(a=b∧a≠∅) ≅ a≠∅ (equivalent to #5)
3. ∃a((a∩b)≠∅) ≅ b≠∅ ≅ a≠∅ (equivalent to #5)
4. ∃b((a∩b)≠∅) ≅ a≠∅ (equivalent to #5)
5. ∃a(a∈b∧a≠∅) ≅ b \ { ∅ } ≠ ∅ ≅ a \ { ∅ } ≠ ∅ (which is new, but obviously not a Rayo name)
6. ∃b(a∈b∧a≠∅) ≅ a \ { ∅ } ≠ ∅ (equivalent to #5 on this list)
7. ∃a∃b(a∈b∈c) ≅ c \ { ∅ } ≠ ∅ ≅ a \ { ∅ } ≠ ∅ (equivalent to #5 in this list)
8. ∃c∃b(a∈b∈c) is a tautology
None of these expression is a Rayo Name, hence the completion of the proof for this class of cases.
Second class of cases (length 19):
∃x(6∧6) where "6∧6" is an expression that has exactly two free variables.
This can only happen if both 6's have the same two variables. We can also assume that the two 6's are different (otherwise the conjuction would be equivalent to one of them alone). So we get the following:
9.∃a(a≠b∧a∉b)
10.∃b(a≠b∧a∉b)
11.∃a(a≠b∧b∉a)
12.∃b(a≠b∧b∉a)
13.∃a(a∉b∧b∉a)
14.∃b(a∉b∧b∉a)
All six expressions are tautologies and are therefore not Rayo names.
Hence the completion of the proof that no number other than 0 is Rayo namable in 19 symbols or less.
QED