Talk:Finite promise games

Why should we feel that this function is even well-defined and outgrows all our notations? I'm starting to think that Loader's function, Laver tables and stuff like that is actually hoax. I haven't seen any proofs for their strength, I saw only claims! Ikosarakt1 (talk ^ contribs) 09:20, June 23, 2014 (UTC)

The proof that, for example, Loader's function grows really fast is the fact that the Calculus of Constructions can implement any function provably recursive in higher order logic. So it's like the Busy Beaver function at a lower level.

Simple proof that Loader's function outgrows any function provably recursive in higher order logic: let f be such a function, and let n be the number of characters required to implement it. Let m be the number of characters required to implement the doubling function. Then we can output f(2x) using at most m+n+x characters, so for large x we have 2x > m+n+x and so D(2x) >= D(m+n+x) >= f(2x).

I don't know the proof that the Calculus of Constructions can implement any function in higher order logic. Anyone have any sources for this? Even proving it for second order arithmetic would be quite interesting.

As for Friedman's finite games, I believe Friedman asserted either that the associated function is not provably recursive in ZFC+Mahlo, or that that the function outgrows all functions provably recursive in ZFC+Mahlo. I forget exactly what he said. The latter statement is of course what we are after, but I believe that if the former statement is true we can assume the latter. It is possible for a recursive function to be not provably recursive in a system T but not outgrow all functions provably recursive in T; for example, we could take f to be sufficiently fast growing on even inputs, and zero on odd inputs. But I believe such exceptions to be pathological, so a "naturally defined function" should satisfy the latter statement if it satisfies the former. Of course Friedman may have stated the latter after all, we should look it up.

As for Laver tables, I am unsure. We know that there are theorems that are not provable in ZFC+"rank into rank cardinal", but does that mean that the specified function outgrows all functions provably recursive in ZFC+"rank into rank cardinal"? I don't see why this should necessarily be the case, so I am suspicious in the case of Laver tables.Deedlit11 (talk) 13:19, June 23, 2014 (UTC)

I just looked up the link, and Friedman does indeed state that the described function dominates all provably recursive functions of SMAH+, which is stronger than ZFC+Mahlo, so there you go. Deedlit11 (talk) 13:22, June 23, 2014 (UTC)

Sorry, but the problem is that our community can't figure out proofs about how these things compares to explicit notations (like up-arrows and\(\psi\)), and these "logics" and "arithmetics" doesn't really give sense of them. How to prove that D(n) indeed outgrows, say,\(n \uparrow^n n\)? Ikosarakt1 (talk ^ contribs) 13:58, June 23, 2014 (UTC)

\(f(n) = n \uparrow^n n\)is expressible even in Peano arithmetic, so we can write a function in the Calculus of constructions that implements it. So just use the proof above to show that D(n) outgrows f(n).

Do you accept that the Busy Beaver function outgrows all our recursive functions, even though we can compute only a few values of the Busy Beaver? Then it's the same with these other functions, accept the class of functions that they beat are smaller. If we take the system T, for example, the expressible functions are exactly the functions provably recursive in Peano arithmetic, so the diagonalizing function obviously outgrows f(n). The functions in the fast-growing hierarchy that are provably recursive in Peano arithmetic are exactly the functions below\(\varepsilon_0\), so I would say we have a good sense of the growth rate of the diagonalizing function of system T. For, say, system F, whose expressible functions are the provably recursive functions of second order arithmetic, the associated ordinal is very, very large, larger than what we can currently express. So I guess for that reason we cannot get a good "sense" of the growth rate. But, it is very likely that all our functions are provably recursive in second order arithmetic, so D(n) will beat all our notations for that reason, even if we cannot get a really good grasp of D(n). Deedlit11 (talk) 14:19, June 23, 2014 (UTC)

Can you show some more bounds for D(n)? Or can you explain how to do that?  Also, can you explain how Friedman's finite games even returns numbers. I don't see any functions here. Wythagoras (talk) 14:54, June 23, 2014 (UTC)

