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.

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.

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.

Handling assumptions

I still have a half-written blog post from when I was in Lisbon last week, but I think it will have to wait, as now I'm thinking about something else, namely, how to handle assumptions in dialogical logic. While preparing a short note on the sound proof rules of N, I noticed that none of them have anything on the left-hand side of the turnstile; that is, none of the rules model anything like reasoning from assumptions. At this point, I have no idea if this is something specific to N, because we don't know enough about N, and how much of this is specific to the dialogical approach, which doesn't, on the face of it, allow for any type of reasoning from assumptions. Now what about IL and CL? They have dialogical characterizations and allow reasoning from assumptions, both in their ordinary semantics and in their proof theory. So why is it that they can be dialogically characterized, if ordinary structural/particle rules don't allow for assumptions? My suspicion is that it's because both logics satisfy a deduction theorem -- $\Gamma\vdash\phi$ iff $\vdash\Gamma\rightarrow\phi$, and hence you can "do away" with assumptions. Now, the fact that the proof rule from $\vdash\phi\rightarrow\psi$ infer $\vdash(\gamma\rightarrow\phi)\rightarrow(\gamma\rightarrow\psi)$ is not sound in N shows that N cannot have an ordinary deduction theorem, and so it is important to find a way to handle reasoning from assumptions in N in a dialogical way. Here is a naive approach, which I will ask Jesse to implement so I can test it via the website: - Fix a set of formulas $\Gamma$ such that Proponent can assert $\phi\in\Gamma$ at any time, as either an attack or as a defense. Essentially then $\Gamma\vDash\psi$ says "if you (Opponent) grant me (Proponent) the info in $\Gamma$, I can prove $\psi$ to you. Being that this is a naive approach, I do not know how well it will work. Luckily, since we know how reasoning from assumptions should work in IL and CL, we can use them as test cases for this approach.