Monday, December 13, 2010
Reasoning from assumptions
Sunday, November 28, 2010
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 subclassical. 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.)
Tuesday, November 16, 2010
Searching for wins as a constraint satisfaction problem I: Ruminations on a constraint language
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 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).
 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 firstorder way using our constraint variables thus:
PLAYER = P ∧ atomic(STATEMENT) → [ ∃k (k < ⟨TURN⟩ ∧ playerat(k) = O ∧ statementat(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. playerat is a function of natural numbers; given k, it gives the player who played at turn k. statementat 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
That is, we make a big disjunction and compute playerat and statementat 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.PLAYER = P ∧ atomic(STATEMENT) → P = O ∧ statement_{0} = STATEMENT ∨ O = O ∧ statement_{1} = STATEMENT ∨ P = O ∧ statement_{2} = STATEMENT …  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.)
Friday, November 5, 2010
Some notes on C. Fermüller's “Parallel dialogue games and hypersequents for intermediate logics” IV: Some worries about the proof of Theorem 1
For every winning (Ei)strategy for Γ ⊢ C there exists an LI′deduction of Γ ⇒ CI have found two problems with the proof:
 the induction predicate is wrongly stated, and
 even with a correct induction predicate, the proof suffers from a gap; the gap may be fixable, or it may illustrate a genuine error.
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 Eiwinning strategies τ for Γ ⊢ C having depth d: for every Pnode 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 Eiwinning strategies τ for Γ ⊢ τ:
if τ has depth d, then for every Pnode 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 Eiwinning 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 Eiwinning strategy consisting of a single node, the root, and no other nodes; this can be proved to be impossible, by the definitions of Eigames, what it means for P to win an Eidialogue, and Eiwinning 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 “stepbystep” 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 “stepbystep” 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 Eiwinning strategy τ for Γ ⊢ C having depth d, that for every Pnode of τ there exists an LI′deduction of the sequent corresponding to the dialogue sequent at the Pnode, assuming that this is true for all d′ < d.
Given Γ, C, τ, and d, then, we have to show that every Pnode 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 Pnode (or nodes) immediately below u.
But this makes sense only if we can construe the tree (or trees) built from the Onode (or nodes) immediately below u as themselves being Eiwinning strategies. And I don't see how that can be done.
Consider the following Eigame for the Wformula (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 Eidialogue for the Wformula 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 Eiwinning strategy for the Wformula. Question: if we really cut just delete nodes from an Eiwinning strategy and get another Eiwinning 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 Eidialogue for the Wformula 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 righthand 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 Eidialogue for the Wformula 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 Wformula, considered as a branch of an Eiwinning 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 Eiwinning strategies from parts of Eiwinning strategies in the paper. Quantifying over winning strategies must not be what was intended.
 Second formulation. Recall that in this formulation, the Eiwinning 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 Pnodes 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.
To illustrate my concern, turn to the earlier Eidialogue for the Wformula. 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 Wformula itself. Folowing Fermüler's proof, O has a unique response, and we return to a Pnode. 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 Pnode of τ. That's clearly not available here, in the case of the Wformula.
Moreover, note a mismatch between how Fermüller sets up his case (a) and what we see in the dialogue for the
Wformula: the dialogue sequent at the Pnode 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 Pnode is p, because that is what O most recently attacked. Some possible responses:
 What I think is an Eidialogue isn't actually an Eidialogue.
But it looks like an Eidialogue to me. I think I understand Eigames, 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 implicationonly 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.
 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 Eiwinning strategy τ for Γ ⊢ C having depth d, that for every Pnode of τ there exists an LI′deduction of the sequent corresponding to the dialogue sequent at the Pnode, assuming that this is true for all d′ < d.
Thursday, November 4, 2010
Breaking: counterexample to a simple proposal for characterizing the logic LQ of excluded middle
P can assert an atom p only if O has already asserted pto
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…
Wednesday, November 3, 2010
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
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′: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 Pnode of τ there is an LI′proof of the sequent corresponding to the dialogue sequent at this node.Recall that for Fermüller Pnodes 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 Onode, since, by the Start rule, O begins the dialogue. Since P wins a Fermüllerstyle game when O makes a “losing” move, the leaves of a winning strategy—which correspond to wins for P—are all Pnodes: 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 everyPnode 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 Pnode(s) immediately succeeding the root is (are) identical to Γ ⊢ C. In the case where C = A→B, the Pnode 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 Pnode 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:
Notes:Move Player Statement Stance Reference State Notes Γ ⊢ C 1 0 O ? Attack — Γ ⊢ C 2 ⋮ 3  Initial state. C is atomic.
 Nothing further is conceded by O, since “?” isn't a formula.
 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 Felscherstyle 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.
 If C is a disjunction A∨B, then the game proceeds thus:
Notes:Move Player Statement Stance Reference State Notes Γ ⊢ A∨B 1 0 O ? Attack — Γ ⊢ A∨B 2 ⋮ 3  Initial state.
 The multiset of granted formulas is unchanged because “?” isn't a formula.
 Unlike the previous atomic case, the game is necessarily continuable here, in one of two or possibly three ways:
 P can defend against the attack of move 0 by asserting A,
 P can defend against the attack of move 0 by asserting B, or
 if Γ contains a nonatomic formula, P can attack it.
 If C is a conjunction A∧B, then the game can open in two ways:
orMove Player Statement Stance Reference State Γ ⊢ A∧B 0 O ?_{L} 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 nonempty: P need not defend immediately against O's attack, but may attack a (nonatomic) 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 nonempty, 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 Pnodes) 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 Pnodes 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.)Move Player Statement Stance Reference State Γ ⊢ A∧B 0 O ?_{R} Attack — Γ ⊢ A∧B ⋮ 
The most interesting case is where C is an implication A→B. The dialogue begins thus:
Notes:Move Player Statement Stance Reference State Notes Γ ⊢ A→B 1 0 O A Attack — A,Γ ⊢ A→B 2 ⋮ 3  Initial state.
 A is granted. Active formula remains unchanged.
 As usual, we can't say exactly what will happen now. If Γ contains a nonatomic 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).
coffee/tea break 
3 The base case, d = 1, follows from the fact that the Pnode (or, in case of C being a conjunction, the two Pnodes) 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
 O just attacked a formula that's contained in the multiset Γ of initially granted formulas, or
 O just asserted ⊥
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 Pnodes of the winning strategy τ for Γ ⊢ C, that there is an LI′deduction of the corresponding sequent Γ ⇒ C. Question: since Pnodes 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 Pnode 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) Pnode(s) deep in the tree and showing how to construct LI′deductions at the Pnode immediately above it (them). Assuming, then, that d > 1, we are looking at a Pnode at the bottom of either of the two figures below, in which filled circles are Pnodes and open circles are Onodes:


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 Pnodes 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 Pnode. P moves from the Pnode to the O^{α}node by stating B.By “the current Pnode” Fermüller means the Pnode(s) at the bottom of the figures above; our task is to show how to construct a LI′deduction for the Pnode 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 Pnode 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 Pnode 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 fleshedout proof…
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
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 movesastransitions 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üllerstyle 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.
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 
 Initial state.
 The active formula remains unchanged from the initial state, since P hasn't asserted anything yet.
 Since there are no other formulas asserted by P at all and O must attack it, the active formula is now p.
 The granted formulas of the dialogue sequence constitute a multiset. Since p has now been asserted twice by O, we have registered that.
Move  Player  Statement  Stance  Reference 

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

p ⊢ p  1  
0  O  p  Attack  —  p,p ⊢ p  2 
 Initial state.
 p is granted and copied to the lefthand side of the dialogue sequent from the previous state.
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 
 Initial state.
 The active formula is unchanged, since P hasn't asserted anything yet. p is now granted.
 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.
 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 lefthand side of ⊢.
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 
 Initial state.
 O grants ¬(p∨q). Active formula is unchanged. (It never changes after O moves.)
 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.
 ¬p is now granted.
 The active formula is now ¬p, because P just defended. See note 3.
 p is now granted.
 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.
 The state after this move is identical to the previous two states!
 p is now the active formula because P just asserted p as a defense. See note 3.
 p has now been granted twice. Again we see a bit of redundancy in the assignment of sequents to dialogue states.
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 
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
 Language
 Felscher treats propositional and firstorder 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 nonatomic 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.
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 Felscherstyle dialogues is always empty).
Although Felscher never defines the term, we can put words into his mouth and say that he defines Pnode and Onode of a dialogue tree as nodes whose label are moves by P or O, respectively. (Felscher does say that some moves are “Psigned” and “Osigned”; the meaning is obvious.) For Fermüller, though, a Pnode in a dialogue tree is a node representing a state of the game where P is to move next (and Onodes are defined as nodes where it is O's turn to move next). I have informally understood Pnodes 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).
A simple dialogical characterization of the logic LQ of weak excluded middle?
Proponent may assert an atom p only if Opponent has already asserted pto
Proponent may assert an atom p only if Opponent has already either asserted p or asserted ¬pbut 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 Nvalidities
Theorem 3: Every Nvalid implication φ>ψ satisfies one of the following three conditions:Last week I spent some time trying to come up with similar characterizations of validities of other types, that is, characterizations of Nvalid atoms, negations, disjunctions, and conjunctions. Three of the four are easy:
 φ is atomic.
 φ is negated.
 ψ is Nvalid.
 No atom is Nvalid [Lemma 2].
 The only Nvalid negations are double negations of validities [Theorem 4].
 A conjunct is Nvalid iff each conjunct is Nvalid [obvious].
 Either φ is Nvalid or ψ is Nvalid.
 Neither disjunct is Nvalid, and neither contains any implication.
 Neither disjunct is Nvalid, but at least one contains an implication.
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?
for all substitutions f (i.e., functions from atoms to formulas) and for all formulas φ: if φ is Nvalid then f(φ) is Nvalid.For example, the formula p→¬¬p is Nvalid, but if we plug in q∧q for p we get (q∧q)→¬¬(q∧q), which turns out to be Ninvalid. 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
 substituting Nvalidities for atoms,
 Is N′ consistent? (We can vary the notion of consistency here, thereby precisifying the question.)
 Does N′ have a suitably straightforward dialogical characterization?
Thursday, October 14, 2010
Live, from Indonesia
Tuesday, September 28, 2010
N goes to India
Tuesday, September 14, 2010
Returning to assumptions
Wednesday, September 8, 2010
News and events
 Jesse Alama & Sara L. Uckelman, "Playing Lorenzen dialogue games on the Web".
 Jesse Alama & Sara L. Uckelman, "Proof rules for the dialogical logic N".
Monday, August 30, 2010
Dialogical logic and abstract argumentation frameworks
 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: 321357.
 Modgil, S. 2009. "Reasoning about preferences in argumentation frameworks", Artificial Intelligence 173, nos. 9/10: 901934.