I'm actually not that well versed in the Calculus of Constructions. Basically, to get bounds on D(n) is very similar to getting bounds on the Busy Beaver function; to get lower bounds, you present a term with n symbols that generates a large number. Getting upper bounds is harder, you need to evaluate all terms and find the biggest number for a given length. On the plus side, you don't have to worry about nonterminating terms, since every term terminates in the Calculus of Constructions. In David Moews' contest recap, he references an article that describes how to program F_epsilon_0 in the Calculus of Constructions. Obviously this is not that big, but it's a start.

For Friedman's finite games, you can read the original post. He gives the theorem

PROPOSITION 1.2. Let T be in PL and n >= 1. If m,s are sufficiently large then Bob wins G(T,n,s) even if Bob accepts all factorials > m offered by Alice.

So for example we can define f(T,n,m) to be the minimum number S such that if s >= S, Bob wins G(T,n,s) even if Bob accepts all factorials greater than m offered by Alice. There's a bit of difficulty here though, because T is a function from N^k to N, which is equivalent to a real, not a natural number. Perhaps it is the fact that T is piecewise linear, that means that T is reducible to integers. I'm not quite sure. So instead let's use proposition 4.2:

PROPOSITION 4.2. Let v_1,...,v_p be in N^k and n,s >= 1. If m is sufficiently large then Bob wins G(v_1,...,v_p;n,s) even if Bob accepts all factorials > m offered by Alice.

Define f(v_1,...,v_p;n,s) to be the minimum number M such that if m >= M, Bob wins G(v_1,...,v_p;n,s) even if Bob accepts all factorials > m offered by Alice. Then f is not provably recursive in ZFC+{There exists a k-strong Mahlo}_k. To get a nice unary function, define f(x) to be max f(v_1,...,v_p;n,s) with n, s, and v_ij for all i,j less than or equal to x. Then f(x) dominates all provably recursive functions of ZFC+{There exists a k-strong Mahlo}_k. Deedlit11 (talk) 15:30, June 23, 2014 (UTC)

Numbers?

I cannot see any statement about functions (or numbers) in the page. How can this theory create large numbers or fast-growing functions? hyp$hyp?cos&cos (talk) 05:01, July 28, 2014 (UTC)

In my opinion, it's just a hoax. Factorials can't provide even tetrational growth rate, but Friedman claims that it grows in the magnitude of something far above\(f_{\psi(M)}(n)\). Ikosarakt1 (talk ^ contribs) 17:20, July 28, 2014 (UTC)

The result is correct, just the article is poorly written and doesn't emphasise what numbers are the ones which are so large. I will try to make article more accessible whenever I'm back home. LittlePeng9 (talk) 17:40, July 28, 2014 (UTC)

LittlePeng9 has made a good edit, I would just like to add that if you go to the source page, for the other propositions of the form "For m sufficiently large, S(a,b,c,m)" where S is some statement involving m and some other variables, we can convert that to a fast-growing function by defining f(n) to be the minimum number M so that if m >= M and a, b, and c are of size no greater than n, then S(a,b,c,m) is true. If a,b,c are natural numbers the notion of "size" is obvious, otherwise we have to make a definition (like for polynomials, the "size" is the maximum of the degree and all the coefficients). Deedlit11 (talk) 05:04, July 29, 2014 (UTC)

SMAH vs. SMAH+

What's the difference between them? I don't see it. The two statement seem the same. hyp$hyp?cos&cos (talk) 00:18, July 29, 2014 (UTC)

SMAH is ZFC plus, for each \(k\), an axiom of the form "there is a \(k\)-Mahlo cardinal". Note that any proof can only invoke at most finitely many of those axioms. On the other hand SMAH+ is ZFC plus "for each \(k\), there exists a \(k\)-Mahlo cardinal". A proof could invoke the axiom to know that there exist \(k\)-Mahlo cardinals for arbitrarily high \(k\).

Another interesting example would be EFAE0 = EFA + for each \(k\), an axiom of the form "\(\omega \uparrow\uparrow k\) is well-ordered", versus EFAE0+ = EFA + "for each \(k\), \(\omega \uparrow\uparrow k\) is well-ordered". The former axioms are all provable in PA, so the former theory is equivalent to PA, but the last axiom is equivalent to "\(\varepsilon_0\) is well-ordered", which is not provable in PA, so EFAE0+ is stronger than PA. Goodstein's theorem is provahble in EFAE0+, but not EFAE0. Deedlit11 (talk) 04:55, July 29, 2014 (UTC)

