Monday, October 25, 2010

Some notes on C. Fermüller's “Parallel dialogue games and hypersequents for intermediate logics” II: Dialogue sequents and states of the game

Yesterday's post on Fermüller's paper focused on the differences between his basic setup and Felscher's. Today I want to focus on some of the concepts that are most specific to Fermüller's approach. This is not to say that these concepts are absent from Felscher's paper. In fact, concepts similar to what I'm about to discuss probably do appear, in some form, in Felscher; the concepts are so basic, and in any case Fermüller credits Felscher but says that Felscher's techniques differ from his in some essential ways. The reason why I am not going to stop comparing Fermüller to Felscher at this point is because I've never managed to penetrate Felscher's paper in as much detail as I'm able to do with Fermüller's. One refreshing perspective in Fermüller's paper is the idea of moves in the dialogue acting on states:
Moves can be viewed as state transitions. In any state of the dialogue the (multiset of) formulas, that have been either initially granted or stated by O so far, are called the granted formulas (at this state). The last formula that has been stated by P and that either already has been attacked or must be attacked in O’s next move is called active formula. (Note that the active formula, in general, is not the last formula stated by P; since P may have stated formulas after the active formula, that are not attacked by O.) With each state of a dialogue we thus associate a dialogue sequent Π ⊢ A, where Π denotes the granted formulas and A the active formula.
Let's look at some examples illustrating this point of view of moves-as-transitions and see how the concept of granted formula, active formula, and dialogue sequent arise in some concrete games. In the following dialogue, and in all Fermüller-style dialogues in this post, the state column records what the dialogue state is after the move described in the first five columns in the same row. Thus the first row of the table doesn't record a move, but only displays the initial state of the dialogue.
Example 1: Fermüller-style dialogue for ∅ ⊢ pp.
∅ ⊢ pp1
  1. Initial state.
  2. The active formula remains unchanged from the initial state, since P hasn't asserted anything yet.
  3. Since there are no other formulas asserted by P at all and O must attack it, the active formula is now p.
  4. The granted formulas of the dialogue sequence constitute a multiset. Since p has now been asserted twice by O, we have registered that.
