Dialogues as decision procedures for intuitionistic logic

Using my code for playing dialogue games, I sometimes search (often prodded by Sara) for winning strategies for concrete formulas in concrete rulesets. Sara asked me today to try, using the so-called E-dialogue rules, to find a winning strategy for a certain formula of interest. The formula has the air of being superintuitionistically valid, and it has 15 connectives, so if there were a winning strategy, it probably would not be discovered without developing the tree to a pretty significant depth. In fact, for the formula that Sara asked about (the implication whose antecedent is the law of weak excluded middle and whose consequent is Scott's formula), a winning strategy (using the E rules) was discovered only at depth 13. She then wondered about the converse of this formula, and I set about developing the game tree to depth 11…12…13…14…with no success. We expect that the formula is actually intuitionistically invalid. My program can reveal that in only one way: by showing that the dialogue tree developed down to a certain depth is such that:

1. every leaf node is expanded (i.e., we considered extending the game at that point, but no moves could be made—we did everything we could within the depth limits), and
2. it is not the case that Proponent can win no matter what Opponent does

Sometimes, for simple formulas, one can develop the dialogue tree in such a way that we can recognize the invalidity in this way (my program returns NIL as the value for the WINNING-STRATEGY function). But such formulas seem to be the exception rather than the rule, at least for the kinds of formulas that interest Sara and me these days. What is more typical is that my exhaustive enumeration program simply fails to decide, at some finite depth, that the formula is invalid. I've coded things so that the program returns the Common Lisp keyword :DIALOGUE-TREE-TOO-SHALLOW, to indicate that the dialogue tree, developed to a certain depth, fails to satisfiy one of the aforementioned pair of conditions. This leads me to wonder about how dialogues could be used as decision procedures for propositonal intuitionistic logic. We know that propositional intuititionistic logic is decidable; in fact, its validity problem is PSPACE-complete. This suggests a tantalizing problem about E-dialogues, which are supposed to capture intuitionistic validity:

Main Problem: Find a decision procedure that operates on dialogue trees that, given a propositional formula φ, determine whether φ is intuitionistically valid.

The intention behind the qualifier “that operates on dialogue trees” is to rule out, as a solution to the problem, some decision procedure that takes φ totally ignores dialogue games by running some already available decision procedure, and then says YES or NO depending on the outcome of that decision procedure. Here are some related problems:

Side Problem 1: Find a computable function f such that, for all propositional formulas φ, Proponent has a winning strategy for φ iff Proponent has a winning strategy for φ of depth < f(φ).

That is, find a computable bound on the depth to which the dialogue tree needs to be developed so that we can determine whether Proponent has a winning strategy. It's quite possible that Side Problem 1 has no solution, even though the Main Problem is solvable. Here's another approach:

Side Problem 2: Find a computable predicate P of sequences s of dialogue moves (partial dialogues) for which P(s) holds iff Proponent cannot win in any continuation of s.

This is unsatisfying, because it's basically just a recapitulation of the Main Problem. But the aim of Side Problem 2 is to search for sound heuristics for when we can cut off the search for extensions to a dialogue. What's puzzling is that, on the one hand, presumably there is a solution to the Main Problem (though possibly not through Side Problem 1 or Side Problem 2), but, on the other hand, even with the experience Sara and I have developed through grinding out one dialogue game after the next, there is little intuition for how to solve it. (We are now exploring a “no repetition” heuristic, but we first need to give a proof that it is sound.) Could it be that, even though E-dialogues are supposed to be about intuitionistic validity, their computational properties are quite different from those of other formalisms for intuitionistic logic? Either possibility—yes or no—would be an important result about dialogues. (Note that the Main Problem here is methodologically similar to the composition problem that spurred us in the first place. As before, we seek a direct solution, involving only dialogue trees; we prefer to abstain from bringing in “foreign” methods to solve our problem. The point of this methodological insistence is not to dismiss the relations between dialogical logic and other logics; rather, the aim is to take dialogical logic seriously, at face value; it is trying to honor the idea that dialogues are supposed to be autonomous way of doing logic. If we cannot answer basic logical questions about dialogues without bringing some kind of translation into another framework, or if dialogues have logical features that, in light of their motivation, are curiosities, then this needs to be made clear.)