有限約束ゲーム

有限約束ゲーム (Finite promise games) は、Harvey Friedmanが定義した4つの関連した2人ゲームである。ZFCの拡張であるSMAHにおける証明可能全体再帰関数を支配する急増加関数であり、より強いSMAH+理論によって証明可能である。

概要

その名前から分かるように、ゲームはそれぞれ有限の長さで、その長さはあらかじめ決められている。それぞれの手番で、プレイヤーの1人（マシモと呼ぶ）が整数を1つあるいは複数選び（提案）、もう1人のプレイヤー（うるかと呼ぶ）は将来の手番を制限する2種類の約束のうちのどちらかをする必要がある。うるかは、ゲームが終了するまでにその約束を守り続けることができれば、勝利する。

ここから先は、次の3つの有名な理論体系を使って説明する。

• RCA₀ はロビンソン算術と\(\Sigma_1^0\)-帰納と\(\Delta_1^0\)-内包公理を持つ理論体系である（二階算術を参照）。
• SMAH は ZFC に、すべての正の整数\(k\)に対して「強い\(k\)-マーロ基数が存在する」という公理を加えたものである。すべての\(k\)に対して加えるので、無限の公理を加えることとなる。
• SMAH+ は、ZFC に、「すべての正の整数\(k\)に対して強い\(k\)-マーロ基数が存在する」という公理を加えたものである。

SMAHとSMAH+の違いは、SMAHの証明では有限の公理しか使えないため、SMAH+の文を証明するために「すべての\(k\)について」と無限の公理を使うことができないところにある。

有限区分線形約束ゲーム (FPLCIゲーム)

関数\(T: \mathbb{N}^k \mapsto \mathbb{N}\)が区分線形 (piecewise linear) であるとは、整数係数の不等式による条件分けされた有限個の一次関数によって表記できることを意味するものとする。区分線形関数\(T\)に対して、ベクトル\(\mathbf{y} \in \mathbb{N}^k\)が\(x\)に対する\(T\)の逆変換であるとは、\(T(\mathbf{y}) = x\)を満たすことを意味するものとする。

区分線形関数\(T: \mathbb{N}^k \mapsto \mathbb{N}\)と、2つの正の整数\(n\)と\(s\)が与えられた時に、有限区分線形約束ゲーム (finite piecewise linear copy/invert game, 略してFPLCIゲーム) \(G(T, n, s)\) を、次のように定義する。\(G(T, n, s)\)は、マシモとうるかの間の2人ゲームで、\(n\)ラウンドで終了する。マシモが先手である。

マシモの手番では、\(w!\) または \(y + z\) となるような\(x \in [0, s]\) を選ぶ。ここで、\(y\)と\(z\)はうるかがそれまでに選んだ数字でなければならない。\(x\)がマシモの提案である。うるかは、その提案を受け入れるか拒否することを選ぶことができる。

• 提案を受け入れた時には、うるかは\(x\)を選んで、うるかは決して\(x\)の\(T\)による逆変換の中から数字を選ばないと約束する。
• 提案を拒否した時には、\(x\)の\(T\)による逆変換の中から好きな数字を選んで、決して\(x\)を選ばないと約束する。

うるかが約束を破ると、うるかの負けである。うるかが\(n\)ラウンドすべて約束を破らなければ、うるかの勝ちである。ここで、約束はうるかの過去、現在、未来のすべての手番に適用される。

---

うるかはあらゆる有限区分線形ゲームに対して勝つ戦略がある。これはRCA₀で証明可能である。

実は、このゲームのルールにおいて、提案を拒否できる条件を制限した時にも、うるかは必ず勝つことができる。「うるかは\(m\)よりも大きい階乗数の提案を必ず受け入れなければならない」というルールを追加したゲームを \(G_m(T, n, s)\) とする。うるかは、すべての\(T\)と\(n\)に対して、十分に大きい\(m\)と\(s\)を設定すれば、\(G_m(T, n, s)\)に勝つ戦略がある。このことは、SMAH+で証明可能であるが、SMAHと同じ強さの部分体系では証明不可能である。

