Talk: Rayo's number/Archive 1

More rigorous definition[]

Need upper and lower bounds for the more rigorous definition of this number... Ikosarakt1 (talk) 12:31, July 19, 2012 (UTC)

The formal definition of this number is found in a cited source. In all honesty, I can't make much sense of it. FB100Z • talk • contribs 20:28, July 19, 2012 (UTC)

Correct me if I'm wrong, but couldn't the fast growing hierarchy be defined within first order set theory? Is so, how can a growth rate within the fast growing hierarchy be specified? How was this result obtained, or where did it come from? Sbiis Saibian (talk) 00:18, January 20, 2013 (UTC)

This article may be helpful for you. Ikosarakt1 (talk) 13:43, January 22, 2013 (UTC)

Thank you for the resource. I have never seen this guy's work before. It seems there are many "googologist's" on the internet, even if they aren't aware of the term or the fact that there is at least one community of googologist's. I have been wondering what the largest well defined number is (let's not quibble like the mathematicians over the well foundedness of such a concept -_-), or more correctly, what the fastest growing well defined paradigm is for sometime. I have heard of oracle turing machines, but I wasn't sure whether that was still included within first order set theory or not. I was also not sure how much of ordinal notation (and consequently how much of the fast-growing hierarchy) was included. There are also a few other miscellaneous concepts which I haven't gotten around to deciding which is stronger. I will have to bookmark these articles and give them a good read. It appears that this guy, at least for the moment, is the champion by all reasonable measures.

Sbiis Saibian (talk) 15:22, January 22, 2013 (UTC)

Corrected strength of function[]

In cimments to this post me and A.P.Goucher concluded, that actual strength of Rayo's function is nuch larger than \(\omega^\text{CK}_1 \times \omega\). It is at level of \(\omega^\text{CK}_\omega\).

First few values[]

What do you think, is it possible to evaluate (or prove lower bounds) small values of Rayo(n)? Ikosarakt1 (talk) 10:07, January 30, 2013 (UTC)

Even the definition of ℜ(n) is enough to make my head hurt, let alone the size of ℜ(10¹⁰⁰). FB100Z • talk • contribs 19:43, February 5, 2013 (UTC)

My guess is that Rayo(10) is the smallest value that has a definition. To my knowledge, it's not possible to force the value of x₁ with less than 10 symbols.

Bounds[]

If we use the naive method of defining the ordinals, by putting 0 in variable 2, 1 in variable 3, 2 in variable 4, etc. we can define a very weak, but rigorous lower bound for Rayo(n).

Defining "(¬∃1(1∈2))" (10 symbols) puts a 0 in x₂.
Defining "(1∈2∧(¬∃1(1∈3∧(¬1=2))))" (23 symbols) puts a 1 in x₃.
Defining "(2∈3∧(¬∃1(1∈4∧((¬1=2)∧(¬1=3)))))" (32 symbols) puts a 2 in x₄.
Defining "(3∈4∧(¬∃1(1∈5∧((¬1=2)∧((¬1=3)∧(¬1=4))))))" (41 symbols) puts a 3 in x₅.
etc.
AND-ing together n expressions takes an additional 3n - 3 symbols.
0 takes at most 10 symbols.
1 takes at most 3 + 23 symbols.
2 takes at most 6 + 23 + 32 symbols.
3 takes at most 9 + 23 + 32 + 41 symbols.
etc.

Therefore the number of symbols it takes to Rayo-name n is at most (9n² + 43n)/2. This gives the lower bound Rayo(10¹⁰⁰) >> 4.7140×10⁴⁹. FB100Z • talk • contribs 22:33, February 5, 2013 (UTC)

Does the variable 10 count as 1 symbol or 2? Also, (2∈1∧(¬∃3(3∈1∧(¬3∈2∧(¬3=2))))) makes 1 the successor of 2. Now we only have to use a linear number of characters to define numbers instead of it having to take a quadratic number of characters. Therefore Rayo(10¹⁰⁰) >>3.333x10⁹⁸. Tomtom2357 (talk) 14:27, June 10, 2013 (UTC)

In set theory each number is abstract concept, not composition of digits. Each number counts as one symbol. LittlePeng9 (talk) 18:09, June 10, 2013 (UTC)

These bounds don't give the grasp how large Ra(10^100) is. It would be nice to show that \(Ra(10^{100}) > S_{BB}(n)\) (for any reasonable n), where \(S_{BB}(n)\) is similar to Bird's \(S(n)\) function (described in his currently last part of array notations), but the rule M1 is replaced by \(\{a,b\} = \Sigma(b,a)\). Ikosarakt1 (talk ^ contribs) 14:41, June 10, 2013 (UTC)

A bit less than that, 0 requires ¬∃1:1∈2 (7 symbols), 1 requires 1∈2∧¬∃1∈3:¬3=2 using set-limitations (22 symbols), 2 requires 2∈3∧¬∃1∈4:¬1=2∧¬1=3 (42 symbols).

80.98.179.160 15:54, December 22, 2017 (UTC)

I'm having a bit of trouble defining addition using set theory. I'm sure once I get how to use recursive definitions, I'll be able to construct large numbers very quickly. Also, my expression above is incomplete, it ensures that the set 1 contains 2 and it does not contain any element that is not 2 or a member of 2. The correct expression is: 2∈1∧¬∃3(3∈1∧¬3∈2∧¬3=2)∧¬∃3(¬3∈1∧3∈2). I now know how to define the subset operation, ¬∃3(¬3∈1∧3∈2) states that 2 is a subset of 1. I can also define the union of 2 sets 2 and 3: ¬∃4(¬4∈1∧4∈2)∧¬∃4(¬4∈1∧4∈3)∧¬∃4(4∈1∧¬4=2∧¬4∈3) (makes 1 the union of 2 and 3). Actually, I can define the union of any set of sets: ¬∃3,4(3∈2∧4∈3∧¬4∈1)∧¬∃3(3∈1∧¬∃4(3∈4∧4∈2)) (1 is the union of all sets in 2). Interestingly, this is simpler than the earlier expression. Yes, I guess I am cheating with the ¬∃3,4 bit, but I couldn't figure out another way to do it. Tomtom2357 (talk) 06:03, June 11, 2013 (UTC)

¬∃3,4(X) is equivalent to ¬(∃3(∃4(X))). ∃3(∃4(X)) states that there exist pair for 3 and 4 so that X is true, just as ∃3,4(X) does, and negation in obvious way preserves equivalence. LittlePeng9 (talk) 11:13, July 5, 2013 (UTC)

At some point I hope to develop a tiny high-level language that will compile into FOST expressions. e.g. you could just type 1 + 2 and it'll take care of all the set theory and ordinal arithmetic for you. (It would be a weird language because you can't really do anything with the compiled code; you can only use it for proofs.) I make no promises about whether this project will ever materialize. FB100Z • talk • contribs 14:51, July 5, 2013 (UTC)

We'll need to figure out how to define addition and use recursion first. Tomtom2357 (talk) 15:42, July 5, 2013 (UTC)

If you want to do it in strictly formalized way, you must not only formalize sentence p(a,b,c)<=>v(a)+v(b)=v(c) (with v(x) meaning value of x), but also proof checker, which will disprove all p(a,b,d) for d different from c and prove p(a,b,c). I personally see no other way. LittlePeng9 (talk) 15:46, July 5, 2013 (UTC)

I made a page at User:FB100Z/FOST. Please contribute some formulas! FB100Z • talk • contribs 16:06, July 5, 2013 (UTC)

I contributed a few formulas to the page. We now have the union, intersection, and powerset operations. I'm still not sure how we define addition though. Tomtom2357 (talk) 03:27, July 6, 2013 (UTC)

Make the page about him itself.[]

You can make the page about him like sbiiss saibian and the peoples.

Jiawheinalt (talk) 11:28, February 14, 2013 (UTC)

Rayo's number is much larger![]

Apparently, in a blog post a few months ago, A.P. Goucher made the claim that Rayo's number was at the level of the order-\(\omega\) Busy Beaver function (and there at the level of \(\omega^\text{CK}_\omega\) in the fast-growing hierarchy, although this association has issues of its own). He therefore concluded that his Xi function grew faster. These statements have been repeated several times in this wiki. However, it is incorrect.

The trouble is that Goucher got the definition of Rayo's number wrong. The correct definition is, per the wiki article, "the smallest number bigger than any finite number named by an expression in the language of first order set theory with a googol symbols or less." Goucher, however, defined it as "the largest integer expressible uniquely by n symbols in first-order logic". He then goes on to define first-order logic, but what he is actually defining is first-order arithmetic.

