Dialogue Logic

DiaLogic: A System for Dialogical Logic

Dialogical Logic [5,6] (also: dialogue logic) was originally proposed by Prof. Paul Lorenzen, who taught philosophy in Erlangen. Essential contributions are due to Kuno Lorenz, who later on became a professor of Philosophy in Saarbruecken. Native speakers of English are referred to Walter Felscher’s articles on dialogical logic [2,3]. The latest and most comprehensive textbook (in German) has been written by Rüdiger Inhetveen [7].

The central idea of dialogical logic is to provide a pragmatic foundation of logic on a game-theoretic basis — hence introducing semantics by a nutual agreement on moves —, but it is as well suited for teaching logic. So, dialogical logic is commited to proof-theory; model theory does not play a foundational, but an illustrative role. Any successful proof in dialogical logic consists in the construction of a model, otherwise of a counter-example.

So, in dialogical logic, the validity of some formula F is examined in two person, perfect information games . There are two players moving alternatively, both having complete information of the current situation of the game. The player who claims being able to justify F is called the proponent, his adversary the opponent.

The initial state, the dialogue setting, is determined by a (possibly empty) set of hypotheses (introduced into the game by the opponent) and a thesis F, the formula to be shown valid, brought in by the proponent. The consecutive moves of the dialogue game are attacks upon formulae asserted earlier or defences against previous attacks. Some moves include the introduction of formulae that might be subject to subsequent attacks.

The legal moves that a player can perform are defined by so-called particle rules and frame rules. For each logical connective PHI a particle rule is given which specifies how attacks upon moves asserting formulae that have PHI as main connective and defences against such attacks have to be performed. The frame rules organize the exchange of arguments, i.e., they impose restrictions on when attacks and defences may take place in the dialogue. Depending on the choice of frame rules, dialogical logic covers constructive („intuitionistic“) and classical logics as well.

A dialogue game is won by a player, if the other player cannot perform any action that conforms with the dialogue rules. The proponent is said to have a winning strategy for a formula F, if he is able to win any game where formula F is the thesis (and a given set of hypotheses) by appropriate choices of his statements. A formula F is valid, if the proponent has a winning strategy for F. Winning strategies might not be unique. Felscher [3,4] presents a proof that the notion of winning strategies in dialogue games (wrt. a well-defined set of dialogue rules) coincides with the notion of provability in Gentzen’s calculus LJ for intuitionistic logic.

Recently, the idea of „logic games“ as well as further approaches to dialogical logic have received a lot of attention, e.g. in publications by Barth, van Benthem, Hintikka, Hamblin, Krabbe, Mackenzie, Walton, and others.

Theorem Provers Implementing Dialogical Logic

We know of at least two implementations in the 1970s . One has been made in Erlangen by Gerrit Haas [4] at the Computer Science Institute (IMMD) on a PDP 7. Another implementation had been done (in Fortran on a Control Data 6600 and later ported to a CD 3300 in Erlangen) in Austin, Texas, where Lorenzen spent some time as a visiting professor (around 1970). Both systems implemented only the propositional part of dialogical logic.

Today, we know of no other implementation of Dialogical Logic except DiaLogic as presented here.

Later on, COLOSSEUM, a theorem prover for constructive predicate logic — without an interactive mode to play dialogue games — has been implemented in Prolog by Claus Zinn. For details, please contact zinnwerk.com.

DiaLogic — A System for Dialogical Logic

As far as we know, DiaLog is the first system which implements Dialogical Logic for propositional, full predicate, and modal logic. We had the following goals in mind:

1. To better understand the dialogue calculus.
2. To have a system for teaching purposes.
3. To promote Dialogical Logic which is rather unknown in the Automatic Deduction community.

