1. Introduction to Tarski Game SemanticWhy a Game Semantic of Mathematical Proofs? Game Semantic have been used successfully to model several fields, from Biology to Economy to Sociology to Logic. For a detailed introduction we refer to the section "Game Theory" in Stanford on-line Encyclopedia of Philosophy or Wikipedia. Here we only want to give an overview of the topic, and we want to explain how games can be used to interpret (to "implement", in a sense) mathematical proofs as mechanical decision method or "algorithm" of a very particular kind. Our goal is to interpret any proof of the existence of an individual having a given property as an algorithm finding an individual having such property. This problem was first raised by Hilbert (see section 2.3.1 of Hayashi's web site on Hilbert notes). Proofs as Learning algorithms. This goal, taken literally, is known since Godel's Incompletness result to be impossible to achieve. However, we will show how to weaken the notion of algorithm, switching from algorithms computing values to algorithms learning values. Using this idea we are able to interpret all proofs as learning algorithms, whose structure mirrors the structure of the proof. These algorithms can be defined as strategies for particular games, games with "backtracking".In these games we are allowed to retract finitely many times each move we did, thereforewe can learn the correct move by trial-and-error. Tarski Game Semantic.Our starting point is Tarski Game Semantic of mathematical statements (without neither "backtracking", nor "learning"). Tarski Game Semantic is not enough toachieve our goal, though. In the next section we will extend Tarski Games allowing "backtracking"or retracting of moves. In Tarski Game Interpretation, each statement is associate to a debate (on strictly rational grounds) between two players. The first one, Eloise, tries and argue that the statement is true, while the second one,Abelard, tries and argue that the statement is false. The debate takes the form of a play, whose moves correspond to all possible logical arguments each player can choose at any step of the debate. Eloise has a winning strategy for the Tarski Game associated to a mathematical statement (that is, she is able to convince eventually Abelard that the statement is true) if and only if the statement is, indeed, true. Abelard has a winning strategy for the Tarski Game associated to the same statement (that is, she is able to convince eventually Eloise that the statement is false) if and only if the statement is, indeed, false. For more information, visit the subsite:
including examples of Tarski plays related to various statements. A program helping to play Tarski Games. Examples are produced by a program we called Tarski, allowing two human players taking the role of Eloise and Abelard, and playing one against the other over a given mathematical statement (look at the Menu for more information). You need a Mathematica intepreter to run the program, otherwise you can only look to the examples of the site. Tarski Games are not an interpretation of proofs. These examples also show that Tarski game interpretation is falling short from our goal. Indeed, truth and falsehood of statements are often interpreted through winning strategy which cannot be computed by algorithms. Whatwe need is an interpretation of mathematical proofs, not just of truth and falsehood, and this will be achieved in the next section by introducing the notion of "backtracking" or retracting of moves.  Courtesy from Goettingen State and University Library (Germany).Picture copied from S. Hayashi, section 2.3.1. |