Now, the "largest integer expressible uniquely by n symbols in first-order arithmetic" is indeed on the order of the order-\(\omega\) Busy Beaver function. But second order arithmetic is much, much stronger; it is measured by Turing hyperjumps, which are on a completely different level from the Turing jumps of first-order arithmetic. So I don't think we are even equipped to measure the strength of second-order arithmetic in terms of higher order Busy Beaver functions. And first order set theory is much, much stronger than second-order arithmetic, or even nth-order arithmetic for any n. I'm not sure how strong Goucher's combinatory logic is, but it doesn't seem to have the power of second order arithmetic. So I strongly believe that Rayo's function grows much, much faster than Goucher's Xi function.

After some time to allow for discussion, I will try to correct the wiki articles with the wrong information on Rayo's number. Deedlit11 (talk) 23:52, March 12, 2013 (UTC)

It took me over an hour to figure out what you were talking about here. Now I think I understand. FO arithmetic is allowed to quantify over sets of numbers, while FO logic is allowed to quantify over any sets (thus, for example, we can make statements about sets of real numbers). I think even second-order arithmetic will overcome Xi function.

I don't know very much about higher-order Turing jumps, but I know there is hierarchy of hyper-n-jumps for every order of arithmetics. If you are right, we'll really need new notation for such large ordinals! (provided such notation is possible!) LittlePeng9 (talk) 13:34, March 13, 2013 (UTC)

oh god FB100Z • talk • contribs 18:31, March 13, 2013 (UTC)

@LittlePeng9, I'm not aware of hyper-n-jumps for n > 1. Where did you hear about them?

Interestingly, while Turing jumps take you through the arithmetical hierarchy (the hierarchy for first order arithmetic), Turing hyperjumps do not in fact take you through the analytical hierarchy (the hierarchy for second order arithmetic). In fact, if S is a Delta-1-2 set, then the hyperjump of S is a Delta-1-2 set as well. So hyperjumps do not even take you out of Delta-1-2 sets, which is quite early in the hierarchy. Second order arithmetic is quite strong! Deedlit11 (talk) 21:31, March 13, 2013 (UTC)

Well, I'm not entirely sure where I heard about them; it may be unconfirmed information as well. And yes, SO arithmetic is very strong, that's why most people use restricted induction/comprehension - there is no ordinal notation known strong enough to measure strength of this system! LittlePeng9 (talk) 22:06, March 13, 2013 (UTC)

Goucher has agreed that, when quantification is over sets (which it is in the case of Rayo's function), Rayo's function will exceed his Xi function. So perhaps we can start removing references to Rayo's function being less than the Xi function or at the \(\omega_{\omega}^{CK}\) level of the fast-growing hierarchy. Deedlit11 (talk) 02:28, March 21, 2013 (UTC)

I think that if first order logic indeed can define fast-growing hierarchy, then Rayo's function must have order type \(\omega_1\) or above, since \(\omega_1\) is actually limit ordinal for the fast-growing hierarchy (which can't be defined without fundamental sequences). Ikosarakt1 (talk ^ contribs) 18:49, May 9, 2013 (UTC)

I don't even think that \(\omega_1\) function is possible. And first-order logic has only countably many sentences, so if we could somehow code functions in it there would be only countably many functions. Rayo's function can't be strictly stronger than diagonalization of all these functions, and diagonalizing through countably many countable ordinals gives still countable ordinal. Similar argument works for any consistent logic theory, so we can't find single consistent theory containing whole FGH. This doesn't hold for inconsistent theories, though. English language, for example, has no limit ordinal (as if it had, sentence "smallest order type larger than all provable ordinals is ordinal" would be provable). English is inconsistent, really. LittlePeng9 (talk) 19:24, May 9, 2013 (UTC)

In that case, I shall remove the sentence that FGH is probably definable in first order logic. Ikosarakt1 (talk ^ contribs) 08:47, May 10, 2013 (UTC)

You can define the FGH up to a given ordinal in first order logic, but to do so you need to define the ordinal. Of course, you can't define \(f_{\omega_1}\) using a fundamental sequence, since the fundamental sequence of \(\omega_1\) is uncountable - but you may be able to define a function for \(f_{\omega_1}\) that surpasses \(f_\alpha\) for all countable \(\alpha\). Whether or not it is possible to define the FGH up to \(\omega_1\) so that no function surpasses the entire hierarchy is independent of ZFC. Deedlit11 (talk) 01:10, May 11, 2013 (UTC)

Rayo's function - end of googology?[]

Is it possible to create a function growing faster than Rayo's function? I read there is a problem with ordinal notation to create a more fast-growing functions.Konkhra (talk) 10:41, March 15, 2013 (UTC)

Even though Rayo(n) is growing very fast asymptotically, I can't understand the size of this number without relations with other known functions. It would be nice to know on what values overtakes tetration, pentation, Ackermann function, ..., up to uncomputable functions such as \(\Sigma(n)\) or even \(\Sigma_2(n)\). Ikosarakt1 (talk ^ contribs) 11:14, March 15, 2013 (UTC)

Konkhra, there is no fastest growing function anyways. Take, say, Rayo(2n), Rayo(n^2), or even Rayo(Rayo(n)), Rayo(Rayo(Rayo(n)))), Rayoⁿ(n). Googology can't end because there are infinitely many numbers greater than Rayo's number. Ikosarakt1 (talk ^ contribs) 11:39, March 15, 2013 (UTC)

If I'm not mistaken, we can ask questions about largest integer nameable in 2nd order logic (by quantifying over finite formulas. LittlePeng9 (talk) 13:45, March 15, 2013 (UTC)

Yes, we could do that, and it should get us larger numbers. Another thing we could do is add a truth predicate to the language; this will allow us to define Rayo(n) within the language, so we get fundamentally larger numbers. We can add another truth predicate that tells us whether a formula within the stronger language is true, and iterate through the ordinals. So the question is, which is stronger, going to higher order logics, or iterating truth predicates? Deedlit11 (talk) 02:00, March 20, 2013 (UTC)

Second order logic is able to define first order truth predicate. Third order logic can define second order one etc. So higher order logic is at least as strong as iterated truth predicates, and I guess it's strictly stronger. LittlePeng9 (talk) 06:27, March 20, 2013 (UTC)

is it difficult get larger numbers with use 2nd order logic? I have never read of such numbers. These numbers have not yet created? Konkhra (talk) 05:09, March 22, 2013 (UTC)

What about taking advantage of type theory? I know loader.c has done some limited form of that. FB100Z • talk • contribs 06:40, March 22, 2013 (UTC)

This may work. Especially if we allow quantification over types. LittlePeng9 (talk) 17:26, March 22, 2013 (UTC)

Shall I break the world record if I define the function \(Ra(a,b)\) to be the largest number that can be expressed using a symbols in b-th order set theory, and then propose the number \(Ra(\text{meameamealokkapoowa oompa},\text{meameamealokkapoowa oompa})\)? Ikosarakt1 (talk ^ contribs) 15:55, March 22, 2013 (UTC)

Define \(b\)-th order set theory. FB100Z • talk • contribs 17:05, March 22, 2013 (UTC)

I don't know the exact definition, but we can replace it with b-th order logic. First order logic allows quantification over sets. Define by induction n+1-th order logic as extension of n-th order logic with quantification over formulas of n-th order logic (let's call them n-formulas).