Ad 1: In the history of Dialogical Logic there has always been a debate about the ‚correct‘ specification of particle and frame rules. It is the case, that different versions of frame and particle rules lead to different logics. In the literature on Dialogical Logic, numerous versions of them (mostly kept rather informal) can be found, cf. [5,6]. In order to experiment with the dialogue rules, DiaLogic offers the possibility to redefine both particle and frame rules by means of a rule language. There are predefined rules for effective, classical and modal logic.

Ad 2: Due to its friendly user interface, DiaLogic can easily been used for teaching purposes. Dialogical Logic has been a part of the curriculum for students of philosophy in Erlangen up to now.

Ad 3: As documented in [0], the first full implementation of Dialogical Logic has been made available to the Automated Deduction community. Dialogical Logic is an interesting proof calculus which is worth further investigation.

A description of the system for Dialogical Logic is provided in [0,1]. The latter description is in German and describes mostly implementation details. However, there is a chapter describing the use of DiaLogic. We have no further user or reference manuals available

Here you see a snapshot of system run with its graphical user interface. The interface is divided into four parts:

Here is a snapshot of the stategy grapher (for the PEIRCE formula proven in the illustration above):

System features are:

The system has been implemented in Scheme and Tk (the Scheme system STk offers both)
by Jürgen Ehrensberger within his master’s project under the supervision of Dr. Claus Zinn
and Prof. Dr. Guenther Goerz at the Dept. of Computer Science / 8, (Artificial Intelligence)
of the University of Erlangen-Nuremberg.

System requirements

To run the DiaLogic system, you need a Scheme interpreter. We have tested DiaLogic with several Scheme implementations obeying the R5RS standard, in particular with SCM (Version 2a6) and STk (Version 4.0.1). The Scheme Library SLIB is required. We recommend strongly to use the Berkeley modification of STk 4.0.1, called UCB Scheme, version 4.0.1-ucb1.16, which is available for Linux, Windows, and Mac OS X. It contains everything you need (including the portable Scheme library SLIB) and is very easy to install.

• To run DiaLogic with a GUI you need either a Unix/Linux (X11) or Windows platform and STk.
• To run DiaLogic without the GUI (i.e., in command line mode), a DOS or any other platform providing a text-based shell, and SCM suffice.

How to obtain the system

Download DiaLogic

References

[0] Ehrensberger Jürgen, and Zinn, Claus. DiaLog — A system for dialogue logic, CADE-14, Conference on Automated Deduction, Townsville, North Queensland, Australia. Lecture Notes in Artificial Intelligence, Vol. 1249, Springer 1997 446–460.

[1] Ehrensberger, Jürgen. Ein System für Dialogische Logik. Diplomarbeit am Institut für Mathematische Maschinen und Datenverarbeitung, Lehrstuhl Künstliche Intelligenz (Informatik 8). Universität Erlangen-Nürnberg, 1996. [PDF]

[2] Felscher, Walter. Dialogues, Strategies and Intuitionistic Provability . Annals of Pure and Applied Logic 28 (1985), 217–254

[3] Felscher, Walter. Dialogues as a Foundation for Intuitionistic Logic Handbook of Philosophical Logic. Vol. III. Ed. by Dov M. Gabbay, and Franz Guenthner. Dordrecht: D. Reidel, 1986. 341–372.

[4] Haas, Gerrit. Programme zur dialogischen Logik . Arbeitsberichte des IMMD. Bd. 3, Nr. 4. Universität Erlangen-Nürnberg, Oktober 1970.

[5] Lorenzen, Paul. Ein dialogisches Konstruktivitätskriterium . Infinitistic Methods. Proceedings of the Symposium on Foundations of Mathematics (Warszawa 1959). Oxford: Pergamon, 1961. 193–200. (Reprinted in P. Lorenzen/K. Lorenz: Dialogische Logik . 9–16).

[6] Lorenzen Paul, and Lorenz, Kuno. Dialogische Logik . Darmstadt: Wissenschaftliche Buchgesellschaft, 1978.

[7] Inhetveen, Rüdiger. Logik — Eine dialog-orientierte Einführung . Leipzig: Teubner, 2002.