I agree that this is quite confusing at first, I had the same problem when I first met the definitions on SMAH and SMAH+. The key thing about SMAH is that we don't allow logical operations on infinite number of statements, so we can't simply take union of infinitely many statements of form "there is \(k\)-Mahlo cardinal" to get "for all \(k\) there is \(k\)-Mahlo cardinal".

Deedlit's example also illustrates the fact on why there must be the least ordinal for which we can't prove it's well-ordered: at first one may think that since PA can prove that \(\omega\) is well ordered, \(\omega^\omega\) is, \(\omega^{\omega^\omega}\) is,... then, since all of these are provable in PA, it should be also the case that PA can prove that it can prove all of the above. One of the reasons why this isn't so obvious is because the proof of each fact requires much more time than earlier ones - so, possibly, while we can prove that \(\omega^\omega\) is well ordered in 500 symbols, for \(\omega^{\omega^\omega}\) we might require \(2\uparrow^{500} 500\). So only way would be to again use some infinitary operation, which is disallowed. LittlePeng9 (talk) 07:17, July 29, 2014 (UTC)

I think the difference is similar to that of "KP + 'there exists a recursively 1-inaccessible ordinal' + 'there exists a recursively 2-inaccessible ordinal' + 'there exists a recursively 3-inaccessible ordinal' + ..." and "KP + 'for all positive integer n, there exists a recursively n-inaccessible ordinal'". But what are the PTO of them? {hyp/^,cos} (talk) 06:09, August 20, 2017 (UTC)

First values of the F function

I believe F(1)=0 or undefined (game must consist of n<1 stages, so that would be zero stages). I also think that F(2) = 1, but can we find more values or lower bounds? I don't understand it in full now. Wythagoras (talk) 08:09, July 29, 2014 (UTC)

Anyone? Wythagoras (talk) 16:33, August 21, 2014 (UTC)

If the game lasts zero stages, the statement "Bob has kept all his promises" is (vacuously) true, therefore Bob wins you're.so.pretty! 18:38, August 21, 2014 (UTC)

Computability

One thing confusing me here is the "for all T," "for all P and Q," "for all V and s." Doesn't that give us infinitely many things to evaluate? Friedman gives the three functions as functions of T, (P,Q), and (V,s) respectively. It appears that we have not three functions, but three infinite families. you're.so.pretty! 16:17, August 22, 2014 (UTC)

Some limitation on T, P, Q and V must be part of an input, e.g. that P,Q have coefficients and degree <n. I have mentioned that when rewritting the article some time ago. LittlePeng9 (talk) 16:19, August 22, 2014 (UTC)

Oh, crap, I must have missed that while rewriting. Thanks. Hope the latest edit corrects it. you're.so.pretty! 16:29, August 22, 2014 (UTC)

Is the number of different variables also limited to n? Wythagoras (talk) 16:31, August 22, 2014 (UTC)

It's not, but it will be finitely restricted if we put a cap on the Gödel numbers of T,P,Q,V you're.so.pretty! 16:59, August 22, 2014 (UTC)

eh

What does