Now a question - can we extend this definition transfinitely? \(\omega \)-th order logic would allow quantification over n-formulas for all (finite) n. Generally, \(\alpha \)-th order logic allows quantification over any \(\beta <\alpha \)-formulas. This definition may be vague or may cause inconsistency (but I don't think it does, it disallows self-quantification) but seems legit. LittlePeng9 (talk) 17:19, March 22, 2013 (UTC)

Based on what I've read, order-\(\omega\) logic is actually type theory... FB100Z • talk • contribs 18:20, March 22, 2013 (UTC)

Hmm, all the type theory systems I'm familiar with are computable, so they wouldn't generate functions faster growing than the Busy Beaver function. Wikipedia distinguishes logic from type theory, but perhaps there are type theory systems with comparable power. Deedlit11 (talk) 02:05, March 23, 2013 (UTC)

It looks like I need to read up on my metamathematics. Does anyone have any websites, books, etc. they recommend? FB100Z • talk • contribs 02:43, March 23, 2013 (UTC)

Well, I learned set theory from "Set Theory: An Introduction to Large Cardinals" by Frank Drake, and recursion theory from "Theory of Recursive Functions and Effective Computability" by Hartley Rogers. As for type theory, I've recently been reading this paper: http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf It's on the untyped lambda calculus, but it relates to typed systems. Deedlit11 (talk) 02:39, March 24, 2013 (UTC)

Okay, I'll scour the local library for those and related books. This is not the kind of stuff they teach me in high school, sadly... FB100Z • talk • contribs 05:58, March 26, 2013 (UTC)

Loader's number[]

I wonder how the output from loader.c compares to Rayo's number? --Ixfd64 (talk) 05:10, March 26, 2013 (UTC)

It's the output of a 512 character C computer program, so it's clearly less than BB_C (512), where BB_C is the Busy Beaver function for C programs. Note that BB_C(n) grows no faster than BB(n). I believe that BB(n) > BB_C(n), so Loader's number would be less than BB(512), and probably less than BB(100). Rayo's number is in a whole different universe. Deedlit11 (talk) 05:41, March 26, 2013 (UTC)

I see. I had initially expected it to be roughly comparable to BB(512), but this post led me to think it would be much larger. I guess it would probably be more in the neighborhood of TREE(3), etc. --Ixfd64 (talk) 16:24, March 26, 2013 (UTC)

@Deedlit11 If BB(n)<BB_C(n), then BB_C(512)>BB(512). You probably meant reverse inequality. All I know is that there exists number a, such that BB_C(a*n)>BB(n), because C is able to emulate TM. I think adding one state requires around 100 symbols, so a is around that large.

@lxfd64 I don't think it's that large. I guess it's expressable using \(\Gamma_0\) LittlePeng9 (talk) 16:40, March 26, 2013 (UTC)

You're right, I had the inequality reversed. I don't think there is a number a such that BB_C(a*n) > BB(n) - to describe a state of an n-state Turing machine requires O(log n) characters, so we need \(a n \log(n)\) characters to emulate an n-state Turing machine. So I imagine that BB(n) ~ BB_C(an log(n)).

Loader's number is much greater than TREE(3) or even SGC(13) - his function is not provably recursive in nth-order arithmetic for any n, so it corresponds to a very large recursive ordinal. Deedlit11 (talk) 23:22, March 27, 2013 (UTC)

perhaps Loader's number larger then SCG(SCG... (SCG(13))...) with for example googol nested functions? Konkhra (talk) 23:31, March 27, 2013 (UTC)

Yes, certainly. Iterating a function is just one level up the fast-growing hierarchy from the original function, so when you have two functions at significantly different ordinals, the faster one will still be faster than iterations of the slower one. Deedlit11 (talk) 00:08, March 28, 2013 (UTC)

Sorry, but I'm a little confused. Letting BB(n) ≈ BB_C(a * log(n)) suggests that the output would be around BB(167), assuming a ≈ 100 and that we're using the natural log. However, I'm having doubts that BB(167) would be larger than SCG(13). Or does the busy beaver function really grow so fast so early? --Ixfd64 (talk) 03:19, March 28, 2013 (UTC)

One thing I've learned about the busy beaver function — that f***er is fast. FB100Z • talk • contribs 06:39, March 28, 2013 (UTC)

That is, as Sbiis Saibian noted "that before you would reach BB(100) the resourcefulness of the human imagination would be overwhelmed". I'll agree him, there are \(\approx 1.889 \times 10^{521}\) TM's to verify, well over a centillion. Ikosarakt1 (talk ^ contribs) 12:56, March 28, 2013 (UTC)

Actually, that should be BB(n) ≈ BB_C(an * log(n)), there's a factor of n in there. Assuming the size of the largest output is proportional to the number of programs, we want x^x ≈ 128^y. Setting y = 512, we get x ≈ 412. I imagine that 400-500 states is a reasonable number of states to try to program a TM that computes SGC(n). But I suspect BB(n) passes SGC(13) _much_ earlier. It is hard to program a TM that gets any near the Busy Beaver function; for example, if you asked someone to program repeated exponentiation, I imagine it would take considerably more than 6 states, but a 6-state machine implementing repeated exponentiation was indeed found. It seems not unreasonable that BB(100) is larger than any number we have dreamt up using recursive processes. I certainly believe that about BB(1000). Deedlit11 (talk) 07:27, March 29, 2013 (UTC)

The problem is that there are a lot of TMs with chaotic behavior. Usually namely these machines are busy beavers. By the way, on the Robert Munafo's site I found the formula that generates lesser number of TMs than usual. Therefore, the number of 100-state TMs to verify (if we exclude the trivial ones) are about \(3.211 \times 10^{517}\). Even the number of them is much larger than the number of Planck volumes in the observable universe. Ikosarakt1 (talk ^ contribs) 11:22, March 29, 2013 (UTC)

Sorry, I had busy day, I made two fails. Yes, loader's number may indeed be that large, for then I thought about D(D(99)). I managed to write body to emulate TM in C++ (it shouldn't be far apart from C form). It needs 205 non-blank characters for body and at most 38+4log_10(s) characters to add new state (where s is number of states). If anyone is interested, I can post code on pastebin. LittlePeng9 (talk) 10:23, March 28, 2013 (UTC)

So we can state that the BB(167) is greater than SCG(13). in this case, the lower bound for BB(167) was found! Konkhra (talk) 00:06, March 29, 2013 (UTC)

Sorry, but this isn't rigorous proof. I found when BB_C is larger than BB, but to be sure we have to find strict inverse relation. Not to mention proving SCG(13)<BB_C(512), but that shouldn't be big problem. LittlePeng9 (talk) 07:07, March 29, 2013 (UTC)

Possible extension?[]

Variable assignments map the positive integers to sets. What about mapping the real numbers to sets? FB100Z • talk • contribs 22:41, March 29, 2013 (UTC)

My feeling is that it doesn't really matter. The variable assignments are restricted to the positive integers, but you still have the full power of set theory in your definition. If for some reason you can define a real number larger than any positive integer, it doesn't take that many more symbols to define the smallest integer larger than that real number. So if we let Rayo'(n) be Rayo's function except with variable assignments for real numbers rather than positive integers, we will have Rayo'(n) < Rayo(n+c) for a reasonably small c. Deedlit11 (talk) 02:40, March 30, 2013 (UTC)

Modification[]

Here is a trivial variation on Rayo's number. It removes parentheses and makes everything into Polish notation. (The spaces are for readability, they're not part of the string.)

∀R {
  {
    ∀[ψ], s: R([ψ],t) ↔ ([ψ] = "∈ i j"    ∧ t(xᵢ) ∈ t(xⱼ))
                      ∨ ([ψ] = "= i j"    ∧ t(xᵢ) = t(xⱼ))
                      ∨ ([ψ] = "¬ [θ]"    ∧ ¬R([θ], t))
                      ∨ ([ψ] = "∧ [θ] ξ"  ∧ R([θ], t) ∧ R([ξ], t))
                      ∨ ([ψ] = "∃ i [θ]"  ∧ ∃t′: R([θ], t′))
                      (where t′ is a copy of t with xᵢ changed)
  } ⇒ R([ϕ],s)
}

I find this to be slightly cleaner, but the growth rate is not affected by much. Like lighting a match and throwing it at the Sun.

Another less pointless change: what about adding a 'dereferencing' operator? Each element in the variable assignment would be indexed not by an integer but by any set in the Von Neumann universe. We add the line ∨ ([ψ] = "→ i" ∧ x_{x_i}) to the definition. Would this be too powerful? FB100Z • talk • contribs 01:35, April 25, 2013 (UTC)

Growth rate of Rayo's function[]

Can we say that for example Ra(10) is greater than BB(100) or BB(1000) or it is not known? Konkhra (talk) 10:13, May 5, 2013 (UTC)

Dubious - I don't think that it is possible to define \(\Sigma(n)\) with merely 10 symbols. Ikosarakt1 (talk ^ contribs) 10:24, May 5, 2013 (UTC)

Yes, Rayo's function has very slow start. In most formulations 0 is empty set, and this formula: (¬∃2(2∈1)) defines empty set. Also, no other set can be uniquely defined in 10 symbols. So Ra(10)=0<BB(100). LittlePeng9 (talk) 11:22, May 5, 2013 (UTC)

Quest can be harder: what is the smallest n such that \(Ra(n)>\Sigma(n)\)? Ikosarakt1 (talk ^ contribs) 13:00, May 5, 2013 (UTC)

Well, n you ask for must be pretty large. We need hundreds of characters to define useful recursion. Before that point best we can do is explained in article. Say we can define recursion with 500 characters in Rayo's micro-language. While BB(500) is unimaginably large, for Ra(500) we can hardly define multiplication. I guess smallest cross point of function is counted in millions, but that'll probably never be known for us. LittlePeng9 (talk) 13:33, May 5, 2013 (UTC)

Number of possible expressions[]

To prove the specific value of Ra(n), we need to sort out all expressions with n symbols. (Like we solve all \((4n+4)^{2n}\) TMs for \(\Sigma(n)\)). Through, how many these expressions for Ra(n)? This significantly depends on radix that we use. For example, if we use decimal, then string defining 0 is: (¬∃2(2∈1)) (10 symbols). Using unary, the string would look like that: (¬∃11(11∈1)) (already 12 symbols). Ikosarakt1 (talk ^ contribs) 13:48, May 5, 2013 (UTC)

