Some notes on C. Fermüller's “Parallel dialogue games and hypersequents for intermediate logics” IV: Some worries about the proof of Theorem 1

In a previous post I suggested that there's something wrong with Fermüller's proof of Theorem 1:

For every winning (Ei-)strategy for Γ ⊢ C there exists an LI′-deduction of Γ ⇒ C

I have found two problems with the proof:

1. the induction predicate is wrongly stated, and
2. even with a correct induction predicate, the proof suffers from a gap; the gap may be fixable, or it may illustrate a genuine error.

This post explains the problems, as I see them.

Problem 1. The induction predicate is wrongly stated.

The actual statement being proved is, so far as I can see,

for all multisets Γ, all formulas C, and for all Ei-winning strategies τ for Γ ⊢ C having depth d: for every P-node of τ there is an LI′-deduction of the sequent corresponding to the dialogue sequent at the node.

Another possibility: for all multisets Γ, all formulas C, and for all Ei-winning strategies τ for Γ ⊢ τ:

if τ has depth d, then for every P-node of τ there is an LI′-deduction of the sequent corresponding to the dialogue sequent at the node.

In this second formulation, τ is a parameter of the statement to be proved by induction. The first formulation quantifies over Ei-winning strategies (and multisets and formulas). The proof is by strong induction on d. The proof goes by checking the “base case” where d = 1, and then checking the “inductive step” where d > 1. There are three problems here; the first two are essentially stylistic and easily remedied, but the third is more difficult:

• What about the case d = 0?

  The case of d = 0 amounts to considering the possibility of an Ei-winning strategy consisting of a single node, the root, and no other nodes; this can be proved to be impossible, by the definitions of Ei-games, what it means for P to win an Ei-dialogue, and Ei-winning strategy. So the induction predicate holds vacuously.

  So there's nothing really wrong with ignoring the case of d = 0, but the justification for ignoring it does rely on a little lemma.

