Some notes on C. Fermüller's “Parallel dialogue games and hypersequents for intermediate logics” I: Differences between Fermüller's and Felscher's notation for dialogues

In trying to show that my modest change to one rule of Felscher's ruleset E generates the logic LQ of weak excluded middle, I have found it necessary to reach out for tools that could help deal with this kind of problem. Of course, one could try to go back to Felscher's paper “Dialogues, strategies, and intuitionistic provability” (Annals of Pure and Applied Logic28, 1985, pp. 217–254), but every time I sit down to work through this paper I give up in frustration at its density. I've been hunting around myself and asking some dialogue experts for help, and I've decided to work through C. Fermüller's “Parallel dialogue games and hypersequents for intermediate logics” (Automated Reasoning with Analytic Tableaux and Related Methods, International Conference TABLEAUX 2003, Rome, Italy, September 2003, Proceedings, Mayer, M. C. and Pirri, F. (eds.), pp. 48–64). This paper uses two techniques that may or may not prove to be relevant for the problem at hand (namely, parallel games and hypersequents); it's value for me at the moment is its proof of the soundness and completeness of so-called Ei dialogue games for intuitionistic logic. (That is not the aim of the paper, but Fermüller proves it en route to other ends.) The presentation is by no means simple, but it appears to be more accessible than Felscher's foundational paper. I thought it would be valuable to try to capture in one place my notes on the paper, since it holds out the promise of being a valuable resource for this problem and future dialogical problems. In this post I concentrate on the differences between the basic definitions employed by Felscher and Fermüller.

Language

Felscher treats propositional and first-order logic, but Fermüller focuses only on propositional logic. Negation is primitive for Felscher and ⊥ has no special significance. For Fermüller, ⊥ is a distinguished atom and negation is defined in the usual way (¬φ ≡ φ→⊥). This difference in language leads to differences in the authors's definitions of the particle rules and what it means for a dialogue to be won; see below.

Particle Rules

The particle rules for disjunction, conjunction, and implication are the same for both authors. Since negation isn't part of the language for Fermüller, he does not have a particle rule for negation, whereas Felscher does such a rule.

Fermüller permits Opponent to attack atoms; the assertion is denoted by “?” (i.e., it is not a formula, but a symbolic attack).

Structural Rules

Felscher defines various rulesets in his paper, but the one of interest in comparing Felscher's approach to Fermüller's is the ruleset E:

• D00: The game starts with Proponent asserting a non-atomic formula and alternates between Proponent and Opponent.
• D01: Attacks are always against composite formulas (and adhere to the particle rules).
• D02: Defenses are always against attacks (and adhere to the particle rules).
• D10: Proponent may assert an atom only if Opponent has already asserted it.
• D11: Defenses must be against the most recent open attack.
• D12: Attacks may be answered at most once.
• D13: Proponent's assertions may be attacked at most once.
• E: Opponent must react to Proponent's immediately prior statement.

Fermüller uses only one ruleset in his paper, which he calls “Ei”—the ‘E’ comes from Felscher's E rule (or ruleset), and the ‘i’ comes from the so-called ipse dixisti (“you said it”) rule, which, unfortunately, is not defined in Fermüller's paper. It has something to do with so-called material dialogues (dialogues in which, from the initial move, some formulas are allowed to be conceded by Opponent); see below.

Here are Fermüller's rules, verbatim:

• Start: The first move of the dialogue is carried out by O and consists in an attack on the initial formula.
• Alternate: Moves strictly alternate between players O and P.
• Atom: Atomic formulas, including ⊥, may be stated by both players, but can neither be attacked nor defended by P
• E: Each (but the first) move of O reacts directly to the immediately preceding move by P.

Let us look at these one by one:

• Start says that games begin with Opponent, not Proponent, as in Felscher (cf. rule D00). This has the advantage that every move of the game is either an attack or defense, unlike in Felscher, where all moves except the first are so.
• Alternate is identical to part of rule D00.
• Atom diverges from Felscher's D00 (and not only because Fermüller has ⊥ as a distinguished atomic formula): along with the other rules, it permits games to commence with atoms, which is ruled out by Felscher's D00. This rule leaves open the possibility of Opponent attacking or defending atoms; these are ruled out (for both players) by D01 and D02, respectively.
• E in Fermüller is the same as in Felscher.

Granted formulas

For Fermüller, the game does not commence simply with a formula but with a formula φ and a list Γ of granted formulas. The idea is that the game does not start from merely a formula, but with a formula and some “assumptions”, granted by Opponent to Proponent. Fermüller doesn't really say explicitly how these are used, but one can get a sense of that through his proofs, where the precise significance of the granted formulas Γ is revealed. The notion of granted formula also makes sense within the game: apart from the set Γ, a granted formula is (by definition) any formula asserted by Opponent.

Winning

Felscher says that Proponent wins a dialogue when

• it is finite,
• ends with a move by Proponent, and
• there are no legal extentions of the game.

Fermüller has a rather different definition. Proponent can win a dialogue in two ways:

• Opponent attacks a formula that has been granted (i.e., already asserted or given in advance of the game; see above), or
• O asserts (grants) ⊥.

For Fermüller, then, the game ends not with some “winning” move made by Proponent, as in Felscher, but with a “losing” move by Opponent. (As I've worked through Fermüller's paper and studied some of his proofs, this has been one of the differences with Felscher that I've had to pay careful attention to, since I can follow a line of Fermüller's thought but arrive at an unexpected conclusion.)

Dialogue tree

This term doesn't appear explicitly in Felscher, but the concept is there, in a way, in his definition of winning strategy, which are trees of a certain kind. So let us take some liberties here and say that Felscher does define dialogue trees, which are intuitively supposed to capture some “unfolding” of the game. Given a formula φ one can define the dialogue tree as the tree showing all logically possible ways the game could go. (Some branches may be infinite.) Inferring from his definition of winning strategy, we would say that a dialogue tree for Felscher for a formula φ is a rooted tree whose nodes are moves and whose branches are dialogues commencing with φ.

Fermüller defines dialogue trees explicitly in his paper. As for Felscher, dialogue trees are rooted trees and are supposed to capture some ways a dialogue can unfold. The main difference is that for Fermüller, the nodes of a dialogue are sequents Γ ⊢ φ and edges are labelled by moves. This is exactly the opposite of Felscher (when we keep in mind that the set of initially granted formulas in Felscher-style dialogues is always empty).

Although Felscher never defines the term, we can put words into his mouth and say that he defines P-node and O-node of a dialogue tree as nodes whose label are moves by P or O, respectively. (Felscher does say that some moves are “P-signed” and “O-signed”; the meaning is obvious.) For Fermüller, though, a P-node in a dialogue tree is a node representing a state of the game where P is to move next (and O-nodes are defined as nodes where it is O's turn to move next). I have informally understood P-nodes in a dialogue tree as moves where P has just moved; for Fermüller, we need to look to the future, not the past, to adhere to his usage of the term.

Winning strategy

Both authors define the this concept in the same way (but note that they disagree on what dialogues are, exactly, and what it means for Proponent to win).

So much for the differences in notation and basic definitions of Felscher and Fermüller; next up: examples of Fermüller-style dialogues and a comparison with Felscher.