As far as I know, every integer is counted as single number, so (¬∃2(2∈1)) has 10 symbols and (¬∃11(11∈1)) is, if we take both 1's separately, is invalid expression. There is infinitely many choices for each character, but we can filter finite number from this by noting that, say, ((2∈1)∧(3∈1)) is exactly same as ((3∈1)∧(2∈1)). So if we make assumption that for largest integer n used as variable every integer <n is also used number of such expressions is bounded, as n-symbol formula uses integers up to n. LittlePeng9 (talk) 14:29, May 5, 2013 (UTC)

It looks like for \(\text{Rayo}(n)\) you have at most \(\leq (7 + n)^n\) strings to search for. If we use Polish notation, we get rid of the parentheses and get \((5 + n)^n\).

We can even reduce it to \((4 + n)^n\) if we replace ¬ and ∧ with ⊼ (NAND). NAND is functionally complete. NOR works, too. FB100Z • talk • contribs 22:19, May 9, 2013 (UTC)

Furthermore, each <acronym title="first-order set theory">FOST</acronym> string names at most one positive integer. Let \(C(n)\) denote all the positive integers Rayo-nameable in \(n\) symbols or less, so that \(\text{Rayo}(n) = \max(C(n)) + 1\). There are at most \(\sum_{i = 0}^n (7 + i)^i\) strings, so \(|C(n)| \leq \sum_{i = 0}^n (7 + i)^i \leq n(7 + n)^n\). FB100Z • talk • contribs 23:04, May 9, 2013 (UTC)

There seem to be two ways to evaluate these types of functions. The first is to loop through all possible expressions, and the second is to build expressions of your own. In this case, the first solution seems nigh impossible. The second is fairly productive; it's not hard to show that Rayo's number >> 10^50. FB100Z • talk • contribs 20:08, May 5, 2013 (UTC)

Yes, but the second way allows us only to give lower bound for Ra(n), because we're not sure that our own expression will be the solution. Ikosarakt1 (talk ^ contribs) 08:46, May 10, 2013 (UTC)

Symbols[]

Anyone know, or know where I can find the complete list of symbols that can be used in rayo's function?

I'm going to try and make some kind of lower bounds (smallest number of symbols needed to define n)

I'll assume for now that they're the same as 1st order logic. DrCeasium (talk) 13:04, June 23, 2013 (UTC)

From the article:

Rayo defined a very specific and abstract micro-language for describing how a formula works:

"a∈b" means that the ath member of the sequence is an element of bth member of the sequence.

"a=b" means that the ath member of the sequence is equal to the bth member of the sequence.

"(¬e)", for formula e, is the negation of e.

"(e∧f)", for formulas e and f, indicates the logical and operation.

"∃a(e)" indicates that we can modify the ath member of the sequence such that the formula e is true.

Ikosarakt1 (talk ^ contribs) 13:44, June 23, 2013 (UTC)

So we have: member symbols (these representing which set is considered), 2 parentheses, ∈, =, ¬, ∧ and ∃. LittlePeng9 (talk) 14:03, June 23, 2013 (UTC)

OK, thanks. I wasn't sure whether those were the only symbols or not. Anyone got any ideas how you could force an expression to evaluate more than once, and so get recursion? DrCeasium (talk) 14:11, June 23, 2013 (UTC)

Hold on. The rules given mean that there can only be one statement in the definition of rayo(n), and defining recursion in a single statement is impossible isn't it, because the whole thing will either evaluate once, and could be comparable to a formula x=8+5×27, or an infinite number of times, and would be comparable to a formula like x=x+1?

This could be solved by allowing a new symbol to end an expression, for example a comma, and allow the naming of formulae. Then it becomes easy to make recursion. DrCeasium (talk) 14:31, June 23, 2013 (UTC)

Rayo's first order language isn't programming language. We can't add two sets. There is no obvious way to define number. Take a look at definition of 0: (¬∃1(1∈2)). We just say that there is no set contained in 0. For 1, we just say that 0 is in it and nothing else is. It's just like formulas in ZFC - this isn't obvious that they can define some sort of recursion, but they do. LittlePeng9 (talk) 14:46, June 23, 2013 (UTC)

As countable ordinals get larger and larger, googological notations become less and less obvious. Ikosarakt1 (talk ^ contribs) 18:21, June 23, 2013 (UTC)

Are there any examples of recursive set theory statements anywhere? DrCeasium (talk) 14:57, June 23, 2013 (UTC)

Oh, so defining recursion is not as easy as I was assuming it was. Has anyone figured out how to define recursion yet? Tomtom2357 (talk) 06:07, June 24, 2013 (UTC)

