The finite promise games are a collection of mathematical games developed by American mathematician Harvey Friedman in 2009 which are used to develop a family of fast-growing functions , and . The greedy clique sequence is a graph theory concept, also developed by Friedman in 2010, which are used to develop fast-growing functions , and .
represents the theory of ZFC plus, for each , "there is a strongly -Mahlo cardinal", and represents the theory of ZFC plus "for each , there is a strongly -Mahlo cardinal". represents the theory of ZFC plus, for each , "there is a -stationary Ramsey cardinal", and represents the theory of ZFC plus "for each , there is a strongly -stationary Ramsey cardinal". represents the theory of ZFC plus, for each , "there is a -huge cardinal", and represents the theory of ZFC plus "for each , there is a strongly -huge cardinal".
Finite promise games
Each of the games is finite, predetermined in length, and has two players (Alice and Bob). At each turn, Alice chooses an integer or a number of integers (an offering) and the Bob has to make one of two kinds of promises restricting his future possible moves. In all games, Bob wins if and only if Bob has kept all of his promises.
Finite piecewise linear copy/invert games
Here, is the set of integers, and is the set of non-negative integers. Here, all letters represent integers. We say that a map is piecewise linear if can be defined by various affine functions with integer coefficients on each of finitely many pieces, where each piece is defined by a finite set of linear inequalities with integer coefficients. For some piecewise linear map , a -inversion of is some such that . We then define the game for nonzero .
has rounds, and alternates between Alice and Bob. At every stage of the game, Alice is required to play , called her offering, which is either of the form or , where and are integers previously played by Bob. Bob is then required to either:
Accept , thereby playing and promising that there will be no -inversion of among the integers ever played by Bob. This promise applies to all past, present and future plays in the game. Reject , thereby play a -inversion of and promising that is never played by Bob.
In RCA0, it can be proven that Bob always has a winning strategy for any given game. The game is a modified version where Bob is forced to accept all factorial offers by Alice . Bob always has a winning strategy for for sufficiently large , although this cannot be proven in any given consistent fragment of , and only . The function is the smallest such that Bob can win for any such that and are greater than or equal to and all the following values are less than :
(the domain of is ) the number of pieces of the absolute values of the coefficients of the inequalities in the absolute values of the coefficients of the affine functions in
Finite polynomial copy/invert games
Let be a polynomial with integer coefficients. A special -inversion at in consists of such that . We now define the game for nonzero , where are polynomials with integer coefficients. consists of alternating plays by Alice and Bob. At every stage of the game, Alice is required to play of the form , or , where is a -tuple of integers previously played by Bob. Bob is then required to either:
Accept , thereby playing and promising that there will be no special - or -inversion of among the integers ever played by Bob. This promise applies to all past, present and future plays in the game. Reject , thereby playing a special - or -inversion of and promising that is never played by Bob.
Let be polynomials with integer coefficients. In RCA0, it can be proven that Bob always has a winning strategy for any given game. If are sufficiently large then Bob wins , which is where Bob is forced to accept all double factorials offered by Alice. However, once again, this cannot be proven in any given consistent fragment of , and only . The function is the smallest such that Bob can win for any such that and are greater than or equal to and all the following values are less than :
(the domain of the polynomials is ) the degrees of and the absolute values of the coefficients of and
Finite linear copy/invert games
We say that are additively equivalent if and only if . For nonzero integers and , we define the game which consists of alternating rounds between Alice and Bob. At every stage of the game, Alice is required to play an integer of the form or , where are integers previously played by Bob. Bob is then required to either: