数理解析研究所講究録
927 巻 1995 年 32-52

32Game Logic and its Applications I
Mamoru Kaneko
Takashi Nagashima$(_{T}^{\wedge}\underline{\mathrm{c}/}**^{\backslash })$$*$\dag er$(_{7}\grave{\tau}<\mathrm{g}\#)^{\mathrm{t}}$July 1995

Abstract
This paper provides a logic framework for investigations of game theoreticalproblems. We adopt an infinitary extension of classical predicate logic as the baselogic of the framework. The reason for an infinitary extension is to express thecommon knowledge concept explicitly. Depending upon the choice ofonthe knowledge operators, there is aof logics.
limit case is an infinitary predicate extension of modal propositional logic, and is of special interestin applications. In Part I, we develop the basic framework, and show some applications: an epistemic axiomatization of Nash equilibrium and formal undecidabilityon the playability of a game. To show the formal undecidability, we use a term
existence theorem, which will be proved in Part II.
$\mathrm{a}..\mathrm{x}\mathrm{i}_{01}\mathrm{n}\mathrm{S}$$\mathrm{h}\mathrm{i}\mathrm{e}\mathrm{r}\mathrm{a}\mathrm{r}\mathrm{c}1_{1}\mathrm{y}$$\mathrm{T}11\mathrm{e}$$I\iota’D\mathit{4}$1. Introduction
In the early stage of their literatures, game theory and mathematical logic had somecommon contributors, e.g., Zermelo, von Neumann and, and then these fields
had been developed with almost no interactions. Recently, the recognition of a possible
relationship in aims and objects between them has been reemerging. The relationshipmay be summarized as the view that game theory is a theory of human behavior insocial situations, while mathematical logic is a theory of mathematical practices byhuman beings. When we emphasize rational behavior in game theory, the relationshipis even closer. In this paper, we take this view and develop a logic framework forinvestigations of game theory.
$\mathrm{M}\mathrm{c}\mathrm{K}\mathrm{i}\mathrm{n}\mathrm{S}\mathrm{e}\mathrm{y}$The authors thank Hiroakira Ono for helpful discussions and encouragements from the early stageof this research project, and Pllillipe Mongin and Mitio Takano for comments on earlier versions of
this paper. The first and second authors are partially supported, respectively, by Tokyo Center of
Economic Research and-Aids for Scientific Research 04640215, Ministry of Education, Science
and Culture.
Institute of Socio-Economic Planning, University of Tsukuba, Ibaraki 305, Japan
Department of Mathematics, Hitotsubashi University, Kunitachi 186, Japan$\mathrm{G}\mathrm{r}\mathrm{a}\mathrm{n}\mathrm{t}_{-}\mathrm{i}\mathrm{n}$$\mathrm{t}$

$t$

33

The primary purpose of the new framework is to understand the players’ rational
decision makings and their interactions in a game situation. In a game situation, eachrational player thinks about his strategy choice, and there he may need to know andthink about the other players’ strategy choices, too, since their decisions affect thoseplayers interactively. Of course, some logical and introspective abilities are required
for such thinking. Here epistemic aspects such as knowledge, logical and introspective
abilities are entangled in the players’ decision makings. We would like to develop ourframework to encompass these features or some important part of them.
With respect to the feature of logical reasoning, we can find some literature called“epistemic logic” initiated by Hintikka [7]. Recently, epistemic logic is applied to theconsiderations of some game theoretical problems (cf., Bacharach [3] for a recent bibliography). Nevertheless, epistemic logic has been developed primarily in propositional
logic. In game theory, the use of the real number system is standard, for example,
the classical existence theorem of a Nash equilibrium in mixed strategies is proved in
the real number system (von Neumann [20] and Nash [17]). Hence we need to extend
epistemic logic to predicate logic so as to formulate some real number theory.
Another important feature is the common knowledge concept. For the decision
making of each player in a game situation, he may need to know the other players’
knowledge and thinking about the situation. These knowledge and thinking may have anested structure, e.g., he knows that the others know that he knows the game situation,and so on. This nested structure may form an infinite hierarchy, which is the problem
of common knowledge. Common knowledge on the basic description of a game as wellas on the logical and introspective abilities of the players may be required.
In the literature of epistemic logic, “fixed point logic” is developed to incorporate
the common knowledge concept into finitary epistemic logic (cf., Halpern-Moses [6] andLismont-Mongin [14] . There common knowledge is treated as a part of logic. Since
common knowledge is an infinitary concept, we choose a framework in which infinitaryconjunctions and disjunctions are allowed to express common knowledge explicitly as alogical formula, which enables us to treat common knowledge as an object of our logic
instead of a part of our logic.1 By choosing this research strategy, we can separate
the development of the logical framework from its application to a particular gametheoretical problem.
, of our framework is
As a consequence of the above desiderata, the base logic,
an infinitary extension of classical predicate logic. In this base logic, we formulate thelogical abilities of the players as well as the knowledge of a game situation. The baselogic may be regarded as the description of the logical ability of the outside investigator.
We give essentially the same logical ability to each player, which is described inside the$)$$GL_{0}$-Nagashima [9] argued in a proof theoretic manner that in a finitary logic without adding
some inference rule on the common knowledge operator, it would be impossible to define the common
knowledge concept. Segerberg [19] reached also a similar conclusion in a senlantical manner.
$\mathrm{l}\mathrm{I}\langle \mathrm{a}\mathrm{n}\mathrm{e}\mathrm{k}\mathrm{o}$34base logic. This is logic.
The next step is to give the introspective ability to each player. We assume thateach knows what he knows, described by, and also that he knows his
logical and introspective abilities. By these assumptions, we obtain logic. Whentllere is only one player, logic
coincides with the infinitary predicate extension ofmodal propositional logic.
When there are at least two players, logic
is much weaker than the extension. Here the knowledge of players about the other players’ logical andof modalintrospective abilities are necessary to introduce. We have a hierarchy of logics$GL_{p}$$\mathrm{A}_{i}(A)\supset I\iota_{i}’Ii_{i}’(A)$$GL_{1}$$GL_{1}$$I\iota’D\mathit{4}$$GL_{1}$$I\mathrm{t}\mathrm{i}D\mathit{4}$$GL_{0},$ $GL_{1},$ $GL_{2},$$\ldots$, ; and the limit$GL_{\omega}$by assuming that player
knows that player knows... player
knows the logicaland introspective abilities of the players to various degrees from $m=1$ to . When
there are at least two players, the limit
coincides with the extension of modal.
For this equivalence, we need the common knowledge of the logical and introspective
abilities of the players. Sections 2-4 are devoted for the development of these logics.
In Sections 5 and 6, we show possible applications of our framework to game theory. The first is an epistemic axiomatization of the Nash equilibrium concept. The
axiomatization includes one epistemic as pect, which leads to the common knowledgeof Nash equilibrium,, instead of Nash equilibrium itself. This axiomatization is formulated in logic
within the ordered field language. The additionalcommon knowledge operator requires us to reconsider the playability of a game and theexistence problem of aequilibrium, which is the subject of Section 6.
The existence theorem of a Nash equilibrium by von Neumann [20] and Nash [17]holds in the real closed field theory. It follows from this that the common knowledgeof the existence of a Nash equilibrium, (Nhas()), is derived from the commongknowledge of the real closed field axioms. However, the axiomatization of Section 5
states that the existence quantifier must be outside the scope of the common knowledge,, to have the playability of a game , which is deductively stronger
than. In Section 6, we prove that the playability is formally undecidable for some three-person game with a unique Nash equilibrium, that is, neither
nor
is provable from the common knowledge ofthe real closed field axioms in logic. Although this undecidability result is dependent upon the choice of a language and can be resolved by extending the language, it is
the point that the players cannot realize the necessity of such an extension, since theyknow neither positive nor negative statement.
In Part II, we will develop sequent calculi of our logics in the Genzten style, and provetlle cut-elimination theorem for them. The key theorem for the formal undecidability
result of Section 6 of Part I will be proved, using the cut-elimination theorem.
$i_{1}$$i_{m}$$i_{2}$$\omega$$GL_{\omega}$$I\iota’D\mathit{4}$$C(N\mathit{0}sh_{\mathrm{g}}(aarrow))$$GL_{\omega}$$\mathrm{N}\mathrm{a}s\mathrm{h}$$C$$\exists^{arrow}XC(NaSh_{\mathrm{g}}(^{arrow}x))$$xarrow$$\mathrm{g}$$C(\exists^{arrow}XNa\mathit{8}h\mathrm{g}(^{arrow}x))$$\mathrm{g}$$\exists xCarrow(NaSh_{\mathrm{g}}(^{arrow}x))$$arrow$$\exists x$$\neg\exists xarrow C(Nash_{\mathrm{g}}(^{arrow}x))$$GL_{\omega}$

35

and

2. Logics $GL_{0},$$GL_{p}$2.1. Base Logic$GL_{0}$$GL_{1}$

We adopt an infinitary language, based on the following list of symbols:;;
Bound variables:
Free variables:;;
Predicaies:
Functions:;
It’nowledge operators:(or), (for all),
Logical connectives: (not), $\supset(implies),$ $\wedge(and),$formulae;many
are allowed to be applied to infinitely$\mathrm{a}_{0},$$f_{0},$ $f_{1},$$\mathrm{a}_{1},$$\mathrm{x}_{0},$$\ldots$$P_{0},$ $P_{1},$$\ldots$$Ii_{1}’,$$\mathrm{x}_{1},$$\ldots$$\ldots$$Ii^{-}n$$\ldots,$$\forall$${ }$$\neg$$\exists$(exists),$\mathrm{w}\mathrm{h}\mathrm{e}\mathrm{r}\mathrm{e}\wedge \mathrm{a}\mathrm{n}\mathrm{d}$$( , )$ .

Parentheses:

The numbers of functions and predicates are arbitrary, except that there is at least
one predicate. A -ary function is an individual constant, and a -ary predicate is a
, we mean that player knows that
propositional variable. By the expression
is true.
The space of terms is defined by the standard finitary induction: (i) each free variableis
are terms, thenis a term; and (ii) if is a -ary function and if
a term.
be tlle set of all formulae generated by the standard finitary inductive defiLet
from the atomic formulae. Suppose thatandnition with respect toanis already defined $(t=0,1, \ldots)$ . We call a nonempty countable subset of,setallowable
the
an
For
variables.
offree
numberafiniteallowable set iff it contains$(\Phi)$ :and $(\Phi)$ are considered here. From the union
expressionsof formulae by the standard finitaryis an allowable set in }, we obtain the spaceby.
. We denoteandinductive definition with respect to$\wedge\{A, B\}$ and $\{A, B\}$ as $A\wedge B$
We
abbreviatea
is called formula.
An expression in
and $AB$ .
The primary reason for the infinitary language is to express common kllowledge
explicitly as a formula. The common knowledge of a formula is defined as follows:is one ofand: eachFor any $m\geq 0$ , we denote the set {is interpreted. When $m=0,$$m-1$ } byfor all $t=1,$
as the null symbol. We define the common knowledge of by
$0$

