two more conjectures

The first one is wholly my own, and this one I have a lot less data to base it on than others, and I can't even really say why I think it might be true. However, it's something for me to spend some time (using the nifty new "search for a strategy (interactively)" functionality, which I am loving) investigating, and it doesn't seem prima facie false:

Conjecture: Let s be a winning E-strategy for phi. Extend s to s' by augmenting the tree wherever required so that the result is a winning D-strategy. Claim: The E-violating moves will occur after P has asserted an atom.

Check back often for evidence for or against this conjecture.

The second one is one that Chris proposed, namely whether D10+D12+D13=CL (i.e., we drop E, but add D12). Now, you might recall from a week or two ago that I conjectured that D10+D12+D13=IL, not CL (and I already have an easy proof that D10+D11+D13=IL), so it will be interesting to see how this pans out.

Proof of BC #2

Proving the second bold conjecture from yesterday turned out to be straightforward:

Let s be a winning D-strategy for \phi, and b a branch in s where E is violated. Let b' be the result of truncating b immediately before the first violation of E (so that the new leaf of b' is a P node). Let s' be the result of doing this for every branch b where E is violated. Claim: s' is a winning E-strategy.

• s' is an E-strategy: All moves which violate E have been removed. All other rules are unaffected by truncation:
  • D10: If P has asserted an atom p in round n of b', then he asserted it at round n of b, and since b followed D10, O's assertion of occurred at some earlier round m. Since m < n, O's assertion of p is in b', so D10 is respected.
  • D11, D12, D13: Straightforward.
• s' is a winning E-strategy. Suppose b' in s' is such that P has not won. Either:
  1. The leaf of b' is a move by O, or
  2. The leaf of b' is a move by P, but there is a legal continuation of the branch according to E.
  (1) is not possible, by construction of s'. (2)Suppose that at the leaf (let it be round n) O has a legal move. Any move that is legal under E is also legal under D, which means that this move already appeared in s, in some branch b* which diverged from b at round n:

  b		round n (P's move)		b*
  	/		\
  round n+1: E-violating move by O				round n+1: E-non-violating move by O

  Since b' is in s', we know that b* was not truncated before round n. Hence, the result of cutting b off at round n+1 looks like this:

  round n (P's move)

  |

  round n+1: E-non-violating move by O

  And hence, contra assumption, n is not a leaf in b'.

QED

When P must repeat a move

In his previous post, Jesse said that we'd speculated that the heuristic where P never repeats a move could be added to either D or E without any consequence (other than cutting down the search space). We'd thought this for quite some time but yesterday afternoon found various counterexamples, of which the simplest is the double negation of excluded middle: Here, P is required to repeat his attack on the negation in order for force P to attack the disjunction, so that he can go back and redefend it. (In a sense, this mimics the behavior you get when you drop D12, and allow repeat defenses to be. It's just that in this case, by allowing P to repeat his attack, he doesn't repeat his defense, because the defenses are to separate attacks.) But the pattern is more general: I'm pretty sure any double-negation of a classically-valid disjunction will require P to attack the same formula twice.

New functionality on the dialogues site: interactively searching for strategies

Thanks to some prodding from Sara, I've implemented some new functionality to the dialogues site: interactively searching for strategies. As usual, one specifies an initial formula and a ruleset. The site then develops the full dialogue tree (that is, the tree that represents all possible moves consistent with the chosen ruleset) to the first Opponent node that has multiple children. One then chooses one of the children (i.e.., one chooses a move for Proponent). The site then continues to develop the dialogue tree, ignoring the unselected children of that Opponent node, until it encounters another Opponent node that has multiple children. One again makes a choice, and so forth. This process ends either when one finds that the choices that one has made for Proponent amount to a winning strategy, or when one finds that there is no winning strategy that is consistent with the choices made so far.

Some functionality is still not implemented. During the interactive search for a strategy, one makes choices about how Proponent should respond. There may not be a winning strategy consistent with those choices. If so, the website simply informs you of this, without letting you go back and choose some alternative course. Even if a winning strategy is found, the website does not permit one to choose alternative paths (thereby possibly discovering a different winning strategy). This functionality actually does exist in the interactive "command line" interface (for the brave, see PLAY-STRATEGY-SEARCH-GAME in the source), but it has not yet been translated to an HTML presentation yet.

With the site one can also now specify heuristics to tack on to a selected ruleset. Strictly speaking, there's no difference between heuristic rules and any other structural rule (in fact, heuristic rules are implemented as structural rules). Playing a game with a ruleset S and heuristic set H just means playing according to the ruleset S ∪ H.

At the moment, only one heuristic rule is presented to you: forbid Proponent from making identical moves (same move, same stance, same reference, same assertion). This can help significantly cut down the set of possibilities available to Proponent. Sara and I have conjectured that adding this heuristic rule to the D and E rulesets does not affect their logical strength: Proponent has a winning D (respectively E) strategy iff Proponent has a winning D (respectively E) winning strategy in which Proponent never repeats a move.

Proof of BC 1

I was pretty sure that I had an easy way to prove Bold Conjecture #1, and I ran it by Jesse; all I had to say was "induction + pigeonhole principle" and he essentially rattled off the rest, which was good confirmation for me that my intuition was right. I should probably still write it up in full detail, but essentially, it is this:

Proof: Assume round n is the first time where O violates E, that is, he references some round n−i such that i≠ 1. Assume further that this is the first time that round n−i has been referenced. Now, look at round (n−i)+1. What move does O reference here? If it is not n−i, then, contra assumption, round n is not the first round where E has been violated. If it is n−i, then, contra assumption, round n is not the first round where n−i is referenced. QED.

Some evidence for a bold conjecture

Sara has formulated a conjecture or two about the difference between the D and E rulesets. Sara proposed the example to Chris, who proposed looking for a counterexample with the formula

¬¬(((A → B) → C) → (((B → A) → C) → C))

This formula was put forward by Chris as a potential counterexample owing to the way that he thinks of Sara's conjecture: for Chris, Sara is claiming that one can get away without contraction in an intuitionistic sequent calculus. But we know the latter not to be the case, hence one should look at at intuitionistically valid formulas for which every sequent deduction involves contraction. Whence the formula above. It turns out that this is not yet a counterexample to Sara's claim. Here is one strategy discovered interactively for that formula (with the help of some brand new functionality of the dialogical logic software that I've been working on, which will be released soon): In this example, see various cases where the E rule is violated:

• in the left branch at move 15;
• in the middle branch also at move 15;
• in the right branch at move 9.

Each branch contains a violation of E, and there is in fact only one violation in each branch. Sara's conjecture still holds because if we were to chop off each branch the first time a violation of the E rule occurs, we obtain an E-strategy. This doesn't prove Sara's conjecture, of course, but in light of the purported significance of this formula (Chris thought it would turn out to be a counterexample) and its complexity (there are eight connectives appearing in it), this is certainly a satisfying piece of evidence in favor of the conjecture.

Bold conjectures

Because what's the point of making a conjecture if it isn't provocative? After a short but extremely fruitful with Chris and Jesse this afternoon, and bolstered up on the basis of a whole two examples that I've worked through, I have the following two bold conjectures:

• [In a D strategy] The first time that the E rule is violated, the reference of that round has already appeared as the reference of an earlier round.
• (Corollary of the first) The first time that the E rule is violated, if you chop the branch off at the previous move (i.e., P's move), the result of doing so for all branches in a winning D-strategy will be a winning E-strategy.

So: The hunt for counterexamples is on!