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: pp is valid in N, but the instance (pp)→(pp) 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.)

Tuesday, November 16, 2010

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,
  • , 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 ⟨s1,…sn⟩ 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→(qr) and (pq)∨(pr), 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’).

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

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:

Thursday, November 4, 2010

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
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 ¬pp is valid in this setting! The idea is that O asserts ¬p, then P can assert p and win the game. That ¬pp 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

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.


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,Γ ⇒ AB is provable in LI′ iff Γ ⇒ AB 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′ ⊢ Γ ⇒ AB, then, by weakening, LI′ ⊢ A,Γ ⇒ AB (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,Γ ⇒ AB, then LI′ ⊢ Γ A→(AB). By soundness, Γ ⊢ A→(AB) is an intuitionistically valid sequent. So is Γ ⇒ [A→(AB)]→(AB), so Γ ⇒ AB is intuitionistically valid (modus ponens), whence, by completeness, LI′ ⊢ Γ ⇒ AB. 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 = AB, the P-node succeeding the root carries A,Γ ⊢ AB 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:
    Γ ⊢ C1
    0O?AttackΓ ⊢ C2
    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 AB, then the game proceeds thus:
    Γ ⊢ AB1
    0O?AttackΓ ⊢ AB2
    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 AB, then the game can open in two ways:
    Γ ⊢ AB
    0O?LAttackΓ ⊢ AB
    Γ ⊢ AB
    0O?RAttackΓ ⊢ AB
    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 AB. The dialogue begins thus:
    Γ ⊢ AB1
    0OAAttackA,Γ ⊢ AB2
    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,Γ ⊢ AB. Notice that we are precisely in the situation where Proposition 1 helps us: we want a LI′-deduction of Γ ⊢ AB, but what we have, by (*), is an LI′-deduction of A,Γ ⊢ AB. Proposition 1 saves us by ensuring the existence of an LI′-deduction of Γ ⊢ AB, 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 AB.
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,Π ⊢ AB 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,Π ⊢ AB? Notice that since we're assuming that P defended AB, 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,Π ⊢ AB. (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…