\(FPLCI(a)\) を、うるかが \(G_N(T, n, N)\) に勝つことができる最小の\(N\)とする。ただし、以下のすべてが \(a\) よりも小さいものとする。

• \(n\)
• \(k\) (\(T\) の定義域は \(\mathbb{N}^k\))
• \(T\) の区分数
• \(T\) の不等式における係数の絶対値
• \(T\) の一次関数における係数の絶対値

有限多項式約束ゲーム (FPCIゲーム)

ここでは、定数 \(k\) に対して \(\mathbb{Z}^k \mapsto \mathbb{Z}\) の整数係数の多項式関数を多項式とする。

多項式 \(P\) に対して、ベクトル \(\mathbf{y}\) が\(x\)の \(P\)による特別な逆変換であるとは、\(P(\mathbf{y}) = x\) かつ、\(\mathbf{y}\) のすべての要素が厳密に 0 と \(x/2\) の間にあることを意味するものとする。

Given two polynomials \(P\) and \(Q\) and two positive integers \(n\) and \(s\), we define the 有限多項式約束ゲーム (finite polynomial copy/invert game を略してFPCIゲーム) \(G(P, Q, n, s)\) as follows. \(G(P, Q, n, s)\) is a two-player game alternating between Mashimo and Uruka, with \(n\) rounds in total. Mashimo goes first.

On his turn, Mashimo selects a number \(x \in [-s, s]\), of the form \((w!)!\) or \(P(\mathbf{y})\) or \(Q(\mathbf{y})\), where \(\mathbf{y}\) is a vector in \(\mathbb{Z}^k\) whose components were all integers previously played by Uruka. \(x\) is called his offer. Uruka either has the choice of accepting or rejecting the offer:

• By accepting, she plays \(x\), and promises that the integers she plays never contain the complete components of a special \(P\) or \(Q\) inversion of \(x\).
• By rejecting, she plays a special \(P\) or \(Q\) inversion of \(x\) of her choice, and promises that none of the integers that she ever plays are \(x\).

If Uruka ever breaks one of her promises, she loses the game. If Uruka lasts the entire \(n\) rounds without ever breaking a promise, she wins. (Promises apply to all past, present, and future plays within the game.)

---

Uruka always has a winning strategy for any given FPCI game. This is provable in RCA₀.

In fact, she can still win even if we restrict the offers that she is allowed to reject. Consider the modified game \(G_m(P, Q, n, s)\) where Uruka is forced to accept all factorial numbers greater than \(m\). Uruka can win \(G_m(P, Q, n, s)\) for all \(P,Q,n\) and sufficiently large \(m\) and \(s\) (a fact provable in SMAH+, but not in any consistent fragment of SMAH).

Let \(FPCI(a)\) be the minimal \(N\) such that Uruka can win \(G_N(P, Q, n, N)\) where all the following are less than \(a\):

• \(n\)
• \(k\) (recall that the domain of the polynomials is \(\mathbb{Z}^k\))
• the degrees of \(P\) and \(Q\)
• the absolute values of the coefficients of \(P\) and \(Q\)

有限順序不変約束ゲーム (FOICIゲーム)

Let \(R : \mathbb{N}^{2k} \mapsto \{0, 1\}\) be order invariant — that is, the order of its inputs does not affect its output. Given a vector \(\mathbf{x} \in \mathbb{N}^{k}\), we say that a vector \(\mathbf{y} \in \mathbb{N}^{k}\) is an R-inversion of \(\mathbf{x}\) iff \(\max(\mathbf{y}) < \max(\mathbf{x})\) and \(R(\mathbf{x}, \mathbf{y}) = 1\) (where the components of the two vectors are concatenated into a vector with \(2k\) components, which is the argument to R).

Given order-invariant \(R : \mathbb{N}^{2k} \mapsto \{0, 1\}\) and two positive integers \(n\) and \(s\), we define the 有限順序不変約束ゲーム (finite order invariant copy/invert game を略してFOICIゲーム) \(G(R, n, s)\) as follows. \(G(R, n, s)\) is a two-player game alternating between Mashimo and Uruka, with \(n\) rounds in total. Mashimo goes first.