What do we do about the contradictory statements like: ¬∃2(¬2∈1∧¬2∈2)∧¬∃2(2∈1∧2∈2) (russel's paradox, set of all sets that do not contain themselves)? Do we say that this statement has no "good" variable assignment, because it gives a contradition? I think that would be the best way to deal with paradoxical sets. Also, I don't think ¬1∈1∧¬∃2(¬2∈1∧¬2∈2∧¬2=1)∧¬∃2(2∈1∧2∈2), and 1∈1∧¬∃2(¬2∈1∧¬2∈2)∧¬∃2(2∈1∧2∈2∧¬2=1) are contradictory, so not allowing unrestricted comprehension might have it's downsides. Tomtom2357 (talk) 07:21, June 24, 2013 (UTC)

No need to worry about whether the statement is contradictory; for no number assigned to 1 is the statement satisfied, so the statement does not define a number, simple as that. Deedlit11 (talk) 09:39, June 24, 2013 (UTC)

Oh, okay, that was easy. Tomtom2357 (talk) 09:47, June 24, 2013 (UTC)

If we take ZF(C) as our basis, via axiom of foundation and restricted comprehension we avoid all paradoxical sets (as far as ZF(C) is consistent) by saying that any such set can't exist. LittlePeng9 (talk) 11:50, June 24, 2013 (UTC)

Well, I don't like that way, because it excludes some sets that might be useful. Deedlit11 gives a good way to do it, his way leaves in all non-paradoxical sets. Tomtom2357 (talk) 13:48, June 24, 2013 (UTC)

Is ZFC stands for Zermelo-Fraenkel set theory? Why not ZFST? Ikosarakt1 (talk ^ contribs) 13:27, June 24, 2013 (UTC)

ZF denotes Zermelo-Fraenkel set theory without axiom of choice, ZFC stands for same theory with axiom of choice. ZF(C) is sometimes used to denote "with or without choice". LittlePeng9 (talk) 13:31, June 24, 2013 (UTC)

Rayo's Number vs Aarex's Number[]

How to compare Rayo's Number and Aarex's Number? Aarex^Tiao 16:30, July 7, 2013 (UTC)

Rayo's number still seems to be unbeaten. LittlePeng9 (talk) 17:06, July 7, 2013 (UTC)

Any function that diagonalizes from the Xi function is unlikely to pass Rayo's function. Tomtom2357 (talk) 04:26, July 8, 2013 (UTC)

If we shall diagonalize it indefinitely long, we shall get a function which grows faster than Rayo's one. Ikosarakt1 (talk ^ contribs) 09:52, July 8, 2013 (UTC)

Actually, Aarex dropped Xi function after 4th Aarex function, now he uses arbitrarily chosen \(f_{\phi^\text{CK}(\omega, 0)}\). LittlePeng9 (talk) 10:09, July 8, 2013 (UTC)

The sixth Aarex function (and thus the sixth Aarex number) is an array notation based on \(f_{\phi^\text{CK}(\omega, 0)}\), where \(\phi^\text{CK}\) is a Veblen hierarchy based on \(\alpha \mapsto \omega_\alpha^\text{CK}\). I'll bet you dollars to donuts that \(\phi^\text{CK}(\omega, 0)\) comes nowhere near the ordinal describing Rayo's function. FB100Z • talk • contribs 04:53, July 8, 2013 (UTC)

Will I get a donut if I program Aarex function in FOST? LittlePeng9 (talk) 06:20, July 8, 2013 (UTC)

A very, very nice donut. Zwischenzug 10:43, July 8, 2013 (UTC)

Jelly-filled if you can program Rayo's function in FOST. FB100Z • talk • contribs 04:26, July 10, 2013 (UTC)

Uh oh, if we can define Rayo's function in FOST, then it will mean that this function is undefined. Actually, it might be possible to do it, because all we have to do is code the symbols and find the one that names the biggest number. What do we do if Rayo's function turns out to not be well-defined? Tomtom2357 (talk) 08:00, July 10, 2013 (UTC)

It would look as though Rayo's function could be defined in Rayo's function. However, this shouldn't make the function not well defined because if Rayo(10^100) can define Rayo(10^100)+1, then that would make that specific statement have an infinite value, discaulifying it from being Rayo's number. Because there is only a finite number of possible statements in set theory, then that would mean that there should still be a finite number of possible values, which would be either finite or infinite, so it should still work. DrCeasium (talk) 08:13, July 10, 2013 (UTC)

Oh, okay, that makes sense. Tomtom2357 (talk) 01:36, July 11, 2013 (UTC)

Wait a minute, as soon as you use \(\alpha \mapsto \omega_\alpha\), you can't use the fast growing hierarchy, because the ordinals are uncountable.

CK superscript means we are dealing with countable (mostly) nonrecursive ordinals. Of particular interest there are admissible ordinals. LittlePeng9 (talk) 12:52, July 8, 2013 (UTC)

Yeah, I didn't see the CK superscript. Tomtom2357 (talk) 14:18, July 8, 2013 (UTC)

derp, whoops, yes, there should be a CK there. FB100Z • talk • contribs 00:39, July 9, 2013 (UTC)

Ok, it makes sense now. Tomtom2357 (talk) 01:52, July 9, 2013 (UTC)

Rayo's ordinal[]

How the ordinal I defined at the end of my subpage compares to Rayo's ordinal? Ikosarakt1 (talk ^ contribs) 09:38, August 20, 2013 (UTC)

To be honest - I have no slightest idea. I'm not sure what exactly you consider "recursive extension", but resulting ordinal may be greater than Rayo's ordinal. LittlePeng9 (talk) 10:47, August 20, 2013 (UTC)

Defining the recursive extension in general is the problem which doesn't lets me to get much past recursive ordinals. I don't know how to define even \(\omega_1^\text{CK}[n]\) formally, although I know that we just need to add more and more recursive diagonalizators like \(\Omega\), I and \(M_\alpha\) inside ordinal collapsing functions. Ikosarakt1 (talk ^ contribs) 14:04, August 20, 2013 (UTC)

We can formalize some enumeration of Turing machines, Kleene's O is then also easily formalizable. Method used to find fundamental sequence for CK ordinal is thus fairly formal. If you want to get it using diagonalization, method concerning this would be incredibely complicated, very likely beyond our current understanding of these methods, as it would be non-recursive itself, so according to Church Turing thesis impossible to do in physical universe. LittlePeng9 (talk) 17:41, August 20, 2013 (UTC)

We can represent fundamental sequence to \(\omega_1^\text{CK}\) as some ordinals in the form \(\theta(A_1)\), \(\theta(A_2)\), \(\theta(A_3)\) so that each \(\theta(A_m)\) is some indexed-diagonalization symbol like \(\Omega_\alpha\), \(I_\alpha\) and \(M_\alpha\). Each new diagonalization symbol can't be used until the power of all previous diagonalizators will be exhausted. Ikosarakt1 (talk ^ contribs) 19:28, August 20, 2013 (UTC)

Yes, I can agree with this, but we then need very complicated definitions, very likely expressible only in infinitary logic. Also, note that notations Deedlit once explained don't use only \(I_\alpha\), but also \(I(1,0)\) and similar, so this isn't only that we have to define symbols \(\Omega,I,M\). LittlePeng9 (talk) 19:53, August 20, 2013 (UTC)

Maybe Deedlit knows Konkhra (talk) 13:22, August 20, 2013 (UTC)

First undefinable ordinal[]

To me, \(\omega_1^\text{DEF}\) seems the most likely candidate for an ordinal describing the function's growth rate. Can we do anything to investigate this guess? FB100Z • talk • contribs 19:19, November 1, 2013 (UTC)

I don't think so, I believe there exists formal system able to define FOST in it. If that's true, Rayo's ordinal is strictly smaller than \(\omega_1^\text{DEF}\). LittlePeng9 (talk) 22:09, November 1, 2013 (UTC)

Oh, wait, I forgot \(\omega_1^\text{DEF}\) is about defining in FOL. In that case, that might be true. LittlePeng9 (talk) 22:11, November 1, 2013 (UTC)

I don't know what FOL is, so I think that the more interesting milestone is the first undefinable ordinal namely in the sense of all formal systems. Ikosarakt1 (talk ^ contribs) 10:48, November 2, 2013 (UTC)

FOL - first-order logic. LittlePeng9 (talk) 11:31, November 2, 2013 (UTC)

Of course I know what that abbreviation is. The problem is that I don't get how we are able to define truly large ordinals (particularly non-recursive) using only four logical operations which almost everyone learned in school. Also, why this logic is first-order? What's the second order logic and beyond? Ikosarakt1 (talk ^ contribs) 11:41, November 2, 2013 (UTC)

Rayo's number uses first order set theory, not first order logic. In here I gave examples of how to implement TM and SKIO in set theory.

About your question - second order logic can quantify over predicates. Predicate may be true or false depending on "input". For example, \(P(x)\iff x<5\) is predicate. Now, \(\forall P:P(0)\implies(\exists x:P(x))\) is second order formula, which happens to be true. LittlePeng9 (talk) 14:03, November 2, 2013 (UTC)

Fish number 7 discussion continued[]

(As FB100Z suggested I move our discussion to talk page)

I have no doubts we can add oracles and create hierarchies, but look at analogy with TMs: we can add oracles transfinitely far, but it's incredibely hard to reach Goucher's ordinal.

Goucher's ordinal is first fixed point of a->w_a^CK. It is known that Xi is at least as strong as Goucher's ordinal, and FOST is beyond Xi. What you probably mean (and should have point out) is that you go for Goucher's ordinal in your hierarchy.

We can define operation of adding truth predicate, analoguous to adding oracle, which will be even stronger than your oracles.

I believe Deedlit meant undefinability of Rayo's function within FOST. LittlePeng9 (talk) 06:18, November 4, 2013 (UTC)

I agree with Deedlit that Kyodaisuu's variant is a little disappointing. Sure, it boosts Rayo's function, but it does little to enhance the underlying logic.

@Deedlit, what's Tarski's theorem? I Wikipedia'd it and I don't see how the result relates to the topic at hand.

The undefinability of Rayo in FOST is a huge surprise to me. And since this is math we're talking about here, the first thing I will try to do is prove it wrong! FB100Z • talk • contribs 07:38, November 4, 2013 (UTC)

Link to original discussion. If we can generalize the operation of adding oracles, by some means such as adding truth predicative, that would be interesting, far more interesting than my work of just making Rayo hierarchy. Then what next? If you enhance the formal system by adding a truth predicative, another Rayo function can be defined to that new system. That another Rayo function cannot be implemented in that system, so we go on to adding oracle or adding higher level of "predicator of predicator" or something? Then we can make hierarchy for such operation of adding new predicators. Anyway, once we define something, we can always make hierarchy. That is the underlying logic of Fish number 7. Kyodaisuu (talk) 08:00, November 4, 2013 (UTC)

All very true. As we've seen with many googological systems, you can always extend it into an ordinal hierarchy. Buchholz hydras come to mind. Of course, the best thing to do after that is to just abandon the entire system and move on to a far stronger one. FB100Z • talk • contribs 08:05, November 4, 2013 (UTC)

@FB100Z, Tarski's undefinability theorem states that it is impossible to make a first-order truth predicate T(x) (for x being some encoding of first-order formulae, e.g. Godel's encoding into naturals) such that T(x) is true iff formula corresponding to x is true. This doesn't directly imply that implementing Rayo's function is impossible, but definitely shows that this isn't as obvious as I thought.

This generalizes simply to systems stronger than FOL. For logical system L let L+ denote system L together with truth predicate for system L. We can create hierarchy (even though it's a bit ad hoc) by continuing following sequence transfinitely: FOL, FOL+, FOL++, FOL+++,... each with new truth predicate for previous system. We can deal with limit ordinals by adding 2-var truth predicate T(n,x) where n tells us which truth predicate we use.

Even stronger way to increase numbers is to use higher-order logic/set theory (quantification over predicates). SOL contains FOL, FOL+, FOL++ etc., and possibly even reaches quite far in transfinite part of sequence. TOL (3rd-order) contains SOL, SOL+, etc. and HOL contains all of these. I'm not quite sure if there exist transfinite order logics/set theories. From what I was told \(\omega\)-th order logic is parallel to type theory.

So yeah, we have many methods of going beyond Rayo's number, much more elegant than oracles. LittlePeng9 (talk) 14:41, November 4, 2013 (UTC)

This is really interesting. It seems to me that adding truth predicative is just as same as adding an oracle. Predicative is better than oracle because it is more primitive operation, looks smart, and it is widely accepted or accustomed way of extension in set theory. FOL=R[1], FOL+=R[2], FOL++=R[3], ... and this extends to R[ω]. I don't understand the part of adding 2-var truth predicate. How strong is T(n,x)? Does it exceed R[Goucher's ordinal] of my hierarchy definition? Kyodaisuu (talk) 15:13, November 4, 2013 (UTC)

I'm pretty sure truth predicate is stronger than oracle. I think it's pretty straightforward that we can compute Rayo's function thanks to truth predicate, but I can't see how we can derive truth of the formula by knowing how big number it can output.

Two variable truth predicate was my idea to extend it transfinitely (to make it "hierarchy"). For example, if T1(x) is truth predicate for FOL, T2(x) is for FOL+ etc. then T(n,x) works like Tn(x). With some work I'm sure we can extend this further. I dunno how it compares to R[something]. LittlePeng9 (talk) 15:57, November 4, 2013 (UTC)

I think that a point of truth predictate is that it can solve halting problem. As we discussed, we might be able to write Rayo function in FOL, but it cannot be implemented in FOL because it makes contradiction, and that is why we introduced oracle. In the same way, if we introduce predicate, we can compare the Rayo function written in FOL inside FOL+, just because we added another symbol to FOL and made it another system, avoiding contradiction. This kind of "adding another symbol to a system" seems to be all the same, regardless of adding predicative or oracle. Actually I can guess that essentially they are doing the same thing. If you compare oracle and +, there may be some diffence in, for example, characters needed to express Rayo^10(10^100), but that difference is not very important, and therefore we can say both system of adding oracle and adding predicate are in the same order. Kyodaisuu (talk) 16:13, November 4, 2013 (UTC)

And for T(n,x), I now understand it because you were trying to make a hierarchy, which means that n is ordinal. In that way, n has a ceiling point of somewhere like Goucher's ordinal (G), so T(G,x) = R[G] in my definition. Kyodaisuu (talk) 16:31, November 4, 2013 (UTC)

First, there is no halting problem for logical systems. We can only talk about problem of deciding truth of sentence.

After some thought, we can't create Rayo's function, as that might be impossible without truth predicate.

Yes, I admit adding truth predicate can be considered analoguous to oracle, as we just add another symbol.

I'm pretty sure truth predicate is much stronger than oracle, as we can derive oracle from predicate, but I believe not vice versa.

I agree hierarchies have meeting point, even though in comparison Goucher's ordinal would be nothing. And even though they meet, T(n,x) creates much stronger systems below that meeting point. LittlePeng9 (talk) 17:04, November 4, 2013 (UTC)

You are right. Oracle can be derived from predicator, and predicator cannot be derived from oracle. Therefore, oracle cannot be stronger than predicator. In order to show that predicator is stronger than oracle, it has to be shown that predicator can work stronger than defining Rayo(n). I think most important work of predicator is to decide Rayo(n), and no more important work remains. This is just my guess and I may be wrong. Kyodaisuu (talk) 17:26, November 4, 2013 (UTC)

Well, we already have that result. System L is strictly stronger tham system M is L can formulate all the things M can and something more. FOST+ can define oracle, so it can do everything R[2] can. But it can also formulate truth predicate (trivially) and R[2] can't (as we agreed), so FOST+ is strictly stronger than R[2]. LittlePeng9 (talk) 17:56, November 4, 2013 (UTC)

I see. Now I understand predicator is stronger than oracle. Kyodaisuu (talk) 18:14, November 4, 2013 (UTC)

LittlePeng9: I've made an oracle extension which strength Gouchers ordinal Wythagoras (talk) 18:27, November 4, 2013 (UTC)

From this discussion, it seems that we are finally approaching a truly "natural" extension of not just Rayo's function, but FOST itself. This is my proposal for the extension FOST*:

∈ab: variable a is a member of variable b.
∃ae: variable a can be changed so that expression e is true.
⊼ef: expression e and expression f are not both true (logical NAND).
Ta: variable a, interpreted as a formula, is a true predicate for all possible variable assignments.

How powerful is this? Since each expression plugged into the T operator can itself be a FOST* string, I suspect that this is far more powerful than FOST+. FB100Z • talk • contribs 20:19, November 4, 2013 (UTC)

Ouch, I feel like it will cause some inconsistency. I'm pretty sure there will exist formula F of form ⊼TaTa such that it's encoding is a. Such formula states it's own falsity, and it's existence follows from (I believe) Godel's diagonal lemma. LittlePeng9 (talk) 20:47, November 4, 2013 (UTC)

Oh, totally. Just like what happens when we introduce an oracle to SKI calculus (and indeed, I'll guess that SKI:SKIO::FOST:FOST*). Do the inconsistencies impact how well-defined Rayo's function is? FB100Z • talk • contribs 21:14, November 4, 2013 (UTC)

Also, I'm going to take a wild stab and guess that the ordinal strength of the resulting Rayo-function (assuming it's defined) is the first fixed point of \(\alpha \mapsto \omega_\alpha^\text{DEF}\), or R[R[R[...]]] in an extension of Kyodaisuu's notation. Of course, we don't yet know what \(\omega_\alpha^\text{DEF}\) means for \(\alpha\) other than 1 :P FB100Z • talk • contribs 21:32, November 4, 2013 (UTC)

Inconsistency in FOST* causes existence of neither true or false sentences. We can seed them out by giving each formula a rank and taking values only from formulas with rank (sounds familiar?). This way we can get massive numbers with no doubts if they are well-defined. At least, I hope so. LittlePeng9 (talk) 21:48, November 4, 2013 (UTC)

Why can't we just ignore the inconsistent formulas? FB100Z • talk • contribs 21:51, November 4, 2013 (UTC)

We can, and giving ranks easily tells us which formulas might be inconsistent. LittlePeng9 (talk) 22:15, November 4, 2013 (UTC)

Ah, I see. So I guess we definitively have a strong variant of the Rayo function now. Whee. FB100Z • talk • contribs 22:37, November 4, 2013 (UTC)

Great! By the way, the reason that FOST+ is stronger than R[2] is that FOST does not have predicator. Beyond this level, introducing another symbol of predicator and introducing oracle is exactly the same. Introducing oracle in FOST* will make FOST**, and introducing another symbol of T will also make FOST**. What we need is just FOST* and FOST** is guaranteered to be a different system. Kyodaisuu (talk) 09:45, November 5, 2013 (UTC)

How do you think FOST** will be stronger than FOST*? If it adds "universal truth predicate" then it gives us nothing, because T in FOST* can do exactly same job. Same with oracle. So FOST**=FOST*. LittlePeng9 (talk) 15:18, November 5, 2013 (UTC)

We already did that discussion. FOST* has universal truth predicatives, but it cannot make Rayo function of itself, because if it writes Rayo(Rayo(10^100)) of FOST* in 10^100 characters it will cause contradiction, it doesn't specify any number, and it is excluded. The reason that FOST** is stronger than FOST* is that it is just different system. FOST** can write Rayo function of FOST*, just because it is different system and make no contradiction. Same as oracle. Kyodaisuu (talk) 15:24, November 5, 2013 (UTC)

Ah, I see now. Adding truth predicate actually does nothing, but adding oracle does. It is because now we can sieve out paradoxal/contradictory formulas. But we can add "super-predicate" which would tell us if given combinator is paradoxal or not (in parallel to Ω_2 combinator for SKIΩ). This will be certainly even stronger than oracle. LittlePeng9 (talk) 15:40, November 5, 2013 (UTC)

It is a simple story. No matter how strong the formal system is, you cannot write Rayo function of formal system A inside formal system A effectively, because it makes contradiction. Even if you introduce super-predicative, you cannot write Rayo function of that system inside the system, but of course it will get stronger than having no super-predicative, and therefore we can start from the system with super-predicative. In order to effectively write Rayo function of formal system A, we need to have another formal system B. Easiest way is to introduce a new operator, but we don't even need a new operator, if we can distinguish between the formal systems. Kyodaisuu (talk) 15:56, November 5, 2013 (UTC)

You are essentially describing a case of Gödel incompleteness. No matter how strong a system you create, you can always find a flaw that allows the creation of a more powerful system. Adding 1 ensures that large numbers will never end, and similarly incompleteness ensures that large number functions will never end. FB100Z • talk • contribs 02:20, November 6, 2013 (UTC)

That's right. Therefore (1) Make a strong formal system (2) Make a hierarchy out of it is a general way of making stronger function. Next step is to make a formal sytem which can create and update formal systems. I am wondering if we can do that work with SOL, by using the expression of ∃Rφ and ∀Rφ in the description of Wikipedia. I don't understand how these expressions work. Kyodaisuu (talk) 12:48, November 6, 2013 (UTC)

Gödel's incompleteness theorems aren't quite about that. It's Tarski's theorem which gives us this result. As far as I know, no formal system can tell us what formal system is (because it might lead to contradiction or something). ∃Rφ and ∀Rφφ". LittlePeng9 (talk) 16:06, November 6, 2013 (UTC)

Okay, so it may not be Godel incompleteness, but it sure feels like it :P FB100Z • talk • contribs 21:40, November 6, 2013 (UTC)

I would like to summarize our discussion.

Formal system L is stronger than formal system M when L can formulate all the things M can and add something more.
Stronger formal sytem will result in stronger Rayo function.
To make FOST stronger, we can add predicative (FOST+ or FOST*) and super-predicative. Going to Second-order logic and higher-order logic might also make the formal system stronger, but we do not know how we can proceed to that level yet.
Once we get a strong formal system, we can always make a hierarchy from that formal system. The hierarchy can be constructed with oracle, like Fish number 7, but it doesn't have to be oracle.
Once we make hierarchy, there exists a upper limit of some ordinal, where we cannot reach by hierarchy definition. Kyodaisuu (talk) 13:07, November 6, 2013 (UTC)

