PrefaceFermü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′:
Theorem 1Here'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
- 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.
- 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
- 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.
- 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 ⋮
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.)
Move Player Statement Stance Reference State Γ ⊢ A∧B 0 O ?R Attack — Γ ⊢ A∧B ⋮
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
- 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).
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 ⊥
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:
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…