Formal Dialogue Semantics for Definitional Reasoning and Implications as Rules

Abstract

In dialogue semantics, the logical constants receive a certain game-theoretical interpretation. Dialogues are games between two players, the proponent and the opponent, who can alternatingly either attack assertions made by the other player or defend their own assertions. The logical validity of an assertion made by the proponent in the first move consists in the existence of a winning strategy for the proponent for this assertion.

Based on a modified standard dialogue semantics for intuitionistic logic, we develop a formal dialogue semantics for definitional reasoning. Definitional reasoning is an extension of logic programming, in which an underlying logic can by extended by definitions of a certain form. The presented dialogue semantics is a semantics for logical reasoning with respect to such definitions. We also develop a formal dialogue semantics for implications considered as rules. Different to standard dialogue semantics for intuitionistic logic, this new semantics needs an additional argumentation form corresponding to cut. An equivalence result is proved for the resulting formal dialogue semantics and the intuitionistic sequent calculus for implications as rules.

In Dialogsemantiken erhalten die logischen Konstanten eine gewisse spieltheoretische Interpretation. Dialoge sind Spiele zwischen zwei Spielern, dem Proponenten und dem Opponenten, die abwechselnd Behauptungen des jeweils anderen Spielers entweder angreifen oder ihre eigenen Behauptungen verteidigen können. Die logische Gültigkeit einer vom Proponenten im ersten Spielzug behaupteten Aussage besteht dann in der Existenz einer Gewinnstrategie des Proponenten für diese Aussage.

Ausgehend von einer modifizierten Standarddialogsemantik für die intuitionistische Logik wird zum einen eine formale Dialogsemantik für definitorisches Räsonieren entwickelt. Das definitorische Räsonieren stellt eine Erweiterung der Logikprogrammierung dar, bei der eine zugrundeliegende Logik um Definitionen bestimmter Form erweitert werden kann. Die vorgestellte Dialogsemantik ist eine Semantik für das logische Schließen bezüglich derartiger Definitionen. Zum anderen wird eine formale Dialogsemantik für als Regeln aufgefaßte Implikationen entwickelt. Anders als bei Standarddialogsemantiken für die intuitionistische Logik bedarf diese neue Semantik unter anderem auch einer der Schnittregel entsprechenden Argumentationsform. Für die resultierende formale Dialogsemantik wird ein Äquivalenzresultat für den für Implikationen als Regeln vorgeschlagenen intuitionistischen Sequenzenkalkül bewiesen.