On his turn, Mashimo selects an integer vector \(\mathbf{x} \in [-s, s]^k\), each component being of the form \(z\) or \(z + 1\) or \(w!\), where \(z\) is an integer previously played by Uruka. \(\mathbf{x}\) is called his offer. Uruka either has the choice of accepting or rejecting the offer:

• By accepting, she plays \(\mathbf{x}\), and promises that she never plays an \(R\) inversion of \(\mathbf{x}\).
• By rejecting, she plays an \(R\) inversion of \(\mathbf{x}\) of her choice, and promises that she will never play \(\mathbf{x}\).

If Uruka ever breaks one of her promises, she loses the game. If Uruka lasts the entire \(n\) rounds without ever breaking a promise, she wins. (Promises apply to all past, present, and future plays within the game.)

---

Uruka always has a winning strategy for any given FOICI game. This is provable in RCA₀.

しかし、フリードマンはFOICIゲームによる急増加関数を作らなかった。

有限線形結合約束ゲーム (FLCIゲーム)

Given two vectors \(\mathbf{x},\mathbf{y} \in \mathbb{N}^k\), we say that they are additively equivalent iff, for all \(i, j \leq k\), \(\sum^i \mathbf{x} < \sum^j \mathbf{x} \Rightarrow \sum^i \mathbf{y} < \sum^j \mathbf{y}\) (where \(\sum^n \mathbf{v}\) is the sum of the first \(n\) components in \(\mathbf{v}\)).

Let \(V\) be a tuple of vectors in \(\mathbb{N}^k\) and two positive integers \(n\) and \(s\), and define the 有限線形結合約束ゲーム (finite linear copy/invert game を略して FLCIゲーム) \(G(V, n, s)\) as follows. \(G(\mathbb{v}, n, s)\) is a two-player game alternating between Mashimo and Uruka, with \(n\) rounds in total. Mashimo goes first.

On his turn, Mashimo selects a number \(x \in [0, s]\), either of the form \(w!\) or \(y + z\), where \(y\) and \(z\) are integers previously played by Uruka. \(x\) is called his offer. Uruka either has the choice of accepting or rejecting the offer:

• By accepting, she plays \(x\), and promises that \(x\) can never be written as \(\sum \mathbf{y}\), where all the components of \(\mathbf{y}\) were played by Uruka at any time and \(\mathbf{y}\) is additively equivalent to a vector in \(V\).
• By rejecting, she plays \(\mathbf{y}\), where \(\sum \mathbf{y} = x\) and \(\mathbf{y}\) is additively equivalent to a vector in \(V\), and promises that she will never play \(x\).

If Uruka ever breaks one of her promises, she loses the game. If Uruka lasts the entire \(n\) rounds without ever breaking a promise, she wins. (Promises apply to all past, present, and future plays within the game.)

---

Uruka always has a winning strategy for any given FLCI game. This is provable in RCA₀.

In fact, she can still win even if we restrict the offers that she is allowed to reject. Consider the modified game \(G_m(V, n, s)\) where Uruka is forced to accept all factorial numbers greater than \(m\). Uruka can win \(G_m(V, n, s)\) for all \(V,n,s\) and sufficiently large \(m\) (a fact provable in SMAH+, but not in any consistent fragment of SMAH).

Let \(FLCI(a)\) be the minimal \(N\) such that Uruka can win \(G_N(V, n, s)\) where all the following are less than \(a\):

• \(n, s, k\)
• the number of vectors in \(V\)
• the components of the vectors in \(V\)

関数

フリードマンが示したように、3つの関数 \(FPLCI(a)\) と \(FPCI(a)\) と \(FLCI(a)\) は極めて急に増加し、SMAHと同じ強さの部分体系で証明可能な再帰関数を支配する。ここで、フリードマンはこれらの関数を明示はしなかったが、ここに書いた定義は彼の仕事からすぐに推測できる。