Reasoning from assumptions

Just a note to remind myself that Lorenzen, Constructive Philosophy, pp. 89ff has some interesting things to say about reasoning from assumptions in the dialogical framework.

Consistency of N with uniform substitution

N does not validate uniform substitution. Many simple failures of uniform substitution can be found: p→p is valid in N, but the instance (p∧p)→(p∧p) isn't. (Verify this at our dialogical logic sandbox!) There are many other failures of uniform substitution (infinitely many, in fact).

This is a somewhat awkward feature of N. Earlier, I asked whether uniform substitution consistent with N: is the closure of N under uniform substitution consistent? Another way to put this is to ask whether uniform substitution is an admissible rule of inference for N.

The answer is “yes”; here is a simple proof, exploiting the fact that N is sub-classical. Let N′ be the closure of N under uniform substitution; we need to show that N′ is consistent. Suppose that there were a formula φ such that both φ∈N′ and ¬φ∈N′. There are formulas α and β in N such that φ is obtained by an application of uniform substitution from α and likewise ¬φ is obtained by an application of uniform substitution from β. Since α∈N, α is a tautology; and since classical logic CL is closed under uniform substitution, φ is a tautology, too. Likewise, ¬φ is a tautology. But that's impossible!

(Thanks to Benedikt Löwe for this nice solution.)

Searching for wins as a constraint satisfaction problem I: Ruminations on a constraint language

I'm just now returning to some ideas that I had while in Indonesia at LPAR-17 about viewing the search for wins (which in this post, unless otherwise indicated, will be ambiguous between “winning play” and “winning strategy”). My question:

Can we profitably view the search for wins as constraint satisfaction problems?

The current code does implement a primitive kind of constraint satisfaction procedure as follows: the constraint variables are

• PLAYER, the player of the move,
• STATEMENT, the statement (i.e., formula or symbolic attack) to be asserted by PLAYER,
• STANCE, the stance (attack or defend) that PLAYER will take,
• REFERENCE
, the number of the move to which this move is a response.

The constraints are simply Lisp predicates in whose definitions PLAYER, STATEMENT, STANCE and REFERENCE are free (Lisp) variables. Testing whether a constraint is satisfied just means assigning the values specified by a candidate solution to the Lisp variables in the predicate, and then simply evaluating the predicate. Given some dialogue ruleset R and a sequence ⟨s₁,…s_n⟩ of moves, we then simply enumerate all possible values for PLAYER, STATEMENT, STANCE, and REFERENCE that satisfy all the constraints. The current approach is less than ideal for several reasons:

• the enumeration of possible values for the variables is brutish: we simply enumerate all possible values for each of the contsraint variables: STANCE ∈ {Attack,Defend}, PLAYER ∈ {P,O}, STATEMENT ∈ sub(φ) ∪ {?_L,?_R,?}, REFERENCE ∈ [0,…n], and check whether all constraints are satisfied. This obviously blows up, as the game proceeds (the domain of the variable REFERENCE grows).
• no techniques from constraint solving are used (there's no propagation, consistency checking, etc).

So as it stands, only in the most primitive sense can it be said that we use constraint solving techniques to search for wins, and that's being charitable. Let's stick with these constraint variables—PLAYER, STATEMENT, STANCE, and REFERENCE—and see what kinds of issues come up.

• The variable PLAYER has only two possible values. Actually, the only reason why I even consider this to be a variable that varies at all is because I was interested in exploring dialogue rulesets in general, including rulesets that permit, say, a player to take multiple moves. This perspective is interesting, but so far nothing has come of it in my research (I haven't taken any steps to see what happens when players can take multiple turns). In the interest of performance, then, one could limit the generality of my approach and consider only alternating games. In that case, the value of the PLAYER constraint variable is always determined by the number of the move we're at, and it could be deleted. (Note that doing this would cut down by one half the number of possible moves to consider, which is nothing to sneeze at.)
• The observation that PLAYER takes on only two possible values led me to wonder about encoding part of the constraint satisfaction problem as an instance of SAT. We could conceivably encode the entire search for wins as a SAT problem, but I digress.
• With these four variables (or three, if we ditch PLAYER), what are the constraints? What's a suitable representation of dialogue rules? Let's look at an example. Felscher's dialogue rule D10 says: “P may assert an atomic formula only after it has been asserted by O before”. We might naively represent this in a first-order way using our constraint variables thus:

  PLAYER = P ∧ atomic(STATEMENT) → [ ∃k (k < ⟨TURN⟩ ∧ player-at(k) = O ∧ statement-at(k) = STATEMENT) ]

  This is a bit of a mess. Evidently we'll need the predicate "atomic", which can be applied to the variable STATEMENT to require that STATEMENT is an atomic formula. “⟨TURN⟩” isn't really a constraint variable, but is a parameter whose value comes form outside, as part of the specfication of the CSP. player-at is a function of natural numbers; given k, it gives the player who played at turn k. statement-at is another function of natural numbers; given k, it gives the statement made at move k. This may or may not actually be the constraint. Since we know ⟨TURN⟩, we could expand the existential quantifier, so that the contraint would be something like

  PLAYER = P ∧ atomic(STATEMENT)

  →

  P = O ∧ statement0 = STATEMENT ∨ O = O ∧ statement1 = STATEMENT ∨ P = O ∧ statement2 = STATEMENT …

  That is, we make a big disjunction and compute player-at and statement-at for each one. Evidently, some of these disjuncts are unsatisfiable because they contain equations such as “P = O”. We could further expand this one constraint into even more constraints by using the equivalence between p→(q∨r) and (p→q)∨(p→r), so that this implicational constraint generates a disjunctive constraint. This gives us an opportnity for parallel processing.
• The only propositional signature used by the site right now is one that has 26 atoms, whose names are simply the letters of the alphabet (case doesn't matter). We could expand any mention of the predicate atomic(STATEMENT) into a disjunction with 26 disjuncts STATEMENT = A ∨ STATEMENT = B ∨ …. We can refine this even further (again, at a cost of restricting the generality of the tool) by looking only at the atoms that are mentioned in the initial formula. (The generality of the site is restricted by doing this because it makes sense only for those rulesets where subformulas of the initial formula [or possibly symbolic attacks] appear.)

These are just some initial thoughts. I've used Felscher's D10 as an example, but we of course need to treat the other dialogue rules as well. It would be nice if, like D10, these can be reduced to boolean combinations of equations between constraint variables and ‘constants’ (like ‘P’).

Some notes on C. Fermüller's “Parallel dialogue games and hypersequents for intermediate logics” IV: Some worries about the proof of Theorem 1

In a previous post I suggested that there's something wrong with Fermüller's proof of Theorem 1:

For every winning (Ei-)strategy for Γ ⊢ C there exists an LI′-deduction of Γ ⇒ C

I have found two problems with the proof:

1. the induction predicate is wrongly stated, and
2. even with a correct induction predicate, the proof suffers from a gap; the gap may be fixable, or it may illustrate a genuine error.

This post explains the problems, as I see them.

Problem 1. The induction predicate is wrongly stated.

The actual statement being proved is, so far as I can see,

for all multisets Γ, all formulas C, and for all Ei-winning strategies τ for Γ ⊢ C having depth d: for every P-node of τ there is an LI′-deduction of the sequent corresponding to the dialogue sequent at the node.

Another possibility: for all multisets Γ, all formulas C, and for all Ei-winning strategies τ for Γ ⊢ τ:

if τ has depth d, then for every P-node of τ there is an LI′-deduction of the sequent corresponding to the dialogue sequent at the node.

In this second formulation, τ is a parameter of the statement to be proved by induction. The first formulation quantifies over Ei-winning strategies (and multisets and formulas). The proof is by strong induction on d. The proof goes by checking the “base case” where d = 1, and then checking the “inductive step” where d > 1. There are three problems here; the first two are essentially stylistic and easily remedied, but the third is more difficult:

• What about the case d = 0?

  The case of d = 0 amounts to considering the possibility of an Ei-winning strategy consisting of a single node, the root, and no other nodes; this can be proved to be impossible, by the definitions of Ei-games, what it means for P to win an Ei-dialogue, and Ei-winning strategy. So the induction predicate holds vacuously.

  So there's nothing really wrong with ignoring the case of d = 0, but the justification for ignoring it does rely on a little lemma.

• Judging from the statement of the “inductive step”, the proof is by strong induction; so why is the case of d = 1 singled out as the “base case”?

  The ordinary structure of a proof by strong induction, with an induction predicate A is to show ∀nA[n] by proving:

  ∀ k ((∀ j (j < k → A[j]) → A[k])

  In a proof by strong induction there is no “base base” as there is in a proof by vanilla induction of ∀ nA[n], where the task is to prove the conjunction:

  A[0] ∧ ∀ k (A[k] → A[k+1])

  In a proof by strong induction the sole proof obligation ∀ k ((∀ j (j < k → A[j]) → A[k]) is, I suppose, the “inductive step”. The proof now goes as follows. Let k be a natural number. There are three cases:

  • k = 0. We have already discussed that A[0] holds vacuously, so (∀ j (j < 0 → A[j]) → A[0] is true.
  • k = 1. Fermüller satisfactorily deals with this case (but note that we can actually prove A[1] outright; we don't need the help of (∀ j (j < 1 → A[j]), which in any case is useless since A[0] holds vacuously).
  • k > 1. The hypothesis (∀ j (j < k → A[j]) evidently is used in to dispose of this case. (But see below!)

  So a minor reformulation of the argument rescues the proof. It is not a proof by vanilla “step-by-step” inductuion, but a proof by strong induction. There is no “base case” exactly analogous to the proob obligation A[0] in a proof by vanilla “step-by-step” induction, but the same proof obligation does arise as a bona fide case in a proof by cases (which proof by induction, strong or weak, manifestly is not).

  There's nothing deep here, but I thought I'd mention it because things like this do catch my eye as sources of potential trouble.

• Can this proof by induction succeed at all?

  I don't think so; neither of the induction predicates I've stated above is suited to the task.

  • First formulation. Recall that this formulation quantifies over winning strategies. Our task is to prove, in the case where d > 0, that, for every multiset Γ of formulas and every formula C, and for every Ei-winning strategy τ for Γ ⊢ C having depth d, that for every P-node of τ there exists an LI′-deduction of the sequent corresponding to the dialogue sequent at the P-node, assuming that this is true for all d′ < d.

    Given Γ, C, τ, and d, then, we have to show that every P-node u of τ has the desired property. Fermüller distinguishes between the stance—attack or defend—that P will take when moving from u to its successor. In either case, Fermüller claims that the induction hypothesis allows us to conclude that there exist suitable LI′-deductions for the P-node (or nodes) immediately below u.

    But this makes sense only if we can construe the tree (or trees) built from the O-node (or nodes) immediately below u as themselves being Ei-winning strategies. And I don't see how that can be done.

    Consider the following Ei-game for the W-formula (p→(p→q))→(p→q). P wins (which is unsurprising, since this is the principle type for the typeable term λxy.xyy in the simply typed λ-calculus):

    An Ei-dialogue for the W-formula

    Move	Player	Statement	Stance	Reference	State
    					⊢ (p→(p→q))→(p→q)
    0	O	p→(p→q)	Attack	—	p→(p→q) ⊢ (p→(p→q))→(p→q)
    1	P	p	Attack	0	p→(p→q) ⊢ (p→(p→q))→(p→q)
    2	O	?	Attack	1	p→(p→q) ⊢ p
    3	P	p→q	Defend	1	p→(p→q) ⊢ p
    4	O	p	Attack	3	p,p→(p→q) ⊢ p→q

    Consider this dialogue as a branch of an Ei-winning strategy for the W-formula. Question: if we really cut just delete nodes from an Ei-winning strategy and get another Ei-winning strtagy (for a different initial dialoguq sequent), what happens when we chop off the top two nodes? Naively, we get this:

    Naive truncation of an Ei-dialogue for the W-formula

    Move	Player	Statement	Stance	Reference	State
    					p→(p→q) ⊢ (p→(p→q))→(p→q)
    0	O	?	Attack	—	p→(p→q) ⊢ p
    1	P	p→q	Defend	—	p→(p→q) ⊢ p
    2	O	p	Attack	1	p,p→(p→q) ⊢ p→q

    I've already adjusted the labels in the Move and Reference columns (not adjusting them truly results in nonsense). But notice that the game has become incoherent for other reasons:

    • the initial dialogue sequent is p→(p→q) ⊢ (p→(p→q))→(p→q), but O initial move in this truncated game is ?, which makes sense only if the right-hand side of the initial dialogue sequent were an atomic formula, but it is actually (p→(p→q))→(p→q). Moreover, the active formula after O's initial move should be (p→(p→q))→(p→q), not p.
    • P's move at step 1 is partly sensible (putting aside the nonsense of O's move at step 0), but the active formula of the dialogue sequent after this move is still wrong.
    • The only move that makes sense in its entirety (assuming the meaningfulness of the previous moves) is the final move at step 2 by O.

    One could complain that this naive truncation is simply too naive. Instead of copying the dialogue sequent after move 1 in the original game and making it the initial dialogue sequent of the truncated game, we should be more intelligent and note that O attacks p at move 2, so that should be the initial active formula. According to this proposal, then, the truncated branch looks like this:

    Less naive truncation of an Ei-dialogue for the W-formula

    Move	Player	Statement	Stance	Reference	State
    					p→(p→q) ⊢ p
    0	O	?	Attack	—	p→(p→q) ⊢ p
    1	P	p→q	Defend	—	p→(p→q) ⊢ p
    2	O	p	Attack	1	p,p→(p→q) ⊢ p→q

    In this more intelligent truncation of the original game, the initial move by O now makes sense in its entirety. But move 1 by P does not make sense: O just attacked an atomic formula, and P defends against that attack by asserting an implication! This violates two rules: Atom, which says that P cannot defend against attacks on atoms, and the particle rules, because only against attacks on composite formulas could a defense be given.

    If there's no way of truncating the original game for the W-formula, considered as a branch of an Ei-winning strategy, then I see no way how this the first formulation of the induction predicate can be rescued. Certainly there's no discussion of producing Ei-winning strategies from parts of Ei-winning strategies in the paper. Quantifying over winning strategies must not be what was intended.

  • Second formulation. Recall that in this formulation, the Ei-winning strategy τ appears as a parameter.

    This understanding of the induction predicate can be dispensed with quite quickly: the assumption that the induction predicate holds for all d′ < d is useless in showing that if τ has depth d, then for all P-nodes of τ…, since if τ has depth d then it can't any other depth d′.

  Problem 2. Even if the induction predicate is correctly stated, the proof may still be erroneous.

  The discussion of Problem 1 is, to some extent, dispensible, because in a previous post I articulated what I take to be the actual induction principle at work in the proof of Theorem 1. I wanted to take some time just to make clear, though, that what is literally written in the paper is in need of rescue. However, even with the induction principle tweaked in a way that strikes me as most sensible, the proof still seems to me to be open to criticism, and possible even mistaken.

  Here's the problem: in the case where we consider trees of depth d > 1, we focus on P-nodes and distinguish between the stance—attack or defend—that P could take in his next move. Fermüller considers these cases, and how O might react. He applies the induction hypothesis at the P-node (or nodes) immediately below the current P-node to get LI′-deductions, from which he constructs a suitable LI′-deduction for the current P-node. But there is a problem here: what if the P-node (or nodes) immediately below the current P-node are leaves of τ? Another way to state my worry: are we sure that the induction predicate holds for the case d = 2?

  Another way to state my worry: are we sure we really know how to compute the winning strategies that the proof of Theorem 1 is supposed to give us?

  In his handling of what he calls the “base case”, Fermüller shows how to construct LI′-deductions for the P-node (!) of τ. But this is easy because the game has only one move in it, the “losing” move by O. How do we deal with the leaf nodes of τ in the general case?

  To illustrate my concern, turn to the earlier Ei-dialogue for the W-formula. Look at the dialogue after move 2. We are considering case (a) of Fermüller's proof, where P defends against an attack on an implication, which in this case is the whole W-formula itself. Folowing Fermüler's proof, O has a unique response, and we return to a P-node. Fermüller now says that the inductive hypothesis should give us an LI′-deduction for the sequent corresponding to the dialogue sequent at this node, which in this case is a leaf of the winning strategy τ. Now, it is clear that there is an LI′-deduction for the sequent p,p→(p→q) ⇒ p→q. But it is not an axiom of LI′.

  But if we compare how Fermüller disposes of the “base case”, we see that he assigns axioms of LI′ to the leaf P-node of τ. That's clearly not available here, in the case of the W-formula.

  Moreover, note a mismatch between how Fermüller sets up his case (a) and what we see in the dialogue for the W-formula: the dialogue sequent at the P-node in question does not match Fermüller's pattern: he says that from P's defense of an attack on an implication, we can infer that the active formula at the current node is the implication itself. This is clearly not the case here: the active formula at the current P-node is p, because that is what O most recently attacked.

  Some possible responses:

  • What I think is an Ei-dialogue isn't actually an Ei-dialogue.

    But it looks like an Ei-dialogue to me. I think I understand Ei-games, but I'm happy to accept that I'm missing something crucial.

  • I'm miscalculating the active formula.

    I don't believe I am. The active formula after O's move at step 2 is p because that is formula asserted by P that O has most recently attacked; there is no issue of a forced O attack on any other formula, since O could have defended at step 2 by defending against the attack of move 1.

  • The proof is mistaken.

    This seems quite possible to me.

    I can't account, for example, for why Fermüller thinks that, if P is about to defend, then (treating only the implication-only fragment of propositional logic for the moment) the active formula is an implication. In my example, it is an atom. P, unlike O, is not constrained to respond to the most recent assertion of the other player; in my example above, P defends against something other than the most recent statement by O.

  This proof feels out of control to me…

Breaking: counterexample to a simple proposal for characterizing the logic LQ of excluded middle

A while ago, I proposed a simple dialogical characterization of the logic LQ of weak excluded middle (also known as Jankov's logic). (See my earier post on the subject.) The idea is, simply, to replace the usual Felscher rule D10, which says

P can assert an atom p only if O has already asserted p

to

P can assert an atom p only if O has either already asserted p or already asserted ¬p.

Chris Fermüller has kindly provided a counterexample to the claim that the usual rules for intutionistic logic, with D10 replaced by this modified version of it, generates LQ: the formula ¬p→p is valid in this setting! The idea is that O asserts ¬p, then P can assert p and win the game. That ¬p→p is not valid in LQ is clear because the formula is not classically valid, and LQ is an intermediate logic. Back to the drawing board…

Some notes on C. Fermüller's “Parallel dialogue games and hypersequents for intermediate logics” III: Soundness of (existence of winning strategies for P in) dialogues for intuitionistic logic

The last two posts in this series (part 1, part 2) focused on the basic setup of Fermüller's paper. It has been good for me to go through the basics in as much detail as I have because I have learned of dialogues only through Felscher (more or less), so he's all that I know. Since there are so many niggling differences between Felscher and Fermüller, and because those details really do matter (we're doing proof theory here, right?), it's been good for me to dwell on the basic setup. But now the time has come to take a look at Fermüller's Theorem 1, which says that winning strategies for dialogue sequents Γ ⊢ φ (for P, the only kind of winning strategy of interest in this context) exist only for intuitionistically valid sequents: if there is an Ei-winning strategy for Γ ⊢ φ, then Γ ⇒ φ is an intuitionistically valid sequent. What follows is a careful annotation of Fermüller's proof.

Preface

Fermüller introduces a variant, which he calls LI′ of a standard sequent calculus LI for intuitionistic logic. In addition to weakening, contraction, and cut, the following are rules of LI′: LI′ differs from LI only slightly: LI treats sequents with empty right-hand sides, but by inspecting the rules one can see that such sequents don't appear in LI′ deductions. This is possible because ⊥ is available. Fermüller states that LI′ is sound and complete for intuitionistic logic. This is important, but we can take this for granted at the moment without investigating why it is so (soundness is obvious). Fermüller states a lemma, Proposition 1, which is a technical theorem about LI′ deductions whose right-hand side is an implication. Proposition 1: A,Γ ⇒ A→B is provable in LI′ iff Γ ⇒ A→B is provable in LI′. Fermüller doesn't prove this, but let's see how a proof might go. Proof of Proposition 1: If LI′ ⊢ Γ ⇒ A→B, then, by weakening, LI′ ⊢ A,Γ ⇒ A → B (the desired LI′-deduction can be obtained from the LI′-deduction d given by assumption by adding an application of weakening to the bottom of d). Going the other way around requires a bit more work. Rather than redeveloping the theory of inversion, cut elimination, etc., or LI′, let's just take a shortcut and use the fact that LI′ is sound and complete for intuitionistic logic. (Actually, Fermüller probably has something like this in mind: he says that Proposition 1 is a corollary to soundness and completeness of LI′.) Thus: if LI′ ⊢ A,Γ ⇒ A→B, then LI′ ⊢ Γ A→(A→B). By soundness, Γ ⊢ A→(A→B) is an intuitionistically valid sequent. So is Γ ⇒ [A→(A→B)]→(A→B), so Γ ⇒ A→B is intuitionistically valid (modus ponens), whence, by completeness, LI′ ⊢ Γ ⇒ A→B. Later we'll investigate the question of the purpose of switching to LI′ from a standard sequent calculus for intuitionistic logic. With these background pieces out of the way, we can proceed with Theorem 1.

Theorem 1

Here's how Fermüller states it:

Every winning strategy τ for Γ ⊢ C (i.e., for dialogues with initial formula C, where player O initially grants the formulas in Γ) can be transformed into an LI′-proof of Γ ⇒ C.

Annotated Proof of Theorem 1

1 We prove by induction on the depth d of τ that for every P-node of τ there is an LI′-proof of the sequent corresponding to the dialogue sequent at this node.

Recall that for Fermüller P-nodes in a dialogue tree/winning strategy represent moves where O is about to play; they thus correspond to moves where O has just played. Recall also that nodes in Fermüller dialogue trees are states, not moves; the edges of Fermüller dialogue trees are the moves. The root node, having depth 0, is thus an O-node, since, by the Start rule, O begins the dialogue. Since P wins a Fermüller-style game when O makes a “losing” move, the leaves of a winning strategy—which correspond to wins for P—are all P-nodes: at the end of a dialogue where P wins, it is P's turn to move, even though he in fact makes no further moves (since the game is over). Winning strategies are by definition finite, so proof by induction is a valid method of proof here. The proof will actually proceed by strong induction, not just vanilla “k to k+1” induction. The depth of a tree isn't defined by Fermüller, but it is presumably just the length of the longest path from the root to a leaf. We will show the existence of LI′-deductions for everyP-node of τ. The LI′-deduction for Γ ⊢ C will presumably be constructed bottom up from the LI′-deductions assigned to the leaves of τ.

2 That this implies the theorem is obvious for the cases where C is either atomic, or a disjunction, of a conjunction; because, in those cases, the dialogue sequent at the P-node(s) immediately succeeding the root is (are) identical to Γ ⊢ C. In the case where C = A→B, the P-node succeeding the root carries A,Γ ⊢ A→B as dialogue sequent; and thus the theorem follows from Proposition 1.

Fermüller here is arguing that

(*) for every P-node of τ there is an LI′-proof of the sequent corresponding to the dialogue sequent at this node,

which we're about to prove by induction, implies that

(**) τ can be transformed into an LI′-proof of Γ ⇒ C,

where τ is a winning strategy for Γ ⇒ C. Let's try to unpack this argument. Proceeding by cases:

• If C is atomic, then, by Start, the first move is by O and is an attack ? on C:

  Move	Player	Statement	Stance	Reference	State	Notes
  					Γ ⊢ C	1
  0	O	?	Attack	—	Γ ⊢ C	2
  ⋮						3

  Notes:
  1. Initial state. C is atomic.
  2. Nothing further is conceded by O, since “?” isn't a formula.
  3. The game may or may not continue beyond move 0. If Γ is empty, then the game cannot continue, though P does not win. (Here is yet another difference between Fermüller and Felscher: in Felscher-style games, a player wins if the other player cannot make any moves. Here, P cannot move (I think), but the winning conditions for P are not satisfied.) If Γ is not empty, then the game can, presumably, continue.
  Assuming (*), we get the desired conclusion (**) because the P-node N associated with the state after move 0 carries the exact same sequent as the one for which we are trying to find an LI′-deduction: the LI′-deduction assigned to N is the one we want.
• If C is a disjunction A∨B, then the game proceeds thus:

  Move	Player	Statement	Stance	Reference	State	Notes
  					Γ ⊢ A∨B	1
  0	O	?	Attack	—	Γ ⊢ A∨B	2
  ⋮						3

  Notes:
  1. Initial state.
  2. The multiset of granted formulas is unchanged because “?” isn't a formula.
  3. Unlike the previous atomic case, the game is necessarily continuable here, in one of two or possibly three ways:
     1. P can defend against the attack of move 0 by asserting A,
     2. P can defend against the attack of move 0 by asserting B, or
     3. if Γ contains a non-atomic formula, P can attack it.
  As in the atomic case, Femüller's point in saying that it is “obvious” that (*) implies (**) in the case where C is a disjunction is simply that dialogue sequent of the initial state is identical to the dialogue sequent after O's first move, so (**) follows simply because we can take the LI′-deduction assigned to the P-node that immediately follows the root; this deduction exists by (*).
• If C is a conjunction A∧B, then the game can open in two ways:

  Move	Player	Statement	Stance	Reference	State
  					Γ ⊢ A∧B
  0	O	?L	Attack	—	Γ ⊢ A∧B
  ⋮

  or

  Move	Player	Statement	Stance	Reference	State
  					Γ ⊢ A∧B
  0	O	?R	Attack	—	Γ ⊢ A∧B
  ⋮

  In both cases, the games are continuable past move 0, but we cannot say exactly what the next move will be if Γ is non-empty: P need not defend immediately against O's attack, but may attack a (non-atomic) formula in Γ. If Γ is empty, then we can say what P will (must) do at step 1: the only available move is to defend against the attack(s). But since the figures are supposed to be valid whether Γ is empty or non-empty, we can't say what will happen at move 1. The point is that O can attack the initial statement in two ways (?_L, ?_R). The winning strategy τ thus branches immediately after the root. Still, as in the atomic case and the disjunction case, that (*) implies (**) in this case is easy to see because the dialogue sequents assigned to both successors of the root node (which are both P-nodes) are identical; (*) tells us that from these we can find LI′-deductions for both of them; so (**) follows by just picking one. (Thus an element of nondeterminism is introduced into the proof: how do we know that the two LI′-deductions assigned to the left and to the right P-nodes that succeed the root are identical? For all we know, they could be different, and so a genuine choice may need to be made. We can put aside for now the question of whether this conceivable situation is mathematically possible.)
• The most interesting case is where C is an implication A→B. The dialogue begins thus:

  Move	Player	Statement	Stance	Reference	State	Notes
  					Γ ⊢ A→B	1
  0	O	A	Attack	—	A,Γ ⊢ A→B	2
  ⋮						3

  Notes:
  1. Initial state.
  2. A is granted. Active formula remains unchanged.
  3. As usual, we can't say exactly what will happen now. If Γ contains a non-atomic formula, then P can attack it at move 1. Even if Γ is empty, there's more than one way the game could go: P could defend against the attack of move 0 by asserting B, or P could attack O's assertion of A (unless A is empty—rule Atom is in effect).
  The dialogue sequent at the P-node succeeding the root is thus A,Γ ⊢ A→B. Notice that we are precisely in the situation where Proposition 1 helps us: we want a LI′-deduction of Γ ⊢ A→B, but what we have, by (*), is an LI′-deduction of A,Γ ⊢ A→B. Proposition 1 saves us by ensuring the existence of an LI′-deduction of Γ ⊢ A→B, so (**) follows, as desired.

So much for the sufficiency of the proposed method for proving our theorem. Ready to continue?

coffee/tea break

3 The base case, d = 1, follows from the fact that the P-node (or, in case of C being a conjunction, the two P-nodes) succeeding the root is a (are) leaf node(s). This implies that one of the winning conditions—C∈Γ or ⊥∈Γ—must hold. Consequently, the corresponding sequent Γ ⇒ C is an axiom.

Why is d = 1 the base case rather than d = 0? Well, could τ have depth 0? No, this is impossible. Observation 1: no matter what Γ and C are, every winning strategy for Γ ⊢ C has depth ≥ 1. Proof: A winning strategy τ of depth 0 for Γ ⊢ C would exist only if O could not even start the game. (Again, keep in mind that nodes in winning strategies are dialogue sequents, not moves; edges represent transitions from states (i.e., dialogue sequents) and are labelled by moves.) But no matter what C is, O can always attack C (and must do so, by Start). Thus τ consists not merely of a root node, but has at least one outgoing edge. □ Fermüller begins his induction with d = 1, but he could have begun with d = 0. He would then have to use Observation 1 to show that this is impossible, so the base case is dispensed with vacuously. But then in the induction step he would have to deal with the case where d = 1, which would be inelegant. So he starts at 1, which is the simplest possible case. That there are winning strategies having depth exactly 1 can be seen by inspecting Example 2 from yesterday. I hope you can convince yourself that that simple concrete dialogue can be regarded as a winning strategy (there's no branching to consider). If the game ends with a win for P after O's initial move, then, by definition, either

1. O just attacked a formula that's contained in the multiset Γ of initially granted formulas, or
2. O just asserted ⊥

In the first case, we have that C ∈ Γ, so the promised LI′-deduction is the axiom Γ ⇒ C. In the second case, ⊥ is granted by O, so the dialogue sequent of the P-node succeeding the root is ⊥Γ ⊢ C; the corresponding sequent is an LI′ axiom. Note that the only way that O's initial attack involve asserting a formula opposed to a symbolic attack is the case where C is an implication. If C is not an implication, then O's assertion will be a symbolic attack (?, ?_L or ?_R), which means that the set of granted formulas remains unchanged.

4 For d > 1 we have to distinguish cases according to the form of the active formula that is defended or the (compound) formula that is attacked by P.

Recall that we are showing that for all P-nodes of the winning strategy τ for Γ ⊢ C, that there is an LI′-deduction of the corresponding sequent Γ ⇒ C. Question: since P-nodes correspond to stages in the game where P is to make the next move, why does Fermüller speak in the past tense about formulas that are attacked or defended by P? Answer: we have been sloppy about what, exactly, we are proving by induction. Our induction predicate at this point P seems to be:

P[d] : for every P-node a of τ of depth d, there exists an LI′-deduction of the sequent corresponding to the dialogue sequent for a,

and we are proving

for all natural numbers d, we have that P[d],

where the winning strategy τ is a parameter (free variable). This way of viewing what we're proving by induction coheres with what was earlier called the “base case”. What we're doing is looking at (a) P-node(s) deep in the tree and showing how to construct LI′-deductions at the P-node immediately above it (them). Assuming, then, that d > 1, we are looking at a P-node at the bottom of either of the two figures below, in which filled circles are P-nodes and open circles are O-nodes:

P-node after a node where O had a unique response ● ↓ ○ ↓ ●

P-nodes after a node where O had two possible responses ● ↓ ○ ↙ ↘ ● ●

When Fermüller talks about “the active formula that is defended or the (compound) formula that is attacked by P”, he's talking about the P-nodes at the top of these figures, not the P-nodes at the bottom.

5 To keep the proof concise, we will only elaborate it for the implicational fragment of the language; it is straightforward to augment the proof to cover also conjunctions and disjunctions.

We'll consider the connetives ∧, and ∨ later; for now, let's just stick with Fermüller and focus on implications.

6 1. P defends A→B.

Again, we are considering the P-nodes at the top of the figures above. Note that we do not consider the case where P defends an atom; that's ruled out by the Atom rule.

7 Let A,Π ⊢ A→B be the dialogue sequent at the current P-node. P moves from the P-node to the O^α-node by stating B.

By “the current P-node” Fermüller means the P-node(s) at the bottom of the figures above; our task is to show how to construct a LI′-deduction for the P-node at the top of the figure, given LI′-deductions em at the bottom. Why justifies us in saying that the sequent assigned to the current top P-node is A,Π ⊢ A→B? Notice that since we're assuming that P defended A→B, we know that O must attack what was just asserted. (This follows by the E rule.) Thus, A is granted, and we can legitimately say that the dialogue sequent at the bottom P-node is A,Π ⊢ A→B. (We don't need to bother with what “O^α-node” means.) (Actually, at this point I have to admit I'm bothered by the assertion that this is what P must be up to. Isn't it possible, in τ, that P attacks some granted formula? Again, I feel that there's something about the use of granted formulas that I'm missing.) Next up: continuing the proof. We shall see that there are some curious steps afoot here, and some additional background work is required for a fully fleshed-out proof…

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 ∅ ⊢ p→p.

Move	Player	Statement	Stance	Reference	State	Notes
					∅ ⊢ p→p	1
0	O	p	Attack	—	p ⊢ p→p	2
1	P	p	Defend	0	p ⊢ p	3
2	O	p	Attack	1	p,p ⊢ p	4

Notes:

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 p→p would go à la Felscher:

Example 1′: Felscher-style dialogue for p→p

Move	Player	Statement	Stance	Reference
0	P	p→p	—	—
1	O	p	Attack	0
2	P	p	Defend	1

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 p ⊢ p

Move	Player	Statement	Stance	Reference	State	Notes
					p ⊢ p	1
0	O	p	Attack	—	p,p ⊢ p	2

Notes:

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 p∧p ⊢ p

Move	Player	Statement	Stance	Reference	State	Notes
					p∧p ⊢ p	1
0	O	?	Attack	—	p,p∧p ⊢ p	2
1	P	?L	Attack	p∧p	p,p∧p ⊢ p	3
2	O	p	Defend	1	p,p,p∧p ⊢ p	4

Notes:

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 p ⊢ p and the game for p∧p ⊢ p, nor between p∧p ⊢ p and, say, p∧(p∨q) ⊢ p. Surely the game has to proceed by analyzing the initially granted formula p∧p.
   • 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 p∧p (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 p∧p ⊢ p 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 p∧p 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 ∅ ⊢ ¬(p∨q)→(¬p∧¬q)

Move	Player	Statement	Stance	Reference	State	Notes
					∅ ⊢ ¬(p∨q)→(¬p∧¬q)	1
0	O	¬(p∨q)	Attack	—	¬(p∨q) ⊢ ¬(p∨q)→(¬p∧¬q)	2
1	P	¬p∧¬q	Defend	0	¬(p∨q) ⊢ ¬p∧¬q	3
2	O	?L	Attack	1	¬(p∨q),¬p ⊢ ¬p∧¬q	4
3	P	¬p	Defend	2	¬(p∨q) ⊢ ¬p	5
4	O	p	Attack	3	p,¬(p∨q) ⊢ ¬p	6
5	P	p∨q	Attack	0	p,¬(p∨q) ⊢ ¬p	7
6	O	?	Attack	5	p,¬(p∨q) ⊢ ¬p	8
7	P	p	Defend	6	p,¬(p∨q) ⊢ p	9
8	O	p	Attack	7	p, p,¬(p∨q) ⊢ p	10

Notes:

1. Initial state.
2. O grants ¬(p∨q). 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 “¬(p∨q)” is actually (p∨q)→⊥). 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 ¬(p∨q)→(¬p∧¬q)

Move	Player	Statement	Stance	Reference
0	P	¬(p∨q)→(¬p∧¬q)	—	—
1	0	¬(p∨q)	Attack	0
2	P	¬p∧¬q	Attack	1
3	O	?L	Attack	2
4	P	¬p	Defend	3
5	O	p	Attack	4
6	P	p∨q	Attack	1
7	O	?	Attack	6
8	P	p	Defend	7

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

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.

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

to

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.

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.

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 q∧q for p we get (q∧q)→¬¬(q∧q), 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!

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.

N goes to India

Jesse and I will be traveling to the 4th Indian Conference on Logic and its Applications to present our paper "A curious dialogical logic and its composition problem".

Returning to assumptions

In an earlier post I discussed how to handle reasoning from assumptions in the dialogic framework. My first proposal was: Reasoning from Assumptions Attempt #1 (Naive): Fix a set of formulas Γ. Γ\vDashφ iff P has a winning strategy for φ when he is allowed to assert any ψ\inΓ, either as an attack or as a defense. I quickly realized that this was not acceptable, since it doesn't work to capture reasoning from implication in CL; take the consequence (p&q)\vDash(p&q): If P asserts the right-hand side, then the material on the left won't help him at all when O attacks (p&q). This lead to: Reasoning from Assumptions (Naive) Attempt #2: Γ\vDashφ iff P has a winning strategy for φ when he is allowed to attack any &psi&\inΓ and to defend with anything in Γ. Now, if we think that any formula is a consequence of its own assumption in N (which may or may not be a reasonable thought), then this approach doesn't work since it fails to make (pVq)\vDash(pVq); if P asserts pVq (the right-hand side), and O attacks it, then if P counterattacks by attacking pVq (the left-hand side), this allows O to defend, and the dialogue will never end. This is only a problem if we think that this consequence should be valid in N. Assuming we do, let's get a bit more creative: Reasoning from Assumptions Attempt #3: Let a(Γ) be the set of atoms which are subformulas of elements of Γ. Then Γ\vDashφ iff P has a winning strategy for φ when he is allowed to assert anything in a(Γ) whenever he wants. This fails because then (pVq)\vDash(p&q). We should also consider: Reasoning from Assumptions #4 (Jesse's proposal): Γ\vDashφ iff there is Γ'\subseteqΓ and \vDash\bigwedge Γ'\rightarrow φ. I dislike this suggestion because it builds in the validity of the deduction theorem, which begs the question against the possibility of reasoning from assumptions in N. I haven't come up with any other candidates yet.

News and events

We have had two short papers accepted to the 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Yogyakarta, Indonesia, October 10-15, 2010:

• Jesse Alama & Sara L. Uckelman, "Playing Lorenzen dialogue games on the Web".
• Jesse Alama & Sara L. Uckelman, "Proof rules for the dialogical logic N".

Both Jesse and I will be giving talks on our recent work at the Workshop on Dialogues, Inference, and Proof - Logical and Empirical Perspectives, Vienna, Austria, November 26-28, 2010. There are also plans in the work for a follow-up workshop in Tübingen, tentatively scheduled for February 25-27, 2011. When details are finalized, they will be announced here among other places.

Dialogical logic and abstract argumentation frameworks

Two weeks ago I was back in Lisbon for ECAI, and after having attended quite a few talks, tutorials, and workshops on dialogues and argumentation. This has caused me to start thinking about some alternative approaches to dialogical logic, which may or may not turn out to be fruitful in the long run, and I started writing up a blogpost about them. However, I got sidetracked and didn't finish the post until now. Argumentation frameworks (AFs) were introduced in Dung 1995. In their most basic form, an argumentation framework is a pair $\langle X,R\rangle$, where X is a set of arguments and R is a binary relation on X called an attack relation, specifying which arguments are attacks on other arguments. Both the arguments and the attack relation are considered atomic/basic; in an AF, there is no further structure to either, they are just given. AFs have been extended in various ways; one such way is by allowing arguments to attack not just other arguments but also the attack relations themselves. AFs with this functionality are called Extend Argumentation Frameworks. One can think of an attack on an attack relation as a defense against that attack. The notion of attacks and defense in the AF and EAFs parallels, at least superficially, the notion of attack and defense in dialogical logic, so the natural question that arises is whether EAFs could be used to model dialogical logic, and, if so, whether this would give us any new insights. To be more precise: For a given formula $\phi$ we can construct a directed graph $D_\phi$ where the nodes of $D_\phi$ are the subformulae of $\phi$ along with the symbolic attacks ?L, ?R, and ?, and there is an edge from node $x$ to node $x'$ if $x$ is an attack of $x'$, according to the set of particle rules in place. We can then extend this graph to one with edges between nodes and other edges, where there is an edge between node $x$ and edge $e$ iff $x$ is a defense of the attack represented by $e$. Once we've represented a dialogical formula this way, we need to answer the following questions to determine whether this representation is helpful or not: - Such a representation does not keep track of either the player making the move or the round in which it occurs. Do we need to add this information? - Does representing a dialogue in this way differ at all from the tree representation of winning strategies given by Felscher? - Are there properties of these graphs that are worth exploiting; that is, are there any correspondents between properties of the graph and the existence of a winning strategy for P? - If we do introduce labels for players and rounds, then how do we represent the structural rules in terms of constraints on the graphs? For example, D10 would say that for any propositional letter, the label for P must be larger than the label for O. Put this way, it makes me think that if we build in player and round information into the labeling of the edges, we're going to end up with something that is just isomorphic to Felscher's trees, and hence this will not provide us with any new insights. - Even so, it would be interesting to ask if all the (known) structural rules can be expressed as constraints on the labeling. References:

• Dung, P. M. 1995. "On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and $n$-person games", Artificial Intelligence 77: 321--357.
• Modgil, S. 2009. "Reasoning about preferences in argumentation frameworks", Artificial Intelligence 173, nos. 9/10: 901-934.