Once again, this meeting point will almost certainly won't be Goucher's ordinal. LittlePeng9 (talk) 16:06, November 6, 2013 (UTC)

I see. I edited the summary. Kyodaisuu (talk) 16:11, November 6, 2013 (UTC)

We can express that ordinal to be the first ordinal that we can never reach by hierarchy definition, so "strongest function that we can ever make" may not be a good expression, because it seems like we can reach there. Once we "reach", we can always exceed it, but we can not reach the ordinal and that is why we cannot exceed it. I changed the expression. Kyodaisuu (talk) 16:21, November 6, 2013 (UTC)

Type theory[]

According to what I read, type theory is extremely strong. I speculate that we'll get a very powerful uncomputable variant of Loader's function if we apply it to sets rather than numbers. Thoughts? FB100Z • talk • contribs 21:40, November 6, 2013 (UTC)

Second-order set theory[]

I finally managed to convince myself that maybe SOST (second-order logic using the ∈ operator and the Von Neumann universe as the domain of discourse) is stronger than FOST (first-order logic using the ∈ operator and the Von Neumann universe as the domain of discourse). Recall that first-order logic allows quantification over elements of the domain, but second-order logic also allows quantification over sub-collection of the domain. V is not a set, but a proper class, and therefore its sub-collections are classes (but none of its elements are). The advantage of SOST is that it lets us use proper classes as well as sets. Is this reasoning sound? If so, does the conclusion make Rayo's function any stronger? FB100Z • talk • contribs 21:11, November 4, 2013 (UTC)

Let me just paste links for wikipedia pages regarding this topic for reference: First-order logic, Second-order logic, Higher-order logic, Type theory . Kyodaisuu (talk) 21:55, November 4, 2013 (UTC)

(note that the terms "first-order set theory" and "second-order set theory" are not in wide use by professional mathematicians; they appear to be coined by Rayo himself FB100Z • talk • contribs 22:56, November 4, 2013 (UTC))

Don't take my word on that, but I think strength of SOL comes from that it can quantify over predicates of form P(x). But for every predicate there is (via I believe axiom of comprehension) a proper class containing these and only sets x for which P(x) holds. Btw, sets are also classes, but they are "small" classes. LittlePeng9 (talk) 22:02, November 4, 2013 (UTC)

It gets interesting because there are subgenres within SOL. "Monadic SOL" doesn't let us quantify over multivariable functions, but "full SOL" does. But when we try to apply this to SOST, they're merged since we can easily condense two variables into one using the definition of the ordered pair. This kind of reasoning initially led me to believe that SOST and FOST were equal because relations already exist within our domain of discourse (but the distinctions between proper classes and sets made me rethink that). In general, using the Von Neumann universe as the domain opens up a lot of curious properties — even the weakest of the systems (FOST) is incredibly powerful.

Since SOL can quantify over predicates, I venture a guess that either SOST = FOST+ or SOST = FOST*. The former seems more likely to me. FB100Z • talk • contribs 22:50, November 4, 2013 (UTC)

I wonder if we can express FOST++, FOST+++, …, T(n,x), and so on, in SOST or not. If SOST can write an expression like "largest namable number in m kinds of predicate symbol FOST in n characters", that will be in the level of T(ω,x). If we can have SOST expression of transfinite induction or make hierarchy of the operation of adding predicate in FOST, we can go to higher ordinal of T(n,x). If "quantify over predicates" means something like that, we might be able to do that, but I don't know how to construct such SOST expression. Kyodaisuu (talk) 00:06, November 5, 2013 (UTC)

(disclaimer: i am not, and do not claim to be, any kind of expert in metamathematics and logic. i shoot my mouth off about it in hopes that i will be proven wrong and properly educated. FB100Z • talk • contribs 09:03, November 6, 2013 (UTC))

Infinite length FOST[]

Can we take the FOST syntax tree and extrapolate it to countable ordinal sizes? Or am I just crazy? FB100Z • talk • contribs 18:47, November 21, 2013 (UTC)

I think you're becoming insane. But still, nothing is impossible before someone proves it is :P LittlePeng9 (talk) 19:32, November 21, 2013 (UTC)

Huh, it looks like this has already been done. I guess I'm no less batshit than some logicians!

The next question is whether infinitary logic can be applied to Rayo's function. FB100Z • talk • contribs 20:23, November 21, 2013 (UTC)

Oh, yeah, I forgot about infinitary logic. The problem for Rayo's function for this system is similar to why there is no busy beaver function for IITMs. However, we can speak of supremum of ordinals definable by some subset of infinite FOST formula, e.g. let F(n) be supremum of ordinals definable by FOST formula, which can be defined in \(\Pi^1_n\). LittlePeng9 (talk) 21:21, November 21, 2013 (UTC)

There is indeed a busy beaver function for ITTMs, namely \(\lambda[n]\). Of course, it produces ordinals instead of natural numbers, so to get a googological function we just plug it into FGH: \(f_\lambda(n)\). We can do the same for infinitary logic. FB100Z • talk • contribs 06:36, November 22, 2013 (UTC)

Hierarchy definition like Fish number 7 can be defined only for ordinal having fundamental sequence. If infinitary logic can be defined with ordinals having no fundamental sequence, upper limit ordinal might exceed the hierarchy definition. I am not sure if sound definition is possible to specify a finite number in that case. If infinitary logic can be applied only to ordinals with fundamental sequence, maybe it is similar to the level of hierarchy definition. Kyodaisuu (talk) 16:57, November 22, 2013 (UTC)

Every countable ordinal has fundamental sequence. Note, that \(\lambda,\zeta,\Sigma\) are all countable, just like ordinal F(n) I suggested for infinite FOST. LittlePeng9 (talk) 19:28, November 22, 2013 (UTC)

Tsk, tsk! You mean every countable limit ordinal has a fundamental sequence. FB100Z • talk • contribs 20:08, November 22, 2013 (UTC)

Derp, yes, of course, that's what I meant. LittlePeng9 (talk) 21:22, November 22, 2013 (UTC)

I see, so even Church-Kleene ordinal has fundamental sequence (I was misunderstanding this). A countable limit ordinal has a way to map to a set of \(\omega\), which means that it has a fundamental sequence. Kyodaisuu (talk) 21:07, November 22, 2013 (UTC)

Yes, CK has a fundamental sequence, although any valid fundamental sequence for the ordinal is uncomputable. FB100Z • talk • contribs 20:02, November 23, 2013 (UTC)

It worries me that we have an uncountable number of expressions to deal with. Are all countable ordinals definable in infinitary logic?

If it turns out that infinitary logic does work, how does infinitary set theory compare to second-order set theory? The fact that we're using the Von Neumann universe distorts things quite a bit. FB100Z • talk • contribs 20:01, November 22, 2013 (UTC)

Variable is uncountable, but FOST expression is countable. Kyodaisuu (talk) 21:09, November 22, 2013 (UTC)

Every countable ordinal can be defined my infinitary logic. Here I defined a mapping which can be translated to definition of ordinal. I also believe infinitary logic is way stronger than higher order logics. LittlePeng9 (talk) 21:22, November 22, 2013 (UTC)

Hmm, most of my sources have told me that infinitary logic is actually weaker than second-order logic (!). Maybe you're working on a different definition of infinitary logic. I will do further research on this. FB100Z • talk • contribs 20:02, November 23, 2013 (UTC)

I hope it's obvious why infinitary logic outgrows FOL (expressions don't have to be infinite). Definition I know about allows disjunction, conjunction and quantification over infinitely many variables. So I think we can implement, say, existential quantificator over predicates by infinite disjunction over all predicates, which would give us strength of at least SOL. Similarily, I think, we can outgrow HOL. LittlePeng9 (talk) 21:25, November 23, 2013 (UTC)

Okay, that makes sense. Can we get a definition for infinitary Rayo for formality's sake? FB100Z • talk • contribs 21:45, November 23, 2013 (UTC)

Infinite Length FOST = Rayo(infinity) —Preceding unsigned comment added by Googleaarex (talk • contribs)

What the hell? There are so many things wrong with that "equation," I don't even know where to start. FB100Z • talk • contribs 20:02, November 23, 2013 (UTC)

Nuff said it contributes nothing to disscusion. LittlePeng9 (talk) 21:25, November 23, 2013 (UTC)

RGH[]

RGH is same at FGH, but faster.

\(r_0(n)\) = \(Rayo(n)\)
\(r_{m+1}(n)\) = \(r^n_m(n)\)
\(r_\alpha(n)\) = \(r_{\alpha[n]}(n)\)

