Formal reasoning about fuzzy evaluation games

Abstract

Logische Auswertungsspiele stellen eine alternative Beschreibung von Wahrheit zu Tarskisemantik dar und führen zu einigen interessanten Erweiterungen klassischer Logik, wie beispielsweise Independence-Friendly Logic von Hintikka. Auswertungsspiele nach Hintikka sind zu einem Standardwerkzeug zur Analyse neuer Logiken geworden. Mathematische Fuzzy Logik ist ein System, um vage Aussagen zu modellieren. Ihr Ursprung liegt in den Werken von Lukasiewicz und Gödel. 1965 wurde der Begriff Fuzzy Logic von Zadeh geprägt. Diese zwei Ansätze wurden durch Hajek zusammengeführt und sind seither ein lebendiges Forschungsgebiet. Es werden Beschreibungen von Auswertungsspielen, sowohl für klassische als auch für prominente Fuzzy Logiken, mit Definition aus formaler Spieltheorie verglichen. Es zeigen sich Diskrepanzen zwischen den Auswertungsspielen und den formalen Definitionen von Spielen in extensiver Form vollständiger Information. Durch die Darstellung der Regel für Negation als regulären Zug einEr SpielerIn werden die Definitionen unifiziert und die Äquivalenz zur Standardsemantik bewiesen. Die Analyse spieltheoretischer Konzepte mit Hilfe formaler Logik, insbesondere Modallogik, stellt ein verhältnismäßig neues Gebiet dar. Sie hat sehr ausdrucksstarke Formalismen, wie beispielsweise Game Logic hervorgebracht, mit welcher die Effektivität von SpielerInnen untersucht werden kann. Die hier vorgenommene Untersuchung der Unschärfen führt zu einer Weiterführung der Formalisierung der Spiele: Eine Axiomatisierung der Spielbäume mit Modallogik wird erstellt und ausführliche Äquivalenzbeweise werden erarbeitet. Eine gründliche Analyse von Prädikatenmodallogik und modaler Korrespondenztheorie wird hierfür vorgenommen. Die vorliegende Axiomatisierung stellt eine mögliche Grundlage dar, um die Klasse der logischen Auswertungsspiele in ausdrucksstärkeren Formalismen zu untersuchen.

Logical evaluation games are an alternative characterization of truth to standard Tarskian semantics. Analyzing truth with the apparatus of formal game theory has led to some interesting generalizations of classical logic, like Independence-friendly logic by Hintikka, based on making evaluation a game of imperfect information. Hintikka-style evaluation games have become standard means of analyzing new logics. Mathematical fuzzy logic provides a formalism for reasoning about vague statements. Its roots can be traced back to works by Lukasiewicz and Gödel. In the second half of the twentieth century Zadeh coined the term fuzzy logic for a formalism used in automation. The approaches were unified in Hajek's framework and have been an active research topic since. A close alignment of evaluation games, for classical and prominent fuzzy logics, with formal game theory reveals a gap between the presentation of logical evaluation games and formal definitions of extensive games of perfect information. This work joins the two notions by providing an explicit game rule of negation as an in-game move and aligning the definitions. The two resulting games, one for classical logic and one for Zadeh's fuzzy logic, along with correspondence proofs to standard semantics are a central result of this thesis. The direction of analyzing game theoretic concepts with formal logic, especially modal logic is a comparatively new field and has yielded highly expressive formalisms, like Game Logic, for reasoning about players' powers for certain game situations. Examining the minor imprecisions in evaluation game definitions in literature led us to the idea of formalizing the games a distinctive step further: we construct modal axiomatizations of the game trees, by viewing them as Kripke structures and carry out extensive formal proofs showing that those axioms describe the games. A thorough analysis of first-order modal logic and modal correspondence theory is carried out in order to capture as many aspects as possible syntactically. The provided axiomatization may serve as a base for concretely analyzing the class of logical evaluation games in richer formal systems.