$0$

$\ell$$f_{k}$$A$$i$$Ii_{i}(\prime A)$$t_{1},$$f_{k}(t_{1}, \ldots, t_{\ell})$$t\ell$$\ldots,$$P_{0}$$\neg,$$\supset,$$\forall,$$Ii_{1,\ldots,n}^{r}Ii^{r}$$\exists$$\Phi$$P_{t}$$\mathcal{P}_{t}$$\Phi$$P_{t}\cup\{(\wedge\Phi),$$(\wedge\Phi)$$\Phi$$\mathcal{P}_{t+1}$$\prime p_{t}$$\neg,$$\supset,\forall,$$\exists$$I_{1}’n$$fi_{1}’,$$P_{\omega}$$\bigcup_{t<\omega}\mathcal{P}_{t}$$\ldots,$$\prime \mathcal{P}_{(v}$$A$$Ii_{i_{1}}’Ii’i_{2}\cdots K_{i_{m}}$$Ii_{n}^{r}$$I\mathrm{i}_{1}’,$$I\zeta_{i_{t}}$$\ldots,$’$i_{t}\neq i_{t+1}$$\mathrm{K}(m)^{2}$$I\mathrm{i}_{i_{1}}’Ii^{\vee}i_{2}\cdots Ii_{i_{m}}$$\ldots,$$A$$\wedge\{K(A) : I1^{r}\in t\bigcup_{<\omega}\mathrm{K}(t)\}$which we denote by $C(A)$ . If is inclosed with respect to the operation$A$

2The requirement$i_{t}\neq i_{t+1}$

for all $t=1,$$\mathcal{P}_{m}$,, then $C(A)$ is in.

$\mathcal{P}_{m+1}$. Hence the space$C(\cdot)$$\ldots,$$m-1$ will be used in Part II.

$\mathcal{P}_{\omega}$

is

36

is defined by the following seven axiom schemata and five inference
Base logic
rules: For any formulae $A,$ $B,$ , allowable set , and term ,$GL_{0}$$C$:$(L2)$ :$(L.3)$ :$(L4)$ :$(L1)$$(L5)$ ::$(L7)$ :$(L6)$$A\supset(B\supset A)$$\Phi$$t$;$(A\supset(B\supset C))\supset((A\supset B)\supset(A\supset C))$;$(\neg A\supset\neg B)\supset((\neg A\supset B)\supset A)_{1}$, where $A\in\Phi$ ;$A\supset\Phi$ , where $A\in\Phi$ ;$\forall xA(x)\supset A(t)$ ;$A(t)\supset\exists xA(x)$ ;$\wedge\Phi\supset A$$\frac{A\supset BA}{B}(hIP)$( -Rule)$\frac{\{A\supset B.B\in\Phi\}}{A\supset\wedge\Phi}$$\frac{A\supset B(a)}{A\supset\forall xB(X)}$$\frac{\{A\supset B.A\in\Phi\}}{\Phi\supset B}$$\wedge$( -Rule)$\forall$$\frac{A(a)\supset B}{\exists xA(X)\supset B}$( -Rule)${ }$( -Rule),$\exists$

where the free variable must not occur in $A\supset\forall xB(x)$ and $\exists xA(x)\supset B$ of ( -Rule)and ( -Rule).
Letbe an empty or allowable set anda formula. A proof of
from
is a
countable tree with theproperties: (i) every path from the root is finite; (ii)a formula is associated with each node, and the formula associated with each leaf is an
instance of $(L1)-(L7)$ or a formula in ; and (iii) adjoining nodes together with theirassociated formulae form an instance of the above inferences. For any subset of,, iff there is an allowable subset of
a formula is provable from , denoted by
and a proof of from .
is an infinitary extension of finitary classical predicate logic. Hence we
Logic
can freely use provable finitary formulae in classical logic. In fact, it is sound andcomplete with respect to the standard interpretation with infinitary conjunctions anddisjunctions. That is, all valid formulae in this sense are provable, and vice versa. We
just mention the deduction theorem for the purpose of comparisons with modal logic.
The above formula (3) is needed to prove this lemma.
$a$$\forall$$\exists$$A$$\Phi$$A$$\Phi$$\mathrm{f}\mathrm{o}\dot{1}\mathrm{l}\mathrm{o}\mathrm{w}\mathrm{i}\mathrm{n}\mathrm{g}$$\Phi$$\Gamma$$A$$\Gamma$$A$$\Gamma$$\mathcal{P}_{\mathrm{t}v}$$\Phi$$\Gamma\vdash_{0}A$$\Phi$$GL_{0}$

Lemma 2.1 (Deduction Theorem). Let be a closed formula. If,.
thencan be regarded as a fragment of infinitary logic
Our base logic(except theaddition of multiple knowledge operator symbols) (cf.,and Keisler [12]). As, is much smaller than the space of formulae in
a space of formulae,. Since our
purposeprimaryof the infinitary extension is to express common knowledge explicitly
as a formula, the present extension suffices for our purpose.
$A$$\Gamma\cup\{A\}\vdash_{0}B$$\Gamma\vdash_{0}A\supset B$$GL_{0}$$L_{\omega_{1}\omega}$$\mathrm{I}<\mathrm{a}\mathrm{r}\mathrm{p}[11]$$\mathcal{P}_{\mathrm{t}v}$$L_{\omega_{1^{(v}}}$

37

2.2. Logic$GL_{p}$: Players’ Logical Abilities

may be regarded as a description of the logical ability of the outside theorist,
Logic. In this subsection, we will give each player essentiallywhom we call theand provethe same logical ability as the investigator’s. That is, we define logic
that each player is given the same logical ability as the investigator’s.
knows the logical axioms $L1-L7$ . For
We as sume that each player $i=1,$
example, the knowledge of $L1$ is described as $I\iota_{i}’(A\supset(B\supset A))$ , which is denoted by. Similarly, we define $L2_{i}-L7_{i}$ . We also assume that each player has the inference
ability corresponding to $hfP$ , ( -Rule), ( -Rule), ( -Rule), ( -Rule):$GL_{0}$$inve\mathit{8}tigat_{\mathit{0}}r$$GL_{p}$$\ldots,$$n$$L1_{i}$$(MP_{i})$:$Ii_{i}’(A\supset B)\wedge Ii_{i(A)}’\supset Ii_{i}’(B)$:$(_{i})$ :$(\exists_{i})$

:
:

;
;
;

$I\mathrm{i}_{i}’(\wedge \mathrm{t}A\supset B:B\in\Phi\})\supset Ii_{i}’(A\supset\wedge\Phi)$$( \bigwedge_{i})$$(\forall_{i})$$\exists$$\forall$${ }$$\wedge$$I\mathrm{i}_{i}’(\wedge\{A\supset B : A\in\Phi\})\supset Ii_{i}’(\Phi\supset B)$$I_{1_{i}^{\vee}}’(\forall X(A\supset B(x)))\supset Ii_{i}’(A\supset\forall xB(X))$$I\mathrm{i}_{i}’(\forall x(A(x)\supset B))\supset I\mathrm{i}_{i}’(\exists xA(x)\supset B)$;,

where $A,$ are any formulae, an allowable set, and a bound variable.
The above schemata are reformulations of inference rules $MP-$ ( -Rule). Here theinvestigator has the description of the logical ability of each player , and can deduce
what player may deduce. This description is made in the object language, while theinvestigator’s logical ability is described in the metalanguage.
For the connection between the investigator’s and the players’ knowledge, we makethe minimum requirement:
$B$

$x$

$\Phi$$\exists$

$i$

$i$

$(\perp_{i})$:$\urcorner K_{i}(\neg A\wedge A)$,. This requires that no contradiction be derived
where is any formula and $i=1,$
basic knowledge.
from player
We add one more axiom, which we call the Barcan axiom:$A$$\ldots,$$n$$i’ \mathrm{s}$$(\wedge- B_{i})$:$\wedge Ii_{i(\Phi}’$)$\supset I\zeta_{i}(\wedge\Phi)$,isdenotes the set $\{Ii_{i(A}’) : A\in\Phi\}$ . Whenis an allowable set andwhere
finite, this is derived from other axioms, but is needed for infinite . For the development
will be used to derive the property:of our framework,$\Phi$$I\zeta_{i}(\Phi)$$\Phi$$\Phi$$(\wedge- B_{i})$$C(A)\supset I\iota’\dot{‘}(C(A))$

This will be provable in$GL_{1}$

for $i=1,$$\ldots,$

$n$

.

(2.1)

and play an important role in game theoretic applications.

38

Logic
is defined by the sets of all instances of $L1_{i}-L7_{i},$and, denoted by, for $i=1,$. That is, for any set of formulae and any
formula , we define theinby$(MP_{i})-(\exists_{i}),$ $(\perp_{i})$$GL_{\mathrm{p}}$$(\wedge- B_{i})$$\triangle_{i\mathrm{p}}$$\ldots,$

$A$

$n$

$\Gamma$$GL_{p}$$\mathrm{p}\mathrm{r}\mathrm{o}\mathrm{V}\mathrm{a}\mathrm{b}\mathrm{i}\mathrm{l}\mathrm{i}\mathrm{t}\mathrm{y}\vdash_{p}$$\Gamma\vdash_{p}$

iff

$A$

$\Gamma\cup(\bigcup_{i}\triangle_{ip})\vdash_{0}$

A.

(2.2)

, the investigator deduces
Whenfrom , using his knowledge of
logicalability described byas well as using player
knowledge. When,the investigator deduces that player deduces from the basic knowledge of player .
The following proposition states that each player is given the same logical ability as theinvestigator’s.
$A$$\Gamma\vdash_{\mathrm{p}}A$$\Gamma$$i’ \mathrm{s}$$i’ \mathrm{s}$$\triangle_{\mathrm{c}p}$$Ii_{i}’(\mathrm{r})\vdash_{p}I_{1_{i}}’(A)$

$A$

$i$

Proposition 2.2 (Faithful Representation). Let
Then
if and only if.

$i$$\Gamma$be a set of closed formulae.

$\Gamma\vdash_{0}A$$Ii_{i}^{r}(\Gamma)\vdash_{p}I\mathrm{i}_{i}^{\vee}(A)$is sound and complete, the logical ability of each player is also complete
Since
in the sense of the infinitary extension of classical logic.
has the following properties.
$GL_{0}$$\mathrm{P}\mathrm{r}\mathrm{o}\mathrm{v}\mathrm{a}\mathrm{b}\mathrm{i}\mathrm{l}\mathrm{i}\mathrm{t}\mathrm{y}\vdash_{\rho}$

Proposition 2.3. Let
bound variable. Then$(\wedge)$:$A$

be a formula,$\vdash_{p}Ii_{i}^{r}(\wedge\Phi)\supset\subset\wedge K_{i}(\Phi)$$()$ :$\vdash_{p}\mathrm{V}I\iota’i(\Phi)\supset Ii_{i}^{r}(\mathrm{V}\Phi)$

$x$

a

;

:

$\vdash_{p}Ii_{i}^{r}(\forall XA(X))\supset\forall xI\mathrm{I}_{i}^{r}(A(x))$;$(\exists)$:$\vdash_{p}\exists x\mathrm{A}_{i}’(A(x))\supset Ii_{i}^{r}(\exists XA(X))$.

$GL_{1}$an allowable set of formulae, and;$(\forall)$

2.3. Logic$\Phi$: Players’ Logical and Introspective Abilities, as was shown in Proposition 2.2, each player has the same logical ability
In logic
as the investigator. Nevertheless, he may know neither his own logical ability nor what
he knows. We define another logic
by adding introspective abilities of players.
Introspective abilities consists of two parts: (i) if a player knows , then he knows that
he knows ; and (ii) he knows his logical and introspective abilities themselves. The
addition of these introspective abilities to our framework is desirable for several reasons.
Formally, the following, called the Positive Introspection axiom, describes (i):$GL_{p}$$GL_{1}$$A$$A$$(PI_{i})$:$Ii_{i}^{r}(A)\supset I\zeta_{i}I\zeta_{i}(A)$,where is a formula. The second requirement (ii) is obtained by putting
to eachformula inand of. That is, we denote the union ofand the set of all$A$$Ii_{i}^{r}$$\triangle_{ip}$$(PI_{i})$$\triangle_{i\rho}$

39

instances of $(PI_{i})(i=1, \ldots, n)$ by
by
define the $provability\vdash_{1}$ in$\triangle_{i0}$, and denote$\triangle_{i0}\cup\{Ii_{i(A)}’ :A\in\triangle_{i0}\}$by$\triangle_{i1}$. We$GL_{1}$$\Gamma\vdash_{1}$

$A$

iff

(2.3)

A.

$\Gamma\cup(\bigcup_{i}\triangle_{i1})\vdash_{0}$In this logic, (2.1) is provable, that is,

Lemma 2.4.

$\vdash_{1}C(A)\supset Ii^{r_{i}}(C(A))$

for any $i=1,$$\ldots,$$n$.

As was stated, Lemma 2.4 is not necessarily proved without the Barcan axiom. This will be discussed briefly in Part II.
is of special interests, since it can be regarded as an infinitary predicate
Logicwhen there is only one player, i.e., $n=1$ . We define
extension of modal logic
andby adding $(MP_{i}),$$(\wedge-$$B_{i})$$GL_{1}$$I\mathrm{f}D\mathit{4}$$(\wedge- B_{i}),$$\mathrm{p}\mathrm{r}\mathrm{o}\mathrm{V}\mathrm{a}\mathrm{b}\mathrm{i}\mathrm{l}\mathrm{i}\mathrm{t}\mathrm{y}\vdash_{I\iota’D}\mathit{4}\mathrm{f}\mathrm{r}\mathrm{o}\mathrm{m}\vdash_{0}$$(PI_{i})$(Necessitation)$, \frac{A}{\mathrm{A}_{i}(A)}$for $i=1,$$(\perp_{i}),$.

$n^{3}$$\ldots,$

Proposition 2.5. Let $n=1$ . Let
if and only
a formula. Then$\Phi\vdash_{1}$$A$$\Phi$

be an allowable set of closed formulae, and.

$A$$\mathrm{i}\mathrm{f}\vdash_{I\mathrm{t}^{r}D\mathit{4}}\wedge\Phi\supset A$

is
When $n\geq 2$ , this relationship breaks down. For example,. To have the equivalence between them, we need to assume thatnot provable inis common knowledge among the players. This means that there
every formula in. This is the subject of Section 3.
tois an infinite hierarchy from
$Ii_{2}’I\iota_{1}^{\nearrow}(A\supset(B\supset A))$

$GL_{1}$$\bigcup_{i}\triangle_{i1}$$\vdash_{1}$$\vdash_{ICD\mathit{4}}$3. Iterated Knowledge of Deductive Abilities
with at least two players, each player does not know the other players’Inlogical and introspective abilities, though he has his own. Once a player knows theirabilities, it would be possible for him to infer what the others deductively know. Thisknowledge of players’ logical and introspective abilities may have a nested structure,knows those abilities. Thus
knows...
knows that player
for example, player
there is an infinite hierarchy of logics with the various degrees of nestedness. Whencoincides with the infinitary predicate
there are at least two players, only the limit
extension of modal propositional logic ICD4. This limit case is particularly importantfor our applications to game theory in Sections 5 and 6.
$1_{0_{\circ}^{\sigma}}\mathrm{i}_{\mathrm{C}}GL_{1}$$i_{m}$$i_{2}$$i_{1}$$GL_{\omega}$

3Axioms$( \bigwedge_{i}),$$(.),$$(\forall:)$and$(\exists:)$

are derived in$\mathrm{t}1_{1}\mathrm{i}\mathrm{s}$extension.

40

3.1. Game Logics $GL_{m}(0\leq m\leq\omega)$

The idea that a player knows his and the others’ logical and introspective abilities isis known to the players in the nested
described by assuming that every formula inbyfor anymanner. Define$\bigcup_{i}\triangle_{i1}$$m\leq\omega$$\triangle_{m}${$\triangle_{m}=$Let$\Gamma$.

$K(A):A \in\bigcup_{1}$$\triangle_{i1}$be a set of formulae. Then we define the$\Gamma\vdash_{m}$

$A$

iff

and

$I \mathrm{i}^{r}\in\bigcup_{t<m}\mathrm{K}(t)$$\mathrm{p}\mathrm{r}\mathrm{o}\mathrm{v}\mathrm{a}\mathrm{b}\mathrm{i}\mathrm{l}\mathrm{i}\mathrm{t}\mathrm{y}\vdash_{m}$$\Gamma\cup\triangle_{m}\vdash_{0}$

}.

(3.1)

in logic $GL_{m}$ by

A.

(3.2)

imply
.
Of course, $m<k$ andIn logic $GL_{m}(m<\omega)$ , the players know the logical and introspective abilities ofthe players up to the depth in the sense that player knows that player knows.s.
, the players know the abilities up to any
that player
knows those abilities. In. That is, the abilities of players are common knowledge among the players.
First, we give some lists of provable formulae in $GL_{m}$ .
$A$$\Gamma\vdash_{m}$$\Gamma\vdash_{k}A$$m$$i_{1}$$i_{2}$$GL_{\omega}$$i_{m}$$\mathrm{d}\mathrm{e}\mathrm{p}\dot{\mathrm{t}}\mathrm{h}$:Proposition 3.1. For any $m$ with $1\leq m\leq\omega$ and any
and$i=1,$,$\vdash_{m}L(A\supset B)\wedge L(A)\supset L(B)$ ;$(MP_{L})$ :: $\vdash_{m}L(\wedge\{A\supset B:B\in\Phi\})\supset L(A\supset\wedge\Phi)$ ;$\vdash_{m}L(\wedge\{A\supset B : A\in\Phi\}\supset L(\Phi\supset B)$ ;$(_{L})$ :: $\vdash_{m}L(\forall x(A\supset B(x)))\supset L(A\supset\forall xB(X))$ ;: $\vdash_{m}L(\forall x(A(x)\supset B))\supset L(\exists xA(x)\supset B)$ ;$(1_{L})$ :
(
A );
;
:
$(PI_{L})$ :$\vdash_{m}L(A)\supset LK_{i}(A)$ ,where $A,$ are formulae, an allowable set, $L(\Phi)$ the set $\{L(C) : C\in\Phi\}$ , and abound variable.
$L\in\{I\mathrm{f}I\zeta_{i}$$\ldots,$$K \in\bigcup_{t<m}\mathrm{K}(t)$$n\}$$( \bigwedge_{L})$$(\forall_{L})$$(\exists_{L})$$\vdash_{m^{\neg}}L$$(B_{L})$$\neg A$$A$$\vdash_{m}\wedge L(\Phi)\supset L(\wedge\Phi)$$B$$\Phi$$x$, these hold for the common knowledge operator
Note that inin the replacement of .
Observe that the claims of this proposition are parallel to the axioms,
by . The formulae corresponding to $L1_{i}-L7_{i}$ , e.g.,:with the replacement of$L(A\supset(B\supset A))$ , belong toby (3.1). Hence, by substituting
forin theassertions of Proposition 2.3, we have the following.
$GL_{\omega}$$C(\cdot)$$L$$I1/IP:-(PI_{\mathrm{i}})$$Ii_{i}^{r}$$L$$L1_{L}$$L$$\triangle_{m}$Proposition 3.2. For any $m$ with $1\leq m\leq\omega$ and any
and $i=1,$$\ldots,$$n$},$L\in\{I\zeta I\zeta_{i}$:$I_{1_{i}}’$$I \mathrm{i}^{\vee}\in\bigcup_{t<m}\mathrm{K}(i)$41:$(_{L})$ :::where $A,$$\vdash_{m}L(\wedge\Phi)\supset\subset\wedge L(\Phi)$$( \bigwedge_{L})$$(\forall_{L})$$(\exists_{L})$$\vdash_{m}L(\Phi)\supset L(\Phi)$;;;$\vdash_{m}\exists xL(A(X))\supset L(\exists xA(X))$ ,$\vdash_{m}L(\forall xA(x))\supset\forall xL(A(X))$$B$

are formulae,$\Phi$an allowable set, and$x$a bound variable.

Thus the same asymmetry as Proposition 2.3 appears in $GL_{m}$ . This asymmetry
remains for the common knowledge formula, that is,:$(_{C})$ :::$( \bigwedge_{C})$$\vdash_{\omega}C(\wedge\Phi)\supset\subset\wedge C(\Phi)$$\vdash_{\omega}C(\Phi)\supset C(\Phi)$;;$(\forall c)$$\vdash_{\omega}C(\forall xA(x))\supset\forall xC(A(X))$$(\exists c)$$\vdash_{\omega}\exists xC(A(x))\supset C(\exists xA(x))$;,

where $C(\Phi)$ is the set $\{C(B) : B\in\Phi\}$ . Especially,
Section 6.
The following properties hold on common knowledge.

$(\exists c)$

be a set of formulae, and a formula. Then
;
imply
;
implies.
if and only if

Proposition 3.3. Let$\Gamma\vdash A$$C(\Gamma)\vdash_{\omega}$$A$$\Gamma$$1)(\mathrm{N}\mathrm{e}\mathrm{C}\mathrm{e}\mathrm{S}\mathrm{S}\mathrm{i}\mathrm{t}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}):C(\Gamma)\vdash_{\omega}$

2):
3):

plays an important role in$A$$C(\Gamma)\vdash I\omega i^{r}i(A)$$C(\Gamma)\vdash_{\omega}C(A)$$C(\Gamma)\vdash_{\omega}C(A)$$A$

3.2. Relationship to Modal Logic

As was already mentioned, when $n\geq 2$ , we need to go to the limit.
comparison to modal logic$GL_{\omega}$

to make a direct$I\mathrm{f}D\mathit{4}$Proposition 3.4. Let $n\geq 2$ . Let
if and only if
a formula. Then$\Phi\vdash_{\omega}$$A$$\Phi$

be an allowable set of closed formulae, and$\vdash_{J\mathrm{i}’D\mathit{4}}\wedge\Phi\supset A$$A$.

Thus when we assume the common knowledge of the logical and introspective abil, it becomes equivalent to the infinitary predicate
ities of the players, our logic,.
extension of
Proposition 3.4 as well as Proposition 2.5 hold in the finitary fragment of our framework. Hence these are not dependent upon the infinitary extension.
$GL_{\omega}$$I\mathrm{f}D\mathit{4}$42

4. Conservativeness of $GL_{m}(1\leq m\leq\omega)$
A formula is said to be nonepistemic iff it does not contain any. Let, which is, more precisely,
be the formula obtained from by eliminating all
defined by induction on the structure of a formula. We denote $\{\epsilon A : A\in\Phi\}$ by
is provable in, for example,. Observing that any formula in, we have the following proposition.
is$A$$Ii_{1}’,$$\epsilon A$$Ii_{n}’$$\ldots,$$A$$K_{1},$$I\zeta_{n}$$\ldots,$$\epsilon\Phi$$GL_{0}$$\epsilon\triangle_{m}$$B)\wedge Ii^{r_{\mathrm{i}()}}A\supset I\iota_{i}’(B))$