Rayo_2(n) = r_{Growth Rate of Rayo() Function}(n) Aarex^Tiao 00:12, December 20, 2013 (UTC)

Really faster, \(r_{\alpha*m}(n) = f_{\alpha*(m+1)}(n)\) if you should look closer. Ikosarakt1 (talk ^ contribs) 07:50, December 20, 2013 (UTC)

This is just an offset version of FGH. FB100Z • talk • contribs 08:03, December 20, 2013 (UTC)

To be exact, if \(\gamma\) measures strength of Rayo's function, then \(r_\alpha=f_{\gamma+\alpha}\). Hierarchies catch up on \(\gamma \cdot\omega\), after which they are the same. LittlePeng9 (talk) 11:56, December 20, 2013 (UTC)

Of course, by "equal" I mean "with comparable rates of growth. LittlePeng9 (talk) 11:57, December 20, 2013 (UTC)

Eureka[]

Rayo's number is 617-253-2559. you're.so.pretty! 04:29, May 17, 2014 (UTC)

I see what you did there :) LittlePeng9 (talk) 07:11, May 17, 2014 (UTC)

How 617-253-2560 compares to Rayo's number then? And what notation you used? Ikosarakt1 (talk ^ contribs) 07:20, May 17, 2014 (UTC)

Well, 617-253-2560 is not Rayo's number, that's one of very few meaningful answers I can give. LittlePeng9 (talk) 07:46, May 17, 2014 (UTC)

Ikosarakt, it is a joke, but is true. Maybe search for 617-253-2559 on the internet? Wythagoras (talk) 08:53, May 17, 2014 (UTC)

Sorry, I haven't thought about it. Ikosarakt1 (talk ^ contribs) 09:56, May 17, 2014 (UTC)

UmF5bydzIHBob25lIG51bWJlcg==? ☁ I want more clouds! ⛅ 10:16, May 17, 2014 (UTC)

If that is true, I have absolutely no idea how you found it. King2218 (talk) 14:03, May 17, 2014 (UTC)

Google "Agustin Rayo number" and you will find it. I had it in first two results. LittlePeng9 (talk) 14:09, May 17, 2014 (UTC)

Wikipedia[]

Look! Rayo's number now has the official article on Wikipedia! Ikosarakt1 (talk ^ contribs) 14:25, May 18, 2014 (UTC)

Binary Rayo and Hyper-R notation[]

The binary Rayo function Rayo(a,b) is the smallest positive integer bigger than any finite positive integer named by an expression in the language of bth order set theory with a symbols or less. Even with b=2, this should grow much, much faster than Rayo's function.

Hyper-R notation is the same as Hyper-E notation, with the slight difference that R(b)a = Rayo(b,a). If b is not specified, assume it is a googol rather than 10. Now I have defined a few more numbers. Rayoplex is R1#2. Rayoplux is R1#1#2. We can continue with numbers in Hyper-E notation. For example, I define the tethrayothoth as R100#^^#100. This may be the biggest finite number ever mentioned. —Preceding unsigned comment added by 77.101.22.166 (talk • contribs)

Before claiming that it's much, much faster than Rayo(n), please solve the challenge: Tethrayothoth

\(\geq\) Rayo's number+1. Ikosarakt1 (talk ^ contribs) 10:20, June 28, 2014 (UTC)

Define bth-order set theory. you're.so.pretty! 15:20, June 28, 2014 (UTC)

Even the current variant of Rayo's number is defined ambiguously, because no exact pseudo-algorithm is given to determine whether the formula true or not. Also, before going past Rayo's function, a certain non-recursive notation must be developed and proved to reach it, otherwise it gets senseless. Ikosarakt1 (talk ^ contribs) 15:46, June 28, 2014 (UTC)

If there were an algorithm for determining the truth of a formula, then Rayo's function would be recursive, and therefore slower growing than the Busy Beaver function. So it is necessary for Rayo's function's strength that truth is not determinable by an algorithm, or even by a recursively enumerable formal theory. Also, there's really no hope of developing an ordinal notation that reaches the level of Rayo's function. You don't have to like it - the upper reaches of googology are not my favorite part. Deedlit11 (talk) 15:58, June 28, 2014 (UTC)

@Iko Uncomputability ≠ ambiguity.

@Deedlit I don't buy your penultimate sentence. Why can't we consider FOST itself an ordinal notation when it uniquely names an ordinal? Obviously it won't be computable, but I don't believe that is a necessary criterion for the designation of "ordinal notation." you're.so.pretty! 16:45, June 28, 2014 (UTC)

Hmm, yes I suppose you can use FOST itself to designate ordinals. The question is, if we let \(\alpha\) be the smallest ordinal not definable in FOST, is \(F_\alpha\) comparable to Rayo's function? Rayo's function grows at least as fast as \(F_\alpha\), since if \(\beta < \alpha\) then \(F_\beta\) is definable in FOST, but it's not clear to me that there isn't some way that Rayo's function grows faster than \(F_\alpha\). Deedlit11 (talk) 17:10, June 28, 2014 (UTC)

Touché. How about we use a more powerful formal system (second-order, infinitary logic, whatever) which is capable of defining Rayo's function, and most likely the ordinal describing its growth rate? All we need to do is regard that formal system as an ordinal notation and Bob's your uncle. you're.so.pretty! 17:22, June 28, 2014 (UTC)

Hmm, probably. I still can't say for certain though that second order set theory or whatever more powerful system we use will extend FGH up to the level of Rayo's function. It seems intuitive that FGH (or BBH) up to Rayo's ordinal reaches Rayo's function, but we're getting to an area where things are very hard to prove. Deedlit11 (talk) 17:41, June 28, 2014 (UTC)

Another reason why this discussion is so inconclusive is that we don't actually know a thing about Rayo's ordinal. I'm optimistic about finding a notation after a certain threshold of knowledge, but for the moment we're still in the tunnel. you're.so.pretty! 18:28, June 28, 2014 (UTC)

Sorry for not signing myself for my post. Anyway, I would guess that second order set theory is to first order set theory roughly what an oracle machine is to a Turing machine. However, I have not been able to formalise it. Also, I am guessing that Rayo's ordinal (R) has the following fundamental sequence:

R[1] requires one (plus an offset) symbol of FOST to define. R[2] requires two (again, plus an offset) symbols to define. This may just be the first undefinable ordinal. 77.101.22.166 08:41, June 30, 2014 (UTC)

Fundamental sequences[]

Let \(N(\alpha)\) be the minimal length of a FOST expression that uniquely identifies \(\alpha\). Then:

\(0[x] = 0\)
\(\alpha[x] = \max\{\beta < \alpha : N(\beta) \leq N(\alpha) + x\}\) (when \(N(\alpha)\) exists)

you're.so.pretty! 16:53, June 28, 2014 (UTC)

First of all, why the hell fundamental sequence for 0? Secondly, there is a simplier alternative - \(\alpha[n]\) is largest ordinal, smaller than \(\alpha\), definable using n FOST symbols (this is pretty much the same, but not symbolic and why the hell again \(N(\alpha+\)). Thirdly, that's about right. LittlePeng9 (talk) 10:42, June 30, 2014 (UTC)

As I said on the talk page for the Church-Kleene ordinal, I'm following suit with a definition given by Weiermann based on the Cichon norm. you're.so.pretty! 20:22, June 30, 2014 (UTC)

higher-order logic[]

concerning the discussion on the application of higher-order logic to set theory, i present a relevant paper that i haven't read yet: [1] it's vel time 07:22, September 20, 2014 (UTC)

By scrolling through the paper, it essentially uses ZF(C) axioms as set theory, not the universe with its truth values. LittlePeng9 (talk) 09:14, September 20, 2014 (UTC)

you've confirmed the fact that i didn't read it

moving on, is there any documented literature regarding collections of classes, or collections of collections of classes, etc.? it's vel time 18:07, September 20, 2014 (UTC)

Re: Bounds[]

There are already Addition, Multiplication, Exponentiation in that page. It seems that it is possible to define a series of up-arrow notation in reasonable linear numbers of symbols. The lower bound of Rayo(googol) may be something like \(\{a,b,10^c\}\) where a,b are reasonable small numbers and c is probably around 97 or 98. Is it? D57799 (talk) 07:44, October 19, 2014 (UTC)

Yes, that's true, but in few thousand symbols we can already define Turing machines, so lower bound you proposed would be very weak (although unarguably correct). LittlePeng9 (talk) 07:49, October 19, 2014 (UTC)

Also, note that no one has yet written down full formula even for addition, so we actually need some effort to make this into real bound. LittlePeng9 (talk) 07:52, October 19, 2014 (UTC)

What's the record by now? D57799 (talk) 07:53, October 19, 2014 (UTC)

Formally proven? I believe 3.333x10⁹⁸ you can see above. LittlePeng9 (talk) 07:58, October 19, 2014 (UTC)