• Judging from the statement of the “inductive step”, the proof is by strong induction; so why is the case of d = 1 singled out as the “base case”?

  The ordinary structure of a proof by strong induction, with an induction predicate A is to show ∀nA[n] by proving:

  ∀ k ((∀ j (j < k → A[j]) → A[k])

  In a proof by strong induction there is no “base base” as there is in a proof by vanilla induction of ∀ nA[n], where the task is to prove the conjunction:

  A[0] ∧ ∀ k (A[k] → A[k+1])

  In a proof by strong induction the sole proof obligation ∀ k ((∀ j (j < k → A[j]) → A[k]) is, I suppose, the “inductive step”. The proof now goes as follows. Let k be a natural number. There are three cases:

  • k = 0. We have already discussed that A[0] holds vacuously, so (∀ j (j < 0 → A[j]) → A[0] is true.
  • k = 1. Fermüller satisfactorily deals with this case (but note that we can actually prove A[1] outright; we don't need the help of (∀ j (j < 1 → A[j]), which in any case is useless since A[0] holds vacuously).
  • k > 1. The hypothesis (∀ j (j < k → A[j]) evidently is used in to dispose of this case. (But see below!)

  So a minor reformulation of the argument rescues the proof. It is not a proof by vanilla “step-by-step” inductuion, but a proof by strong induction. There is no “base case” exactly analogous to the proob obligation A[0] in a proof by vanilla “step-by-step” induction, but the same proof obligation does arise as a bona fide case in a proof by cases (which proof by induction, strong or weak, manifestly is not).

  There's nothing deep here, but I thought I'd mention it because things like this do catch my eye as sources of potential trouble.

• Can this proof by induction succeed at all?

  I don't think so; neither of the induction predicates I've stated above is suited to the task.

  • First formulation. Recall that this formulation quantifies over winning strategies. Our task is to prove, in the case where d > 0, that, for every multiset Γ of formulas and every formula C, and for every Ei-winning strategy τ for Γ ⊢ C having depth d, that for every P-node of τ there exists an LI′-deduction of the sequent corresponding to the dialogue sequent at the P-node, assuming that this is true for all d′ < d.

    Given Γ, C, τ, and d, then, we have to show that every P-node u of τ has the desired property. Fermüller distinguishes between the stance—attack or defend—that P will take when moving from u to its successor. In either case, Fermüller claims that the induction hypothesis allows us to conclude that there exist suitable LI′-deductions for the P-node (or nodes) immediately below u.

    But this makes sense only if we can construe the tree (or trees) built from the O-node (or nodes) immediately below u as themselves being Ei-winning strategies. And I don't see how that can be done.

    Consider the following Ei-game for the W-formula (p→(p→q))→(p→q). P wins (which is unsurprising, since this is the principle type for the typeable term λxy.xyy in the simply typed λ-calculus):

    An Ei-dialogue for the W-formula

    Move	Player	Statement	Stance	Reference	State
    					⊢ (p→(p→q))→(p→q)
    0	O	p→(p→q)	Attack	—	p→(p→q) ⊢ (p→(p→q))→(p→q)
    1	P	p	Attack	0	p→(p→q) ⊢ (p→(p→q))→(p→q)
    2	O	?	Attack	1	p→(p→q) ⊢ p
    3	P	p→q	Defend	1	p→(p→q) ⊢ p
    4	O	p	Attack	3	p,p→(p→q) ⊢ p→q

    Consider this dialogue as a branch of an Ei-winning strategy for the W-formula. Question: if we really cut just delete nodes from an Ei-winning strategy and get another Ei-winning strtagy (for a different initial dialoguq sequent), what happens when we chop off the top two nodes? Naively, we get this:

    Naive truncation of an Ei-dialogue for the W-formula

    Move	Player	Statement	Stance	Reference	State
    					p→(p→q) ⊢ (p→(p→q))→(p→q)
    0	O	?	Attack	—	p→(p→q) ⊢ p
    1	P	p→q	Defend	—	p→(p→q) ⊢ p
    2	O	p	Attack	1	p,p→(p→q) ⊢ p→q

    I've already adjusted the labels in the Move and Reference columns (not adjusting them truly results in nonsense). But notice that the game has become incoherent for other reasons:

    • the initial dialogue sequent is p→(p→q) ⊢ (p→(p→q))→(p→q), but O initial move in this truncated game is ?, which makes sense only if the right-hand side of the initial dialogue sequent were an atomic formula, but it is actually (p→(p→q))→(p→q). Moreover, the active formula after O's initial move should be (p→(p→q))→(p→q), not p.
    • P's move at step 1 is partly sensible (putting aside the nonsense of O's move at step 0), but the active formula of the dialogue sequent after this move is still wrong.
    • The only move that makes sense in its entirety (assuming the meaningfulness of the previous moves) is the final move at step 2 by O.

    One could complain that this naive truncation is simply too naive. Instead of copying the dialogue sequent after move 1 in the original game and making it the initial dialogue sequent of the truncated game, we should be more intelligent and note that O attacks p at move 2, so that should be the initial active formula. According to this proposal, then, the truncated branch looks like this:

    Less naive truncation of an Ei-dialogue for the W-formula

    Move	Player	Statement	Stance	Reference	State
    					p→(p→q) ⊢ p
    0	O	?	Attack	—	p→(p→q) ⊢ p
    1	P	p→q	Defend	—	p→(p→q) ⊢ p
    2	O	p	Attack	1	p,p→(p→q) ⊢ p→q

    In this more intelligent truncation of the original game, the initial move by O now makes sense in its entirety. But move 1 by P does not make sense: O just attacked an atomic formula, and P defends against that attack by asserting an implication! This violates two rules: Atom, which says that P cannot defend against attacks on atoms, and the particle rules, because only against attacks on composite formulas could a defense be given.

    If there's no way of truncating the original game for the W-formula, considered as a branch of an Ei-winning strategy, then I see no way how this the first formulation of the induction predicate can be rescued. Certainly there's no discussion of producing Ei-winning strategies from parts of Ei-winning strategies in the paper. Quantifying over winning strategies must not be what was intended.

  • Second formulation. Recall that in this formulation, the Ei-winning strategy τ appears as a parameter.

    This understanding of the induction predicate can be dispensed with quite quickly: the assumption that the induction predicate holds for all d′ < d is useless in showing that if τ has depth d, then for all P-nodes of τ…, since if τ has depth d then it can't any other depth d′.

  Problem 2. Even if the induction predicate is correctly stated, the proof may still be erroneous.

  The discussion of Problem 1 is, to some extent, dispensible, because in a previous post I articulated what I take to be the actual induction principle at work in the proof of Theorem 1. I wanted to take some time just to make clear, though, that what is literally written in the paper is in need of rescue. However, even with the induction principle tweaked in a way that strikes me as most sensible, the proof still seems to me to be open to criticism, and possible even mistaken.

  Here's the problem: in the case where we consider trees of depth d > 1, we focus on P-nodes and distinguish between the stance—attack or defend—that P could take in his next move. Fermüller considers these cases, and how O might react. He applies the induction hypothesis at the P-node (or nodes) immediately below the current P-node to get LI′-deductions, from which he constructs a suitable LI′-deduction for the current P-node. But there is a problem here: what if the P-node (or nodes) immediately below the current P-node are leaves of τ? Another way to state my worry: are we sure that the induction predicate holds for the case d = 2?

  Another way to state my worry: are we sure we really know how to compute the winning strategies that the proof of Theorem 1 is supposed to give us?

  In his handling of what he calls the “base case”, Fermüller shows how to construct LI′-deductions for the P-node (!) of τ. But this is easy because the game has only one move in it, the “losing” move by O. How do we deal with the leaf nodes of τ in the general case?

  To illustrate my concern, turn to the earlier Ei-dialogue for the W-formula. Look at the dialogue after move 2. We are considering case (a) of Fermüller's proof, where P defends against an attack on an implication, which in this case is the whole W-formula itself. Folowing Fermüler's proof, O has a unique response, and we return to a P-node. Fermüller now says that the inductive hypothesis should give us an LI′-deduction for the sequent corresponding to the dialogue sequent at this node, which in this case is a leaf of the winning strategy τ. Now, it is clear that there is an LI′-deduction for the sequent p,p→(p→q) ⇒ p→q. But it is not an axiom of LI′.

  But if we compare how Fermüller disposes of the “base case”, we see that he assigns axioms of LI′ to the leaf P-node of τ. That's clearly not available here, in the case of the W-formula.

  Moreover, note a mismatch between how Fermüller sets up his case (a) and what we see in the dialogue for the W-formula: the dialogue sequent at the P-node in question does not match Fermüller's pattern: he says that from P's defense of an attack on an implication, we can infer that the active formula at the current node is the implication itself. This is clearly not the case here: the active formula at the current P-node is p, because that is what O most recently attacked.

  Some possible responses:

  • What I think is an Ei-dialogue isn't actually an Ei-dialogue.

    But it looks like an Ei-dialogue to me. I think I understand Ei-games, but I'm happy to accept that I'm missing something crucial.

  • I'm miscalculating the active formula.

    I don't believe I am. The active formula after O's move at step 2 is p because that is formula asserted by P that O has most recently attacked; there is no issue of a forced O attack on any other formula, since O could have defended at step 2 by defending against the attack of move 1.

  • The proof is mistaken.

    This seems quite possible to me.

    I can't account, for example, for why Fermüller thinks that, if P is about to defend, then (treating only the implication-only fragment of propositional logic for the moment) the active formula is an implication. In my example, it is an atom. P, unlike O, is not constrained to respond to the most recent assertion of the other player; in my example above, P defends against something other than the most recent statement by O.

  This proof feels out of control to me…