For the sake of comparison, let's look at how a [maximal] dialogue (indeed, the only [maximal] dialogue) for pp would go à la Felscher:
Example 1′: Felscher-style dialogue for pp
One difference is, of course, the absence from the Felscher-style dialogue of a state and its associated dialogue sequent. (Again, I am not claiming that Felscher does not employ this concept in his proof of the soundness and completeness of dialogue games for intuitionistic logic; I'm saying only that I haven't come across the concept in my failed attempts to read his paper.) Nonetheless, it should be plausible that a Felscher-style dialogue can be converted to a Fermüller-style dialogue: if the initial formula is φ then the initial state of the game is ∅ ⊢ φ, and we can make the game end in the Fermüller-style dialogue by making O attack some atom asserted by P that has already been conceded by O (which makes sense in light of Felscher's rule D10). And it should be plausible that one can map Fermüller-style dialogues to Felscher-style dialogues when the set Γ of granted formulas is empty, and these transformations are inverses of one another. The devil is in the details, obviously, and my suggested transformations may break when one seriously considers the differences in the rules employed by Fermüller and Felscher. But it seems natural enough to me that Fermüller's approach is just a syntactic variation of Felscher's; I'm confident that Fermüller is not trying to diverge conceptually from Felscher, but he employs different notation to ease his proofs. To get a better sense of granted formulas, let's look at a second example of a Fermüller-style game.
Example 2: Fermüller-style dialogue for pp
  1. Initial state.
  2. p is granted and copied to the left-hand side of the dialogue sequent from the previous state.
The game ends with a win for P because O has attacked a formula that has been granted. (In fact, the attacked granted formula is one of the initially granted formulas.) There is no Felscher-style analogue of this Fermüller-style dialogue because for the former there is no notion of formulas granted by O before the beginning of the game. Of course, the notion of non-initial granted formula makes sense for Felscher-style games: these are simply the formulas asserted by O during the course of the dialogue. To explore the concept of initially granted formulas, let's consider a further example:
Example 3: Fermüller-style dialogue for ppp
  1. Initial state.
  2. The active formula is unchanged, since P hasn't asserted anything yet. p is now granted.
  3. I'm assuming that the game can proceed in this way; I think that P can attack initially granted formulas. This makes sense to me for various reasons:
    • If the game actually ends at step 0 with a win for P, then there is no difference between the game for pp and the game for ppp, nor between ppp and, say, p∧(pq) ⊢ p. Surely the game has to proceed by analyzing the initially granted formula pp.
    • If the game does not end at step 0, then P has to either attack or defend. But surely he can't defend, since there's no attack against which to defend.
    For lack of any other notation, I've set the reference sot for this move as the intially granted formula pp (there's no number that I could put there, and I don't want to put simply “—”). The active formula remains unchanged, since ?L isn't a formula.
  4. p occurs twice in the multiset of granted formulas because it has been asserted twice now by O. This suggests, to my mind, some inefficiency in the mapping that will eventually be constructed from winning strategies to sequence calculus deductions in intuitionistic logic. These simple examples suggest to me that perhaps not all intuitionistic sequent calculus deductions will arise as the result of mapping winning strategies to derivations, but only those with some extra, redundant assumptions occurring on the left-hand side of ⊢.
This example puzzles me. I'd like to say that P wins this game: obviously ppp is intuitionistically valid, so P ought to have a winning strategy for it, and the winning strategy ought to be very simple. I'd like to say that the dialogue above (when regarded as a linear dialogue tree) actually is a winning strategy for P. But it feels weird to say that P wins here, because it feels that now P is trapped: he cannot attack p (by Atom). Fermüller does not include any non-repetition rules in his ruleset, so I suppose that P could repeat an earlier move or, say, re-attack the initially granted formula pp with ?R. But what good would that do? I must be missing something about the use of initially granted formulas and the ipse dixisti rule. Or maybe I don't understand one of the winning conditions: does P win here because O has granted a formula (at step 2) that he attacked earlier (at step 0)? Frustratingly, the ipse dixisti rule is not defined by Fermüller; I can only guess that it has something to do with the winning condition for P; the only reference I have at hand that talks about the ipse dixisti rule, Krabbe's “Formal systems of dialogue rules” (Synthese 63, 1985, pp. 295–328) says that the ipse dixisti rule is a a “‘winning remark’ that ends (at least a part of a) dialogue” (p. 300). This is frustrating for me, because I need to know precisely how this game will go if I am to understand Fermüller's proofs. Perhaps from the proofs, though, I'll be able to reconstruct what exactly the force of the ipse dixisti rule is. Let's look at a more complex example: one of the De Morgan formulas. Here's a Fermüller-style dialogue:
Example 4: Fermüller-style dialogue for ∅ ⊢ ¬(pq)→(¬p∧¬q)
∅ ⊢ ¬(pq)→(¬p∧¬q)1
0O¬(pq)Attack¬(pq) ⊢ ¬(pq)→(¬p∧¬q)2
1P¬p∧¬qDefend0¬(pq) ⊢ ¬p∧¬q3
2O?LAttack1¬(pq),¬p ⊢ ¬p∧¬q4
3P¬pDefend2¬(pq) ⊢ ¬p5
4OpAttack3p,¬(pq) ⊢ ¬p6
5PpqAttack0p,¬(pq) ⊢ ¬p7
6O?Attack5p,¬(pq) ⊢ ¬p8
7PpDefend6p,¬(pq) ⊢ p9
8OpAttack7p, p,¬(pq) ⊢ p10
  1. Initial state.
  2. O grants ¬(pq). Active formula is unchanged. (It never changes after O moves.)
  3. The active formula is now ¬p∧¬q because O must attack this new statement by P. In general, any time P defends, the next move by O is an attack on whatever P just asserted, thanks to the E rule.
  4. ¬p is now granted.
  5. The active formula is now ¬p, because P just defended. See note 3.
  6. p is now granted.
  7. The active formula is unchanged because O does not need to attack this formula, because he could defend against the attack at move 5 by asserting ⊥ (recall that “¬(pq)” is actually (pq)→⊥). At step 6, O will in fact attack the disjunction asserted by P at step 5; the point is that, when calculating what formula is active, one needs to consider what Omust do.
  8. The state after this move is identical to the previous two states!
  9. p is now the active formula because P just asserted p as a defense. See note 3.
  10. p has now been granted twice. Again we see a bit of redundancy in the assignment of sequents to dialogue states.
The game ends at move 8 with a win for P because O just attacked a formula that he already granted at step 4. The game could have gone differently: at step 6, for example, O could have defended against the attack at move 5 by asserting ⊥, which would have led to a loss for him at that step. And of course O could have asked O to defend the right conjunct rather than the left one at step 2. There are even more ways the game could have gone, but these alternatives need not distract us here. For comparison, here is the Felscher-style game analogous to the one of Example 3:
Example 4&prime: Felscher-style dialogue for ¬(pq)→(¬p∧¬q)
The Felscher-style game ends here because there are no more moves availabe for O to make at this point. So much for concrete dialogue games à la Fermüller. One can then see how Felscher-style dialogue trees are, because these are simply derived from treating Fermüller-style dialgues. Of course, all of the examples above of Fermüller-style dialogues can be regarded as extreme cases of Fermüller-style dialogue trees if we simply ignore all possible branching (which does exist whenone considers the De Morgan formula of Example 4, but not in the other dialogue sequents, owing to their simplicity). Next up in this series on Fermüller's paper: a discussion of Fermüller's proof of his Theorem 1, on the soundness of Ei-dialogues for intuitionistic validity (i.e., Proponent has a winning strategy for a formula φ iff φ is intuitionistically valid).

Sunday, October 24, 2010

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.
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.
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.

A simple dialogical characterization of the logic LQ of weak excluded middle?

I've recently returned to a problem about dialogues and the propositional logic LQ of weak excluded middle: is it true that if, in Felscher's ruleset E for intuitionistic logic, one changes the rule
Proponent may assert an atom p only if Opponent has already asserted p
Proponent may assert an atom p only if Opponent has already either asserted p or asserted ¬p
but leaves all other rules unchanged? If one relaxes the restriction on Proponent's use of atoms as described, then the law of weak excluded middle ¬q∨¬¬q becomes valid, while the usual law of the excluded middle q∨¬q remains invalid. This naturally suggests, in light of the soundness and completeness of the ruleset E for intuitionistic logic, that the modified ruleset characterizes the logic LQ of weak excluded middle, a fascinating superintuitionistic logic. My interest in LQ comes from constructive mathematics, but in any case, the problem is now purely a dialogical one. I'm not invested one way or the other in this result, but I would like to try to show that this simple change in one of Felscher's rules gives rise to an interesting known logic. Of course, a simple counterexample would be nice, too, but so far I've not found any. The problem here is unlike the case of N, which (for the moment) has no known characterization or meaning outside the context of dialogues.

Friday, October 22, 2010

Characterizing N-validities

One of the key theorems of our first paper on N was the theorem characterizing valid implications:
Theorem 3: Every N-valid implication φ->ψ satisfies one of the following three conditions:
  1. φ is atomic.
  2. φ is negated.
  3. ψ is N-valid.
Last week I spent some time trying to come up with similar characterizations of validities of other types, that is, characterizations of N-valid atoms, negations, disjunctions, and conjunctions. Three of the four are easy:
  • No atom is N-valid [Lemma 2].
  • The only N-valid negations are double negations of validities [Theorem 4].
  • A conjunct is N-valid iff each conjunct is N-valid [obvious].
So, can we characterize disjunctions? Suppose φVψ is N-valid. There are three cases:
  1. Either φ is N-valid or ψ is N-valid.
  2. Neither disjunct is N-valid, and neither contains any implication.
  3. Neither disjunct is N-valid, but at least one contains an implication.
In the first case, nothing more is needed. For the other two, I have a
Conjecture: (2) At least one atom occurs at least twice in the formula, once with an odd number of negations and once with an even number of negations. NOTE: I do not mean occurs "within the scope of an odd/even number of negations" (as you would find in classical logic) but that attached to the atom itself are an odd or even number (0, of course, being an even number). (3) At least one atom occurs both in the antecedent of a conditional and in either the consequent of a conditional or as a stand alone atomic subformula. (If we wanted a more felicitous phrasing, we could say that an atom is the consequent of a trivial conditional, and then say: "at least one atom occurs in both the antecedent and the consequent of a conditional". But Jesse found this problematic.)
Now we have the following open problem: Prove the conjecture, or find a counterexample.

Thursday, October 21, 2010

Is uniform substitution consistent with N?

One of N's curious features is its failure to validate uniform substitution: it is not true that
for all substitutions f (i.e., functions from atoms to formulas) and for all formulas φ: if φ is N-valid then f(φ) is N-valid.
For example, the formula p→¬¬p is N-valid, but if we plug in qq for p we get (qq)→¬¬(qq), which turns out to be N-invalid. Although N does not validate uniform substitution in its full generality, N is closed under some classes of substitutions:
  • renamings of atoms
  • double negating atoms
We have proofs that N is closed under these kinds of substitutions. We suspect further that N is closed under
  • substituting N-validities for atoms,
but we lack a proof for this third case. Question: how to respond to N's failure to validate uniform substitution? There are a number of possibilities that are worth investigating, but I want to explore one approach here: is N consistent with uniform substitution? More precisely, the question can be put this way. Let N′ be the closure of N under uniform substitution (i.e., N′ is the smallest set of formulas extending N that is closed under uniform substitution). We then ask:
  1. Is N′ consistent? (We can vary the notion of consistency here, thereby precisifying the question.)
  2. Does N′ have a suitably straightforward dialogical characterization?
We might further ask: what is it about Felscher's rule E (“Opponent must respond to the immediately prior assertion by Proponent”) that ensures closure under uniform substitution? Recall that our logic N is characterized simply by dropping the rule E from a ruleset known to characterize classical logic, which of course is closed under uniform substitution. We thus know that “Rule E” is not the answer to question 2 above that we seek!

Thursday, October 14, 2010

Live, from Indonesia

Tuesday afternoon, Jesse and I released N into the wild. He gave a talk introducing the website (look for significant improvements to it soon!) and then I spoke about N and the challenges of developing a proof theory for it. I think we rather perplexed the audience, as there was only one person in it that had ever heard of dialogical logic before, and we only had 20 minutes between the two of us. A substantive blog post will come soon; I've got a couple of topics that have been rattling around in my mind.