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.
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′:
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,Γ ⇒
A→
B is provable in
LI′ iff Γ ⇒
A→
B 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′ ⊢ Γ ⇒
A→
B, then, by weakening,
LI′ ⊢
A,Γ ⇒
A →
B (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,Γ ⇒
A→
B, then
LI′ ⊢ Γ
A→(
A→
B). By soundness, Γ ⊢
A→(
A→
B) is an intuitionistically valid sequent. So is Γ ⇒ [
A→(
A→
B)]→(
A→
B), so Γ ⇒
A→
B is intuitionistically valid (modus ponens), whence, by completeness,
LI′ ⊢ Γ ⇒
A→
B.
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 = A→B, the P-node 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 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:
| Move | Player | Statement | Stance | Reference | State | Notes |
|---|
| | | | | Γ ⊢ C | 1 |
| 0 | O | ? | Attack | — | Γ ⊢ C | 2 |
| ⋮ | 3 |
Notes:
- 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 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 A∨B, then the game proceeds thus:
| Move | Player | Statement | Stance | Reference | State | Notes |
|---|
| | | | | Γ ⊢ A∨B | 1 |
| 0 | O | ? | Attack | — | Γ ⊢ A∨B | 2 |
| ⋮ | 3 |
Notes:
- 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 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 A∧B, then the game can open in two ways:
| Move | Player | Statement | Stance | Reference | State |
|---|
| | | | | Γ ⊢ A∧B |
| 0 | O | ?L | Attack | — | Γ ⊢ A∧B |
| ⋮ |
or
| Move | Player | Statement | Stance | Reference | State |
|---|
| | | | | Γ ⊢ A∧B |
| 0 | O | ?R | 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 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 A→B. The dialogue begins thus:
| Move | Player | Statement | Stance | Reference | State | Notes |
|---|
| | | | | Γ ⊢ A→B | 1 |
| 0 | O | A | Attack | — | A,Γ ⊢ A→B | 2 |
| ⋮ | 3 |
Notes:
- Initial state.
- A is granted. Active formula remains unchanged.
- 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,Γ ⊢ A→B. Notice that we are precisely in the situation where Proposition 1 helps us: we want a LI′-deduction of Γ ⊢ A→B, but what we have, by (*), is an LI′-deduction of A,Γ ⊢ A→B. Proposition 1 saves us by ensuring the existence of an LI′-deduction of Γ ⊢ A→B, so (**) follows, as desired.
So much for the sufficiency of the proposed method for proving our theorem. Ready to continue?
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
- O just attacked a formula that's contained in the multiset Γ of initially granted formulas, or
- 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 A→B.
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,Π ⊢ A→B 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,Π ⊢
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
P-node 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 fleshed-out proof…
