TR-2010002: Reasoning About Games
Melvin Fitting · CUNY Academic Works (City University of New York) · 2010
A mixture of propositional dynamic logic and epistemic logic is used to give a formalization of Artemov's knowledge based reasoning approach to game theory, (KBR), [4,5,6,7].We call the (family of) logics used here PDL + E. It is in the general family of Dynamic Epistemic Logics [21], was applied to games already in [20], and investigated further in [18,19].Epistemic states of players, usually treated informally in game-theoretic arguments, are here represented explicitly and reasoned about formally.The heart of the presentation is a detailed analysis of the Centipede game using both the proof theoretic and the semantic machinery of PDL + E. The present work can be seen partly as an argument for the thesis that PDL + E should be the basis of the logical investigation of game theory.read as: agent A knows X.A dual operator K A is sometimes introduced, with K A X abbreviating ¬K A ¬X. K A X can be read as asserting that X is compatible with the knowledge of agent A.Axiomatically each K A is a normal modal operator, so there is a knowledge necessitation rule, from X conclude K A X.There are also modus ponens, and the following axiom schemes (note that these are schemes, not individual axioms).E-1 All tautologies (or enough schemes to generate them)In addition there may be some or all of the following as axiom schemes.E-3 K A X ⊃ X, Factivity.Its presence or absence is what distinguishes knowledge from belief, in this approach.