Proposition 4.1 (Conservative Extension). Let
impliesformula in. Then.
$\Gamma\vdash_{m}$$\mathcal{P}_{\omega}$$\epsilon(K_{i}(A\supset$$(\epsilon A\supset\epsilon B)\wedge\epsilon A\supset\epsilon B$$A$

be a subset of$\Gamma$$P_{\omega}$

and

$A$

a

$\epsilon\Gamma\vdash_{0}\epsilon A$

The next proposition follows immediately from Proposition 4.1. The consistency ofwill follow from the cut-elimination theorem forin Part II.

$GL_{0}$$GL_{0}$

Proposition 4.2 (Relative Consistency). Let
be a subset of, then is consistent with respectconsistent with respect.
$\Gamma$$\mathrm{t}\mathrm{o}\vdash_{0}$$\Gamma$

The following fact will be important in Section 6: Let
formulae and a nonepistemic formula. Then$\mathcal{P}_{\omega}$. If$\epsilon\Gamma$is$\mathrm{t}\mathrm{o}\vdash_{m}$$\Gamma$be a set of nonepistemic$A$$C(\Gamma)\vdash_{\omega^{\neg}}\exists x_{1}\ldots\exists X_{\ell}C(A(x_{1}, \ldots, X\ell))$

if and only if$C(\Gamma)\vdash_{\omega}C(\urcorner\exists x_{1}\ldots\exists X\ell A(X_{1}, \ldots, x\ell))$

(4.1)

.

In contrast withof Section 3, there is no distinction between these two llegative
existential statements.
$(\exists c)$

5. Applications to Game Theory I: Epistemic Axiomatization of$\mathrm{N}\mathrm{a}\mathrm{s}\mathrm{l}_{1}$Equilibrium
This and following sections provide applications of our framework to game theory. Sinceclassical game theory is described in the real number system, we need to specify alanguage and axioms for a real number theory. We use the standard language and axioms
for the ordered field theory in this section, and will use the real closed field theory in
Section 6. These are sufficient for the consideration of classical game theory. This section
gives an epistemic axiomatization of Nash equilibrium, based on Kaneko-Nagashima .
$[8]^{4}$4We can find some axiomatizations of Nash equilibrium in the recent game theoretical literature.
Related papers are: Bacharach [2] made some axiomatic requirements for individual decision making
in a game situation, and proved that such requirements are inconsistent even for a game with a unique
Nash equilibrium. Aumann [1] gave an epistemic consideration of Nash equilibrium in a game withperfect information. Balkenborg-Winter [4] showed that common knowledge is not necessary in the caseof a game with perfect information. This should be compared with our epistemic axiomatization. For
other related game theoretical problems, see Kaneko-Nagashima [8].

43

The result of the axiomatization deviates slightly from Nash equilibrium in classicalgame theory in that it is the common knowledge of Nash equilibrium. This can be
regarded rather as faithful to the intended interpretation of Nash equilibrium in gametheory. But this additional common knowledge operator requires us to reconsider adeeper problem of the playability of a game, which will be the subject of Section 6.
. The consideration of the present
In these two sections, we use game logic
section cannot be done in logic $GL_{m}$ for finite $m$ . In fact, the ordered field axioms are
not used in this section, but the ordered field language suffices for the present purpose.
equilibrium, which is the subject of Section 6, we
For the existence problem of a
use those axioms.
$GL_{\omega}$$\mathrm{N}\mathrm{a}s\mathrm{h}$5.1. Language and Basic Game Theoretic Concepts
Here we specify the list of basic symbols:, /;predicates:

Binary functions: $+,$ $-$ ,Constants: $0,1$ ;Binary predicates:$\geq,$ $=$; and$\ell-a\Gamma y$$D_{n}$$D_{1},$$\ldots,$,

in addition to the other basic symbols specified in Section 2. The l-ary predicatesare prepared for the epistemic consideration of Nash equilibrium. The otherprepared for the description of the ordered field theory. We denote thearesymbols(cf., Mendelson [15], [16]).
set of all ordered field axioms and equality axioms bywhich should not cause
equalities,
informalandformalsymbol
same
the
use
We
confusions.
First, we describe a noncooperative game in informal mathematics. Consider an-person finite game . For simplicity, we assume that each player has the same finite
number, , of pure strategies. The payoff to player from a pure strategy combination. The game of Table 1 is called
is given as a rational number(not confess)the “Prisoner’s dilemma”, where each player has two pure strategies
players, e.g.,tothepayoffs
of
pair
a
table
is
the
in
vector(confess). Eachand. We allow also mixed strategies, where a mixed strategy
over his pure strategies.
distribution
probabilityaisfor player$D_{1},$$D_{n}$$\ldots,$$\Phi_{\mathrm{o}\mathrm{f}}$$=\mathrm{f}\mathrm{o}\mathrm{r}$$n$$\mathrm{g}$$i$$\ell$$\mathrm{g}_{i}(s_{1}, \ldots, \mathit{8}_{\mathcal{R}})$$(s_{1}, \ldots, s_{n})$$f\mathrm{V}$$C$$(\mathrm{g}_{1}(N, C),\mathrm{g}2(\mathit{1}\mathrm{V}, C))=(1,6)$
$i$

$N$

$C$

$B$

$M$

$N$

$(5,5)$$(1,6)$$B$$(2,1)$$(0,0)$$C$$(6,1)$$(2,2)$$M$$(0,0)$$(1,2)$

Table 2
Table 1
Now we formulate those game theoretical concepts in our formal language. First,
we define numerals as follows: $[0]$ is $0,$ $[m]$ is $[m-1]+1$ for an positive integer $m$ , and$[m]$ is $0-[-m]$ for a negative integer $m$ . For a rational number $q=m/k(m/k$ are
irreducible and $k>1$ ), we define $[q]$ to be $[m]/[k]$ . Thus numerals are closed terms.

44

Using numerals, the above game is described in our language as follows: the payoff
to player from a strategy combination
is given as. A mixed
strategy for player is a vector of freesatisfying the following
formula:$\mathrm{g}$$i$$(s_{1}, \ldots, s_{n})$$i$$[\mathrm{g}i(s1, \ldots, sn)]$$\mathrm{v}\mathrm{a}\mathrm{r}\mathrm{i}\mathrm{a}\mathrm{b}\mathrm{l}\mathrm{e}\mathrm{s}a_{i}arrow=(a_{i1}, \ldots, a_{i}\ell)$$( \sum_{t=1}^{\ell}a_{i}t=1)\wedge(\wedge\{a_{it}\geq 0 :which we denote by$St(^{arrow}a_{i})$t=1, \ldots, \ell\})$

,

(5.1)

. Next, the payoff to player from a mixed strategy combina$i$

is given as the expected payoff with respect to the probability
distribution over the pure strategy combinations
induced:$tionarrow a=(a_{1}\ldots,a_{n})arrow,arrow$$(s_{1}, \ldots, s_{n})$$\sum_{t_{1}}$which we denote by...

$\mathrm{b}.\mathrm{v}arrow a$

,

(5.2)

$\sum_{t_{n}}a1t_{1}.\ldots\cdot atnn.[\mathrm{g}i(st1’\ldots, s_{t_{n}})]$. Note that thisis a term. In the following, we denote, anditself.
Now we have the basic description of a game with mixed strategies. Finally, weformulate the Nash equilibrium concept introduced by Nash [17] as a generalization of
the maximin strategy of von Neumann [20], which has been playing the central role in
the literature of game theory. A lVash equilibrium is defined to be a mixed strategy
satisfying the following formula:$g_{i}(a)arrow$$g_{i}(a)arrow$$arrow \mathrm{m}\mathrm{e}\mathrm{a}\mathrm{n}\mathrm{s}arrow a$$(arrow a_{i};a-i)$$(\overline{a}_{1}, \ldots,a_{i-}1,ai+1, \ldots,an)arrowarrowarrow \mathrm{b}\mathrm{y}aarrow-i$$\mathrm{g}$$\mathrm{c}\mathrm{o}\mathrm{m}\mathrm{b}\mathrm{i}\mathrm{n}\mathrm{a}\mathrm{t}\mathrm{i}_{\mathrm{o}\mathrm{n}}arrow a=(a_{1}, \ldots,a_{n})arrowarrow$$\wedge\{St(a_{i})arrow\wedge(\forall^{arrow}X_{i}(St(X_{i}arrow)\supset g_{i}(aarrow)\geq g_{i}(_{X_{i}}^{arrow};a-i)):i=1, \ldots, n\}$

where
note

$\forall x_{i}Aarrow(^{arrow}x_{i})$means$\forall x_{i1}\ldots\forall x_{i}\ell A(xi1, \ldots, X_{i\ell})$$\exists x_{i1}\ldots\exists x_{i}\ell A(Xi1, \ldots, xi\ell)$$J\mathrm{V}ash_{\mathrm{g}}(^{arrow}a_{1}, \ldots,a_{n})arrow$

and, later,$\exists x_{i}Aarrow(x_{i}arrow)$. We denote the formula of (5.3) by

,

(5.3)

is used to deor

$Nash_{\mathrm{g}}(\overline{a})$. Note that this is a formula relative to a specific game .
$\mathrm{g}$The prisoner’s dilemma has a unique Nash equilibrium $(C, C)$ even in mixed strategies (the formal counterpart is $((0,1),$ $(0,1))$ ). The game of Table 2, called “the Battleof Sexes”, has three equilibria, $(B, B),$ $(M, M)$ and $((2/3,1/3),$ $(1/3,2/3))$ (the formal
counterparts are $((1,0),$ $(1,0)),$ $((0,1),$ $(0,1))$ and $(([2/3], [1/3]), ([1/3], [2/3]))$ .
5.2. Infinite Regress of the Knowledge of Final Decision Axioms and its
Solution

In a game , each player deliberates his and the others’ strategy choices and may reacha final decision. The expression
describes a strategy
finally reached
by a player. We would like to characterize this “final decision”
operationally by
the following four axioms: for $j=1,$(
may be the same),$\mathrm{g}$$D_{i}(a_{i})arrow$$\mathrm{d}\mathrm{e}\mathrm{c}\mathrm{i}\mathrm{S}\mathrm{i}_{0}\mathrm{n}arrow a_{i}$$D_{i}(a_{i}arrow)$$i,$$\ldots,$$D1$:$\forall x_{i}(arrow Di(x_{i})arrow\supset St(^{arrow}X_{i}))$;$n$$i,$ $j$

45

;

$D2$

:

$\forall x_{1\cdots n}arrow\forall^{arrow}X[\bigwedge_{j}^{n}=1jD(xarrow)j\supset\forall^{arrow}y_{i}(s_{t}(arrow y_{i})\supset gi(^{arrow}x)\geq g_{i}(y_{i;}arrowarrow x_{-}i))]$

$D3$

:

$\exists x_{i}D_{i}arrow(^{arrow}x_{i})\supset\exists xjDarrow(^{arrow}jXj)$

$D4$

:

$\forall xi[arrow Di(xarrow)i\supset Ii_{j}^{r}(D_{i}(^{arrow}x_{i}))]$;.

is a final decision for player , then $D1$ : it is a strategy; $D2$ : given
These mean:
maximizes his payoff; $D3$ : any other player reaches
the others’ final
also a final decision; and $D4$ : all players know that player reaches his final decision. Although each axiom has several formulae, we mean the conjunction of them by
each. We denote $D1\wedge D2\wedge D3$ A $D4$ by $D(1-4)$ .
Axioms $D1$ and $D2$ is apparently related to Nash equilibrium, indeed,$i$$\mathrm{i}\mathrm{f}x_{i}arrow$$j$$\mathrm{d}\mathrm{e}\mathrm{c}\mathrm{i}\mathrm{s}\mathrm{i}\mathrm{o}\mathrm{n}\mathrm{s}xarrowarrow-i,x_{i}$$i$$arrow x_{i}$$D1,$ $D2 \vdash_{\omega}\bigwedge_{i=1}^{n}D(ai)arrow\supset Nash(^{arrow}\mathrm{g}a)$

.

(5.4)

Axiom $D3$ plays a role for independence of individual choice. Axiom $D4$ is an epistemic
condition and has not been explicitly discussed in game theory. In fact, the explicit
consideration of $D4$ leads to an infinite regress of the knowledge of these axioms.
, we find, by looking at
Although those axioms are intended to determine$D4$carefully, that the above axioms are insufficient in the following sense. Axiom
Axiom$D4$ requires that each player know his and the other player’s final decisions, but thisrequirement could not be fulfilled unless the meaning of “final decisions” is given to theplayers. In fact, the meaning should be given by the above four axioms. Therefore we. Then it
for $i=1,$, i.e.,
assume that each player knows theseholds that.
$D_{i}(^{arrow}a_{i})$$\mathrm{a}_{\lrcorner}\mathrm{x}\mathrm{i}\mathrm{o}\mathrm{m}\mathrm{S}$$I\mathrm{f}_{i}(D(1-4))$$\ldots,$$n$$D(1-4),\wedge I\zeta_{\ell}(D(1-4)\ell=1n)\vdash_{\omega}D_{i}(^{arrow}a_{i})\supset I\zeta_{j}Ii_{t}^{r}(Di(^{arrow}a_{i}))$is a final
Again, we have a problem: player in the mind of player knows
decision for player , but he is not given the meaning of “final decisions”. Thus weneed to assume $Ii_{j}’Ii’t(D(1-4))$ , but meet the same problem as above, that is, it holds
and $m<\omega$ ,in general that for any$\mathrm{t}\mathrm{h}\mathrm{a}\mathrm{t}arrow a_{i}$

$j$

$t$

$i$

$K\in \mathrm{K}(m)$$\{L(D(1-4)) :L\in t<\cup \mathrm{K}(t)\}\vdash D\omega i(^{arrow}a_{i})\supset K(D_{i}(arrow)ai)m$

.

(5.5)

Thus when we assume $L(D(1^{-}4))$ for all of depth up to $m-1$ , it is required that theof the depth $m$ . Henceis known to the players in the sense of
meaning of
we need to add $L(D(1^{-}4))$ for of depth $m$ : we have the same problem as before.
To avoid this problem, we assume $\{K(D(1^{-}4)) : Ii^{r}\in\bigcup_{m<\omega}\mathrm{K}(m)\}$ . Thus we meet an$L$$I\iota’$$D_{i}(a_{i})arrow$

$L$

46

infinite regress, which forms the common knowledge of $D(1-4)$ , i.e., $C(D(1- 4))^{5}$. We
will solve this infinite regress.
Now we have the following proposition.

Proposition 5.1.1):
2):;$C(D(1-4)) \vdash_{\omega}\bigwedge_{i=1}^{n}Di(a_{i})arrow\supset C(Nash\mathrm{g}(^{arrow}a))$$C(D(1-4))\vdash_{\omega}D_{i}(^{arrow}ai)\supset\exists^{arrow}x{}_{-i}C(Nash\mathrm{g}(arrowarrow ai;X-i))$

In fact, the formula,$C(D(1^{-}4))$ for a solvable game. A gameiff the following holds:.

, can be regarded as the solution ofis called a solvable (in the sense of Nash [17])$\exists xarrow {}_{-i}C(NaSh(^{arrow}\mathrm{g}a_{i};X-i) arrow)$$\mathrm{g}$$\forall\overline{x}_{1}\ldots\forall^{arrow}X_{n}[\wedge(\exists y-iNaSh(^{arrow}iarrow \mathrm{g}x_{i};y-i))\supset Nash_{\mathrm{g}}(_{X}^{arrow})]$

.

(5.6)

This is satisfied by the game of Table 1 but not by that of Table 2. We denote thisformula by SOLV. Of course, when the game has a unique Nash equilibrium, this issatisfied.
By the expression $C(D(1-4))[A_{1}, \ldots, A_{n}]$ , we mean the formula obtained from $C(D(1-$$4))$ by substituting eachfor every occurrence ofin $C(D(1^{-}4))$ . If$4))[A_{1}, \ldots, A_{n}]$ , then$C(D(1^{-}4))$
satisfy
under the as sumptions . The following lemma states that under the common knowledge of SOLV, the axiom $C(D(1^{-}4))$ issatisfied by the formulae of Proposition 5.1.2).
$\mathrm{g}$$A_{i}(\cdot)$$A_{1},$$\Gamma\vdash_{\omega}C(D(1-$$D_{i}(\cdot)$$A_{n}$$\Gamma$$\ldots,$

Lemma 5.2.

Let

$Sol_{i}(^{arrow}a_{i})$be$C(SOLV)\vdash_{\omega}C(D(1-4))[sol_{1}, \ldots,sol_{n}]$$\exists y{}_{-i}Carrow(Nash_{\mathrm{g}}(a_{i}arrowarrow);y-i)$.

for $i=1,$$\ldots,$$n$. ThenThe concept intended by $C(D(1^{-}4))$ is the weakest one among those satisfying$C(D(1-4))$ , since, otherwise, it would contain some properties additional to that given

by $C(D(1^{-}4))$ . To require this idea, we impose the following axiom schema:$C(D(1-4))[A_{1}, \ldots, A_{n}]\supset\forall x_{i}(arrow A_{i}(^{arrow}xi)\supset D_{i}(x_{i}arrow))$

,

where
are any formulae. We denote this by $WFD$ . Since we proved in Lemma
5.2 that the premise of this axiom is provable with Soll,under the assumptionof $C(SOLV)$ , we have the $C(SOLV),$. This together with
Proposition 5.1.2) implies the following theorem.
$A_{1},$$A_{n}$$\ldots,$$\ldots,sol_{n}$$WFD\vdash_{\omega}Sol_{i}(^{arrow}a_{i})\supset D_{i}(arrow a_{i})$Theorem 5.

$\mathrm{A}$. $C(D(1-4)),$ $c(SoLV),$$\exists y_{-}iC(Nash\mathrm{g}(^{arrowarrow}ai|y_{-}i))$for $i=1,$$\ldots,$$\iota VFD\vdash_{\omega}D_{i}(^{arrow}ai)\supset\subset$$n$.

5We explained the necessity of each step from depth $m$ to $m+1$ in a heuristic manner. In the finitary, we can prove that the step of depth $m$ cannot be derived from the previous one, using
fragment of
the depth lemma in-Nagashima [9]. This lemma is not yet extended into the infinitary.
$GL_{\omega}$$\mathrm{I}\{\mathrm{a}\mathrm{n}\mathrm{e}\mathrm{k}_{0}$$GL_{\omega}$

47

is determined to be a Nash strategy
This theorem states that the final
to notice that the existential
importantIt
property.
iswith the common knowledge,
quantifier is outside the common knowledge operator. If it was, the existence of the other players’
bywhich is implied by
Nash strategies are simply required to be known. The formularequires player to know specific Nash strategies for the other players. This difference
is important for the subject of Section 6.
$\mathrm{d}\mathrm{e}\mathrm{c}\mathrm{i}\mathrm{s}\mathrm{i}\mathrm{o}\mathrm{n}arrow a_{i}$$C(\exists y_{-i}Nash\mathrm{g}(^{arrow}ai;arrow y_{-}i))$$\exists y_{-}iC(Nash(\mathrm{g}a_{i};arrow arrow y-i))$$(\exists c)$$\exists y_{-i}C(\mathit{1}\mathrm{v}ash(\mathrm{g}ai;arrowarrow y_{-}i))$$i$

Theory II: Undecidability Theorems on the
6. Applications to
Playability of a Game$\mathrm{G}\mathrm{a}\mathrm{n}’1\mathrm{e}$, is needed for each player to be able to
The existence of a final decision,
make a final decision. By Theorem 5. , this existence is equivalent to the existence of. As wasa Nash strategy with the common knowledge property, i.e.,already stated, the existence quantifiers are outside the scope of the common knowledge. In classical game theory, the existence of a Nash equilibrium is proved
operator
by using Brouwer’s fixed point theorem (cf., von Neumann-Morgenstern [21] and Nash[17] . When the real number axioms are common knowledge, this existence proof implies, where the existential quantifiers are in the scope of the common
knowledge operator. There is a gap between the above two existential statements.
In this section, we adopt the real closed field axioms as a particular choice of realis provable from the common
number axioms, and show that although
is formally undecidable, i.e.,knowledge of the real closed field, is provable fromneither this existence statement nor its negation,field
axioms.
the common knowledge of the real closed$\exists x_{i}D_{i(^{arrow})}arrow xi$$\mathrm{A}$$\exists^{arrow}XC(NaSh_{\mathrm{g}}(^{arrow}x))$$C(\cdot)$$)$$C(\exists^{arrow}xNaSh\mathrm{g}(\overline{X}))$$C(\exists^{arrow}xNaSh_{\mathrm{g}}(^{arrow}x))$$\mathrm{a}\backslash ’\dot{\lrcorner}\mathrm{o}\mathrm{m}\mathrm{s},$$\exists^{arrow}xC(Nash_{\mathrm{g}}(^{arrow}x))$$\neg\exists xarrow C(Nash_{\mathrm{g}}(^{arrow}x))$6.1. Real Closed Field Axioms and the Existence of a Nash Equilibrium

The real closed field theory is defined by adding the following axioms to the ordered:
field axioms$\Phi_{\mathrm{o}\mathrm{f}}$;andfor any odd natural number $m$ ,$\forall x\exists y(X\geq 0\supset(y^{2}=x))$$\forall ym-1\cdots\forall y0\exists x(x+m-1x-1+m+y1^{X}+y0=0y_{m}\ldots)$

(6.1)

.

. The theory
and the set of the formulae of (6.1) by
We denote the union ofis the finitary fragment ofis called the real closed field theory, where. Here we refer to Tarski’s completeness theorem on the real
without including$\Phi_{\mathrm{r}\mathrm{c}\mathrm{f}}$$\Phi_{\mathrm{o}\mathrm{f}}$$P_{\mathrm{o}\mathrm{f}}$$(P_{\mathrm{O}}\mathrm{r}, \Phi_{\Gamma}\mathrm{c}\mathrm{f})$$D_{n}$$D_{1},$$\ldots,$$P_{\omega}$

48

closed field theory (cf., Rabin [18]): for any closed formula$\Phi \mathrm{r}\mathrm{c}\mathrm{f}\vdash 0\neg A$

$A$

.

in

$P_{\mathrm{o}\mathrm{f}}$, either$\Phi_{\mathrm{r}\mathrm{c}\mathrm{f}}\vdash_{0}$

$A$

or

The standard existence proof of a Nash equilibrium for any finite game with mixed
strategies relies upon Brouwer’s fixed point theorem (Nash [17]). This implies that in
the standard (real number) model of, the existence of a Nash equilibrium,, is valid. Since
is complete, we have,
which together with Proposition 3.5.1) implies the following.
Proposition 6.1. Let be any -person finite game. Then$\mathrm{g}$$(P_{\circ \mathrm{f}}, \Phi_{\mathrm{r}\mathrm{C}}\mathrm{f})$$\exists xNarrow ash_{\mathrm{g}}(xarrow)$$(\mathcal{P}_{\circ \mathrm{r}}, \Phi_{\Gamma \mathrm{c}\mathrm{f}})$$n$$\mathrm{g}$$\vdash_{\omega}C(\exists^{arrow}xNaSh_{\mathrm{g}}(^{arrow}x))$$\Phi_{\mathrm{r}\mathrm{c}\mathrm{f}}\vdash_{0}\exists x\mathit{1}Varrow has\mathrm{g}(\overline{x})$$C(\Phi_{\mathrm{r}\mathrm{c}\mathrm{f}})$.

Thus, in logic, the existence of a Nash equilibrium is common knowledge if
the real closed field axioms are common knowledge. Nevertheless, this is different from, which is required for a player in order to play the gameby Theorem 5. .
The following is the key result for such an evaluation, which is called the term
existence theorem: for a setof nonepistemic closed formulae and a nonepistemic
formula with no free variables in,$GL_{\omega}$$C(\Phi_{\mathrm{r}\mathrm{c}\mathrm{f}})\vdash_{\omega}\exists xCarrow(Nash_{\mathrm{g}}(^{arrow}x))$$\mathrm{A}$$\mathrm{g}$$\Gamma$$A$$\exists x_{1}\ldots\exists x\ell C(A(x_{1}, \ldots, x\ell))$$C(\Gamma)\vdash_{\omega}\exists x_{1}\ldots\exists X\ell C(A(X1, \ldots, X\ell))$

if and only if(6.2)
for some closed terms.
This term existence theorem will be proved in Part II, using the cut-elimination theoremfor. This theorem tells us that we should distinguish between the mere knowledgeof the existence, i.e., only the existence proof is common knowledge, and the specificobjects having the property are common knowledge.
As the direct application of (6.2) to our problem, we have
$C(\Gamma)\vdash_{\omega}C(A(t1, \ldots, tn))$$t_{1},$$t_{\mathit{1}}$$\ldots,$$GL_{\omega}$$A$$C(\Phi_{\mathrm{r}\mathrm{C}\mathrm{f}})\vdash_{\omega}\exists xarrow C(NaSh\mathrm{g}(Xarrow))$

if and only if$C(\Phi_{\mathrm{r}\mathrm{C}\mathrm{f}})\vdash_{\omega}C(Nash\mathrm{g}(^{arrow}t))$(6.3)

for some closed term$\mathrm{v}\mathrm{e}\mathrm{C}\mathrm{t}_{0}\mathrm{r}tarrow$.

Thus, for the specific existence, we need probability, eachcomponent of which is represented as a closed term. In the present language together
with the ordered field axioms, for any closed term there is a rational number
such that. Informally speaking, (6.3) implies that there should exist a Nashequilibrium in rational numbers. However, this does not always hold for games withmore than two players.
$\mathrm{v}\mathrm{e}\mathrm{c}\mathrm{t}_{0}\mathrm{r}\mathrm{S}arrow t_{i}=(t_{i1},$$t_{i\ell)}$$\ldots,$$\Phi_{\mathrm{o}\mathrm{f}}$$t$$\Phi_{\mathrm{o}\mathrm{f}}\vdash t=[r]$6.2. Undecidability Theorems on the Playability of a Game

Consider the following three-person game:

$r$

49

$\alpha_{1}$$\alpha_{2}$(1,0,0)(2,0,8)(0,0,1)(1,1,0)$\beta_{2}$$\beta_{1}$$\beta_{2}$$\beta_{1}$(2,0,9)(0,1,1)$\alpha_{1}$$\alpha_{2}$(0,1,1)(1,0,0)$\gamma_{2}$$\gamma_{1}$Table 4
Table 3In this game, each player has two pure strategies, and the tables mean that when the, the right upper vector (0,1,1) of Table 4
players choose pure strategies, say,gives payoffs to the players. This game has no Nash equilibrium in pure strategies, but
has a unique Nash equilibrium $((p, 1-p),$ $(q, 1-q),$ $(r, 1-r))$ in mixed strategies, where$\alpha_{1},\beta_{2},$$\gamma_{2}$$p=(30-2\sqrt{51})/29,$ $q=(2\sqrt{51}-6)/21$ and $r=(9-\sqrt{51})/12$ .

The probability weights in equilibrium are irrational numbers. Therefore those probabilities are not represented as closed terms in our language. Therefore it follows from.
(6.3) that it is not the case thatis
In fact, the negation of this existential assertion, as was stated in (4.1). Hence Proposition
equivalent to.
6.1 implies that it is not the case thattheorem.
In sum, we have the following$C(\Phi_{\mathrm{r}\mathrm{C}\mathrm{f}})\vdash_{\omega}\exists xarrow C(Nash_{\mathrm{g}}(^{arrow}x))$$C(\Phi_{\mathrm{r}\mathrm{c}\mathrm{f}})\vdash_{\omega}\neg\exists^{arrow}XC(NaSh_{\mathrm{g}}(^{arrow}x))$$C(\Phi_{\mathrm{r}\mathrm{c}\mathrm{f}})\vdash_{\omega}C(\neg\exists^{arrow}Xl\mathrm{V}ash\mathrm{g}(\overline{x}))$$C(\Phi_{\mathrm{r}\mathrm{c}\mathrm{f}})\vdash_{\omega^{\neg}}\exists xCarrow(NaSh\mathrm{g}(Xarrow))$

Theorem 6. (Formal Undecidability I). Let
Tables 3 and 4. Then$\mathrm{A}$neithernor$\mathrm{g}$be the three-person game given by$C(\Phi_{\mathrm{r}\mathrm{C}\mathrm{f}})\vdash_{\omega}\exists xarrow C(Nash_{\mathrm{g}}(^{arrow}x))$$C(\Phi_{\mathrm{r}\mathrm{C}\mathrm{f}})\vdash_{\omega^{\neg}}\exists xCarrow(NaSh\mathrm{g}(Xarrow))$.

As was stated in (6.3), the condition for a player to find a Nash strategy is that
there is a Nash equilibrium in closed terms. He can verify whether each closed term
vector satisfies the Nash condition. Therefore if there is a Nash equilibrium in closed
terms, he would eventually find a Nash equilibrium. However, when there is no Nashequilibrium in closed terms such as in the game of Tables 3 and 4, he continues theverification of whether each candidate satisfies the Nash condition. Each player does
not have the knowledge of the space of closed terms, more generally, he does not haveknowledge about the language as a whole he is using. Therefore he should continue tosearch a Nash equilibrium, and cannot know whether there is a Nash equilibrium ornot.
For the above three-person game, our undecidability result would become a decidability result if we introduce a function symbol and some axiom to allow the radical
expression $f$ . The the above undecidability result depends upon the choice of a

50

language. The point of the theorem is, however, that the players cannot notice the necessity of an extension of the language, since neither the positive nor negative statement
is known to them.
The property that a Nash equilibrium involves irrational numbers is general forgames with more than two players, except some degenerate cases. In fact, it is provedin Bubelis [5] that any algebraic real number in $[0,1]$ occurs in a Nash equilibrium forsome three-person game with finite numbers of pure strategies.6 Thus the problemof obtaining the decidability result in the general case is not so simple as in the casementioned in the above paragraph for the particular game. This will be discussed in
Kaneko [10].
In Section 5, our concern was the determination of final decision predicate.
Under axioms $C(D(1-4)),$ $c(soLV)$ and レワア D, final decision
coincides with
. Noting that whenis assumed, $C(SOLV)$ is not necessary, the playability of a game is directly stated as$D_{i}(a_{i})arrow$$D_{i}(^{arrow}a_{i})$$\exists\overline{x}-iC(Nash\mathrm{g}(\overline{a}i;xarrow-i))$$C(\Phi_{\mathrm{r}\mathrm{c}\mathrm{f}})$$\mathrm{g}$whether or not $C(D(1^{-}4)),$ $WFD,$

In fact, we obtain a formal undecidability on$C(\Phi \mathrm{r}\mathrm{C}\mathrm{f})\vdash_{\omega}\exists x_{i}arrow D_{i(x_{i})}arrow$$\exists x_{i}arrow D_{:(xi}arrow$

Theorem 6. (Formal Undecidability II). Let
by Tables 3 and 4. Then$\mathrm{B}$neither $C(D(1^{-}4)),$ $?VFD,$

nor $C(D(1-4))$ , VVFD,$\mathrm{g}$

.

(6.4)

).

be tlle three-person game given$c(\Phi \mathrm{r}\mathrm{c}\mathrm{f})\vdash_{\mathrm{t}v}\exists x_{i}Darrow i(^{arrow}xi)$$C(\Phi_{\mathrm{r}\mathrm{c}\mathrm{f}})\vdash_{\omega^{\neg}}\exists x_{i}arrow D_{i}(x_{i}arrow)$.

The following lemma is a crucial step for Theorem 6. .
$\mathrm{B}$Lemma 6.2. Let
Then$(\mathcal{P}_{\omega}, C(D(1-4)),$$P_{\omega}\#$be the set of formulae in
without including
is a conservative extension of$\mathrm{T}/VFD,$$P_{\omega}$$C(\Phi \mathrm{r}\mathrm{c}\mathrm{f}))$$D_{1},$$D_{n}$$\ldots,$$(\mathrm{p}_{\omega}\#,C(\Phi \mathrm{r}\mathrm{c}\mathrm{f}))$.

.

7. Conclusions
This paper provided the logic framework for the investigations of game theoretical problems, and showed two applications. The first application is an epistemic axiomatizationof Nash equilibrium, and the second is the undecidabihty on the playability of a game.

6Lemke-Howson [13] gave a finite algorithm to find a Nash equilibrium for a two-person game with
mixed strategies, wltich implies the existence of a Nash equilibrium in rational numbers. Therefore
undecidability fails since the existential formula is provable for any two-person game. However, if weformulate the real closed field theory based on only
, then we obtain an undecidability result
even in the two-person case.
$+\mathrm{a}\mathrm{n}\mathrm{d}.$51

The first is still a game theoretical problem, though it was discussed in the game logic
framework. The second is also a game theoretical problem, but it can be regarded as alogic problem as well in that it is a metatheorem. It is important that the latter was
raised by the former. Therefore, these form a result belonging to both game theory andmathematical logic.
To obtain the undecidability results, we used the term existence theorem, which
is a metatheorem on provability. It is difficult to prove such metatheorems in thepresent Hilbert style formulation. In Part II of this paper, we reformulate the gamelogic framework in the Gentzen style sequent calculus, and prove the cut-elimination
theorem for it. By the cut-elimination theorem, we prove the term existence theorem
and the converse of the Proposition 2.2 (faithful representation). The Gentzen styleformulation and the cut-elimination theorem will provide other deeper results. These
are the subjects of Part II.
From the viewpoints of logic as well as of game theory, the epistemic axiomatization
theoretical discussionsof Nash equilibrium in Section 5 needs more discussions.
are found in Kaneko-Nagashima [8]. Proof theoretical evaluations of the epistemic
will be discussed in a different paper.
As was mentioned, the undecidability results of Section 6 depend upon the choiceof constants or function symbols. If more constants are introduced to describe all real
algebraic numbers, then we obtain the decidability results. There still remain important
problems in this direction from the viewpoint of both logic and game theory. These will
be discussed in Kaneko [10].
$\mathrm{C}_{7}\mathrm{a}\mathrm{m}\mathrm{e}$$\mathrm{a}_{d}\mathrm{x}\mathrm{i}\mathrm{o}\mathrm{m}\mathrm{a}\mathrm{t}\mathrm{i}_{\mathrm{Z}\mathrm{a}}\mathrm{t}\mathrm{i}_{\mathrm{o}\mathrm{n}}$References[1] Aumann, R. J., (1993), Backward Induction and Common Knowledge of Rationality, Mimeo.
[2] Bacharach, M., (1987), A Theory of Rational Decision in Games, Erkenntnis 27,

17-55.
[3] Bacharach, M., (1994), The Epistemic Structure of a Theory of a Game, Theory
and Decision 37, 7-48.
[4] Balkenborg, D. and E. Winter, (1995),. A Necessary and Sufficient Condition for
Playing Backward Induction, Mimeo.
[5] Bubelis, V., (1979), On Equilibria in Finite Games, International Journal of Game
Theory 8, 65-79.

[6] Halpern, J. H. and Y. Moses, (1992), A Guide to Completeness and Complexity
for Modal Logics of Knowledge and Beliefs, Artificial Intelligence 54, 319-379.

52[7] Hintikka, J., (1962), Iinowledge and Belief, Cornell University Press.
[8] Kaneko, M. and T. Nagashima, Final Decisions, Nash Equilibrium and Solvability
in Games with the Common Knowledge of Logical Abilities, Mathematical Social
Sciences 22, 229-255[9] Kaneko, M., and T. Nagashima, (1994), Axiomatic Indefinability of Common
Knowledge in Finitary Logics, To appear in Epistemic Logic and the Theory ofGames and Decision, eds. M. Bacharach, L. A. Gerard-Varet, P. Mongin and H.

Shin.
[10] Kaneko, M., (1995), The Knowledge of the Existence of a Nash Equilibrium and
the Playability of a Game, Forthcoming.
[11] Karp, C., (1964), Languages with Expressions of Infinite Length, North-Holland.

[12] Keisler, H. J., (1971), Model Theory for Infinitary Logic, North-Holland.
[13] Lemke, C. E., and J. T. Howson, (1964), Equilibrium Points of Bimatrix Games,
SIAM Journal of Applied Mathematics 12, 412-423.

[14] Lismont, L. and P. Mongin, (1994), On the Logic of Common Belief and Common
Knowledge, Theory and Decision 37, 75-106.
[15] Mendelson, E., (1973), Number Systems and the Foundations of Analysis, Academic
Press.

[16] Mendelson, E., (1987), Introduction to Mathematical Logic, Wadsworth.
[17] Nash, J. F., (1951), Noncooperative Games, Annals of Mathematics 54, 286-295.

[18] Rabin, M., (1977), Decidable Theories, Handbook of Mathematical Logic, ed. J.
Barwise, 595-630.
[19] Segerberg, K., (1994), A Model Existence Theorem in Infinitary Propositional
Modal Logic, Journal of Philosophical Logic 23, 337-367.

[20] von Neumann, J., (1928), Zur Theorie der Gesellschaftsspiele, Mathematische Annalen 100, 295-320.
[21] von Neumann, J., and 0. Morgenstern, (1944), Theory of Games and Economic
Behavior, Princeton University Press.