Farewell to dialogues

Today, my contract to work on the ESF DiFoS project ends, and this marks my last post on this blog. It's been an interesting few years with some discoveries and results that I never expected. One thing I regret is that the original question that Jesse and I first bonded over is one that we never ended up having a chance to work on, namely whether there is a constructive way to move from the classical dialogical proof of a double-negation translation of a formula to the intuitionistic dialogical proof of the base formula. I still think that this is something which should be possible, and would be very interesting to investigate. Alas, it must be left to someone else to pursue, since I've now got other things on my plate, and must leave dialogues behind.

Summary of the trip

Tomorrow I leave Vienna and head back to Amsterdam, and thus I thought it would be useful to put a brief recap of the important results of the last month:

• Jesse and I finished up our extended paper on N, "A Curious Dialogical Logic and Its Composition Problem", and sent it off.
• Significant new features have been added to the dialogues website, including the long-awaited ability to compute strategies interactively and the possibility of selecting arbitrary rulesets (from a pre-defined set of rules).
• Our goal with Chris was to find out general conditions under which it can be proved that E is redundant; we have not gotten as far as we like, but the results of my various pokings and proddings on the subject are contained in "Some Remarks on the E rule in Dialogical Logic".

This research visit was funded by a grant from the European Science Foundation EUROCORES Short-Term Visit scheme within the framework of the ESF EUROCORES Programme entitled 'Modelling Intelligent Interaction', which we gratefully acknowledge.

Would you look at that!

OK, now this result does surprise me. I think I just found a ruleset that is not closed under modus ponens! D10+D12+D13+E:

• validates ~~φ->φ.
• validates (~~φ->φ)->(φv~&phi).
• does not validate φv~φ.

And here are my proofs to double check my work, because this is very, very strange:

In fact, the same also holds of D10+D12+D13, without E:

probably surprising to no one other than me

And I wouldn't say it's exactly surprising to me, since that seems to imply I expected the opposite, whereas I didn't have any expectations at all.

I spent a lot of yesterday testing a number of other formulas under D10+D12+D13 and D10+D12+D13+E, and I think I have another conjecture about how E works, namely, while adding E may increase the number of validities (e.g., going from N to CL), it will never decrease the number; I have not found a single formula which is valid under the non-E ruleset but invalid when E is added. There is probably an easy, straightforward explanation of this/proof that this always happens, but I haven't spend any time thinking about it yet.

Even if there is, though, it's still something interesting to point out, because it is not a general phenomenon (i.e., that increasing the number of rules in your ruleset will never decrease the set of validities), since D10+D12+D13 validates all four version of DeMorgan's, but this is not the case if you add D11, since one of the versions is not intuitionistically acceptable.

returning to the role of E

One of the original motivations our work with Chris here in Vienna started with is contexts under which we can show that E is redundant; IL is an obvious case, and hence D10+D11+D13 is as well. D10+D12+D13 was a surprising (to some) countercase. CL is an obvious countercase...or is it?

It appears that the unique redundancy of E in IL noted above is actually closely tied to Felscher's formulation of the rules. If we stray from there (keeping E: "The Opponent must immediately respond to the previous Proponent move") and start formulating rules on our own, can we perhaps come away with sets of rules where the presence or absence of E is irrelevant?

When we talked about this a few days ago, my conjecture was that it's not the immediate-response consequence of E that is so important for CL, but rather the restriction on the number of moves O can make. I propose the following:

• D10: P cannot assert an atom before O does.
• D13: A P-statement can be attacked at most once.
• D14: A P-attack can be defended at most once.

Certainly D10+D13+E implies D10+D13+D14. But D10+D13+D14 does not imply E, since it relaxes the immediate-response constraint.

So one hypothesis for how to go about constructing rules that would allow us to prove the redundancy of E in a particular ruleset is by looking at variants of the bounded rules that Krabbe proposed in his 1985 Synthese article which put constraints on the number of times O can repeat a move.

However, if you are in the context of E, what is it that separates IL from CL? It is the ability of P to go back and essentially "change his mind" about a defense, e.g., in the case of excluded middle. So here, it appears that the important distinction is not how many times O can repeat a move, but how many times P can. The case is not quite the same, though: In IL, there are contexts where P is allowed to repeat a move (same formula/symbolic attack, same stance, same reference), and in CL, it is not that we are allowing P to repeat a move that he's already made, but rather to re-refer to a move of O that he's already referred to. So the cases aren't quite parallel, but it still shows a tantalizing dimension to consider.

Teasing rules apart

Based on the chart in my previous post, the most interesting pair of candidates to look at is D10+D12+D13 and D10+D12+D13+E. I went through the first 17 predefined formulas on the dialogues site, for the following results (formulas of particular note have been highlighted in red):

Formula	D10+D12+D13	D10+D12+D13+E
Excluded middle	not valid	not valid
Peirce	not valid	valid
WEM	not valid	not valid
Cond. EM	not valid	not valid
Dummett	not valid	not valid
DNI	valid	valid
DNE	valid	valid
K	valid	valid
B	valid	valid
C	valid	valid
W	valid	valid
Scott	tried to depth 36	tried to depth 20
Smetanich	tried to depth 24	valid
DM1	valid	valid
DM2	valid	valid
DM3	valid	valid
DM4	valid	valid

The ones where I tried to a certain depth I'm pretty sure are not valid because of the existence of infinite branches. I don't have a proof of this yet.

Fill in the Blanks

Note: Rather than continuing to update this post, the results can be found in the results paper linked in this post.

	D10	D11	D12	D13	E	notes
N	X			X		AU
CL	X			X	X	AKU
not CL	X		X	X		excluded middle, Peirce not valid
not CL	X		X	X	X	validates Peirce, does not validate excluded middle
IL	X	X		X		U, blog post
IL	X	X		X	X	U, blog post
IL	X	X	X	X		Felscher
IL	X	X	X	X	X	Felscher