\(\mathbb{N}^k\) mean? (I couldn't find anything) King2218 (talk) 08:20, August 23, 2014 (UTC)

It means the set of all size-k vectors whose elements are in\(\mathbb{N}\) (i.e. positive integers). — ☁ I want more clouds! ⛅ 08:48, August 23, 2014 (UTC)

cross product \(\mathbb{N} \times \cdots \times \mathbb{N}\) (with \(k\) copies of \(\mathbb{N}\)) you're.so.pretty! 19:52, August 23, 2014 (UTC)

Playing x

What means "Bob plays x"? What we should do with x? Expect that, I think I got the definition. Ikosarakt1 (talk ^ contribs) 13:17, August 26, 2014 (UTC)

When Bob plays x, we can assume he writes this number on a piece of paper visible to both players. LittlePeng9 (talk) 16:10, August 26, 2014 (UTC)

Thanks. Now I understand: affine function is the function in the form

\(f(a_1,a_2,\cdots,a_m) = N_1*a_1+N_2*a_2+\cdots+N_m*a_m+c\) . Thus, roughly speaking, affine function is the multi-variable function which returns a polynomial. Piecewise linear means that we can also make each

\(a_k\) for each k to be the result of affine function too. In otherwords, we can construct "tetrational hypernomials." All other parts are quite easy. The problem for me is only the part

\(T: \mathbb{N}^k \mapsto \mathbb{N}\)

does that mean the input of the function should be in the form

\(n^k\) for integers n and k and output in the form

\(n\) for integer n? Also, why we use "vector y?" Do we work with numbers or vectors? Ikosarakt1 (talk ^ contribs) 17:05, August 26, 2014 (UTC)

Vector is an ordered tuple of numbers, for example, an ordered pair is a vector of size 2. Generally, element of \(\mathbb{N}^k\) is a k-tuple, or vector of size k, which is of the form \(a_1,a_2,...,a_k\) with all \(a_i\in\mathbb{N}\). LittlePeng9 (talk) 17:16, August 26, 2014 (UTC)

Note that \(k\) is fixed, but only with respect to each game. You could think of it as a separate argument, but really it comes "bundled" with T,R,P,Q,V (since we can derive it from their domains). you're.so.pretty! 17:36, August 26, 2014 (UTC)

infinitely many axioms

Are there any theories that allow proofs employing infinitely many axioms? you're.so.pretty! 19:16, August 26, 2014 (UTC)

Maybe. LittlePeng9 (talk) 19:50, August 26, 2014 (UTC)

ZFC

Is this the only function on the wiki that is known to dominate all functions provably recursive in ZFC? That's a little surprising! you're.so.pretty! 21:54, August 31, 2014 (UTC)

"Known" King2218 (talk) 09:27, September 1, 2014 (UTC)

Well, out of other things, only Laver tables have a chance, but it's hard to say anything about them. LittlePeng9 (talk) 10:06, September 1, 2014 (UTC)

Or the fusible margin function. you're.so.pretty! 10:28, September 1, 2014 (UTC)

That function is provably recursive in ZFC. LittlePeng9 (talk) 11:24, September 1, 2014 (UTC)

How come? you're.so.pretty! 19:09, September 1, 2014 (UTC)

T inversion of x

In FPLCI game, when Wojtek accept, he plays x and promises that

none of the integers he ever plays will contain a T inversion of x.

Actually it is confusing because he plays an integer and T inversion of x is a vector. Suppose that T inversion of x is (1,3,4). Which is correct?

1. He can't play 1. He can't play 3 or 4, either.
2. He can play 1, but he can't play all of the 1, 3, 4 in different turn, which will make (1,3,4) altogether.

🐟 Fish fish fish ... 🐠 10:06, January 25, 2017 (UTC)

Note: I am looking at Friedman's original post, so if the article implies something different, it ought to be changed.

First let me clarify (if it is not clear), that we aren't allowing Bob/Wojtek/me to play any T inversion of x, since they may be many of these, but for simplicity let's assume (1,3,4) is the only one.

Friedman says that "there will be no T inversion of x among the integers ever played by Bob". In our case, this means precisely that the tuple 1,3,4 will never be among the numbers played by Bob. As long as some, but not all, of the integers in this inversion have been played, everything is fine, so the second alternative is the right one. LittlePeng9 (talk) 13:55, January 25, 2017 (UTC)

I see. Thanks. 🐟 Fish fish fish ... 🐠 14:15, January 25, 2017 (UTC)

Questions regarding FLCI games

> Nathan selects a number x∈[0,s], either of the form w! or y+z, where y and z are integers previously played by Wojtek.

Do the integers y and z Nathan can pick include the components of any of the vectors Wojtek has played?

> By rejecting, he plays y, where ∑y=x and y is additively equivalent to a vector in V

Is it also required that the components of y were played by Wojtek at any time, similar to when he accepts the offer? If not, wouldn't that allow infinitely many vectors for him to choose from? How could one compute all the possible vectors he could play if the choices are infinite?

> Consider the modified game G_m(V,n,s) where Wojtek is forced to accept all factorial numbers greater than m.

Isn't Nathan only able to select factorial numbers less than or equal to s? If m>s, wouldn't that mean Wojtek could still reject any offer if he wants to?

QuasarBooster (talk) 23:29, June 9, 2019 (UTC)

> Do the integers y and z Nathan can pick include the components of any of the vectors Wojtek has played?

Wojtek can only play a natural number, but not a vector, Actually, the description in the article is quite ambiguous. I corrected the error following the original definition.

> Is it also required that the components of y were played by Wojtek at any time, similar to when he accepts the offer?

No. Instead, Wojtek plays all components of y at this time.

> If not, wouldn't that allow infinitely many vectors for him to choose from? How could one compute all the possible vectors he could play if the choices are infinite?

He can choose explicitly one vector \({\bf y}\). Maybe the corrected version of the article is clearer.

> Isn't Nathan only able to select factorial numbers less than or equal to s?

Yes. Therefore the restriction has some effect only when \(m < s\).

> If m>s, wouldn't that mean Wojtek could still reject any offer if he wants to?

Exactly. Therefore I guess that Friedman intended "\(m\) is not so much smaller than \(s\). (Since I have never read the proof using the restriction, I do not know at all whether it is actually what Friedman intended or not.)

p-adic 00:25, June 10, 2019 (UTC)

I get it now. When he rejects, he plays all the components, not the vector itself.

> He can choose explicitly one vector \({\bf y}\).

I'm really dumb. I thought the components of y could be anything, and completely forgot that they all must add up to x. I always forget that that restriction makes the choices finite.

> Therefore I guess that Friedman intended \(m\) is not so much smaller than \(s\).

That's what I was thinking too. Since s<=a I'm pretty sure that means FLCI(a)<=a. Obviously that's a huge contradiction with it being a very fast growing function. There's gotta be something else he mentioned ambiguously that resolves this issue.

QuasarBooster (talk) 01:40, June 10, 2019 (UTC)

Oh... The description in the article is completely different from the original description... Now I corrected the error.

p-adic 11:55, June 10, 2019 (UTC)

Ah, now I can see how FLCI(a) could get pretty large theoretically. Now that Wojtek is required to win all games G_m(V,n,s) for all n,s>0, is this function still computable? The way I see it, we either have to check each game for all values of n and s, unless he loses a game, or we somehow prove computationally that he'll always win, without checking all of the possible values.

QuasarBooster (talk) 15:05, June 10, 2019 (UTC)

The computaability in googology is a little ambiguous. In the sense that the definition do not write an explicit algorithm, it is not computable. On the other hand, we often say that a fnunction (without a specified algorithm) is computable when there is an (unspecified) algorithm to compute it. This should be the latter case.

It is very difficult to create an explicit computation rule because it looks like a variant of a verification-falsification game in set theory. Assuming that the statements by Friedman are correct, I guess it is computed in the following recursive way:

1. For each \(k,V\) satisfying the restriction on \(a\), compute \(m(k,V)\) in the following way:
   1. Enumerate all strings which are proofs of statements in \(\textrm{RCA}_0\). (This can be done by the method called Goedel correspondence.)
   2. Let \(i,N = 0\).
      1. If \(i\) is a proof in \(\textrm{RCA}_0\) of the statement "Wojtec wins \(G_N(V,n,s)\) for all \(n,s \geq 1\)", then \(m(V,k)\) is the current value of \(N\).
      2. If \(i\) is a proof in \(\textrm{RCA}_0\) of the negation of the statement "Wojtec wins \(G_N(V,n,s)\) for all \(n,s \geq 1\)", then replace \(i\) by \(0\) and \(N\) by \(N+1\), and go back to 1.2.3.
      3. Replace \(i\) by \(i+1\), and go back to 1.2.3.
2. Then return \(\textrm{FLCI}(a)\) as the maximum of the values of \(m(k,V)\). It is computable because there are only finitely many \((k,V)\)'s.

I believe that the computation of \(m(V,k)\) terminates from guessing the statements by Friedman. This is just an example to compute the value of \(\textrm{FLCI}(a)\), and hence there might be an algorithm which is much easier to understand.

p-adic 23:38, June 10, 2019 (UTC)

That's a pretty intense algorithm. But I'll take your word that it allows us to get a value of N that works for all n and s. As you say, maybe one day someone will come up with a more streamlined way to show the same thing.

QuasarBooster (talk) 01:46, June 11, 2019 (UTC)

As verification-falsification game and consistency proof are sometimes reduced to hydra games, I believe that the computation can be interpreted into some hydra game.

p-adic 04:43, June 11, 2019 (UTC)

Hmm, that would be very interesting to see. I can't imagine how crazy of a hydra game this would make for, haha.

QuasarBooster (talk) 04:04, June 12, 2019 (UTC)

Search space of FPCI games?

It looks like if you wanted to program FLCI(a) for the finite linear copy invert games, you wouldn't be able to simply just check all games until the desired condition is met, since it requires Wojtek to win for every value of n and s, and thus the search space at any value of N is infinite. However, it doesn't seem like the search space for any value of N is infinite for the other games, namely finite polynomial copy invert. The two polynomials and n are all bounded by the input of FPCI, which means that you could search through all the games until you found a large enough N for Wojtek to win. Have I missed something in the definitions that actually makes the search space of FPCI games infinite for a fixed value of N when P, Q, and n are bounded?    QuasarBooster (talk) 00:38, November 15, 2019 (UTC)

I think that the search space of FPCI is actually finite. But I am not certain that whether a given strategy is a winning strategy or not is determined in a trivial way. For example, you need to check all posibilities of Nathan's offers, which might contain an offer of a number greater than N.

p-adic 05:43, November 15, 2019 (UTC)

Come to think of it, aren't Nathan's offers always restricted to between [-N,N]? If not, I don't see where in the definition he's allowed to go beyond that interval. Also, if Wojtek is forced to accept any factorial numbers greater than N but Nathan isn't able to offer integers greater than N, doesn't that kind of defeat the point of that restriction? QuasarBooster (talk) 06:58, November 15, 2019 (UTC)

Uh, I found a mistake in the article. The numbers \(m\) and \(s\) are not necessarily \(N\), but are greater than or equal to \(N\). I corrected it. (I noticed that when we feel something strange in the article, then we should go back to the original definition...) So even if \(m = N\), \(s\) can be much greater than \(N\). Also, my answer above is incorrect. I got confused. Nathan's offers are actually bounded by \(s\) instead of \(N\), and hence when we fix an \(s\), we can check whether a given recursive strategy is a winning strategy or not. The point is that we need to check the existence of a winning strategy for any \(m\) and \(s\) greater than or equal to \(N\).

p-adic 08:20, November 15, 2019 (UTC)

It does make a lot more sense with the wording of the article to have m and s greater than or equal to N. Thanks for noticing that! Unfortunately for me, that means the search space is now infinite as I feared, so one can't simply check all games for a fixed N. Oh well. QuasarBooster (talk) 15:46, November 15, 2019 (UTC)

According to Friedman, they are somewhy computable for any fixed input a. Therefore there should be a recursive criterion for determining whether a given N actually satisfies the condition or not without searching infinitely many m and s. Maybe we need to understand the background in proof theory to know Friedman's intension.

p-adic 22:41, November 15, 2019 (UTC)

You definitely might be right about that. QuasarBooster (talk) 01:38, November 16, 2019 (UTC)

I recall that I wrote in the section above that FLCI(a) is perhaps computed by searching formal proofs (in arithmetic) of either the existence or the non-existence of a winning strategy. Similarly, I guess that FPCI(a) is computed by searching formal proofs. Namely, consider the following algorithm:

1. Let N = 0 and i = 0.
2. If i is the Goedel number of a formal proof of the statement "for any m,s>= N and (P,Q,n) satisfying the restrictions, there exists a winning strategy of G_m(P,Q,n,s)", then return N.
3. If i is the Goedel number of a formal proof of the negation of the statement above, then increment N and set i = 0. Go back to 2.
4. Increment i. Go back to 2.

According to Friedman, the statement above is provable under arithmetic for sufficiently large N. The point is that we do not know whether 3 works well or not, i.e. whether the truth value of the statement is decidable by the provability in arithmetic or not.

p-adic 04:02, November 16, 2019 (UTC)

Ideally there would be a more organic way to compute these functions; one that doesn't require writing proof checkers and such. I know that's wishful thinking, but I'm just saying it would be nice. Assuming the questions about these games get resolved, the first person to find such a way is a genius. QuasarBooster (talk) 04:15, November 16, 2019 (UTC)

Exactly. I hope so, too. Such a new interpretation will tell us how to encode consistency into games. Then it will give us new strategy to define computable large numbers.

p-adic 04:36, November 16, 2019 (UTC)