- 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
- it is not the case that Proponent can win no matter what Opponent does

`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:

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:Main Problem:Find a decision procedure that operates on dialogue trees that, given a propositional formula φ, determine whether φ is intuitionistically valid.

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 1:Find a computable functionfsuch that, for all propositional formulas φ, Proponent has a winning strategy for φ iff Proponent has a winning strategy for φ of depth <f(φ).

This is unsatisfying, because it's basically just a recapitulation of the Main Problem. But the aim of Side Problem 2 is to search forSide Problem 2:Find a computable predicatePof sequencessof dialogue moves (partial dialogues) for whichP(s) holds iff Proponent cannot win in any continuation ofs.

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

## No comments:

## Post a Comment