tag:blogger.com,1999:blog-53711324002410729882017-01-17T12:55:39.908-08:00TONIGHT: Proponent v. OpponentJesse Alamahttp://www.blogger.com/profile/18300729364134604326noreply@blogger.comBlogger54125tag:blogger.com,1999:blog-5371132400241072988.post-9749108064418498202011-12-31T05:40:00.000-08:002011-12-31T05:40:11.621-08:00Farewell to dialoguesToday, my contract to work on the <a href="http://www.esf.org/">ESF</a> <a href="http://www-ls.informatik.uni-tuebingen.de/difos/">DiFoS</a> 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.Sara L. Uckelmanhttp://www.blogger.com/profile/14716054827293611237noreply@blogger.com0tag:blogger.com,1999:blog-5371132400241072988.post-24925337213591570542011-07-05T02:48:00.000-07:002011-07-25T05:31:35.553-07:00Summary of the tripTomorrow 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:
<ul>
<li>Jesse and I finished up our extended paper on N, <a href="http://staff.science.uva.nl/~suckelma/latex/wollic2011/n-forjpl.pdf">"A Curious Dialogical Logic and Its Composition Problem"</a>, and sent it off.</li>
<li>Significant new features have been added to the <a href="http://www.dialogical-logic.info/">dialogues website</a>, including the long-awaited ability to compute strategies interactively and the possibility of selecting arbitrary rulesets (from a pre-defined set of rules).</li>
<li>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 <a href="http://staff.science.uva.nl/~suckelma/latex/erule/erule.pdf">"Some Remarks on the E rule in Dialogical Logic"</a>.</li>
</ul>
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.Sara L. Uckelmanhttp://www.blogger.com/profile/14716054827293611237noreply@blogger.com3tag:blogger.com,1999:blog-5371132400241072988.post-76595829847713471332011-07-01T04:10:00.001-07:002011-07-01T04:58:43.072-07:00Would you look at that!<p>OK, now <i>this</i> result does surprise me. I think I just found a ruleset that is not closed under modus ponens! D10+D12+D13+E:</p>
<ul>
<li>validates ~~φ->φ.</li>
<li>validates (~~φ->φ)->(φv~&phi).</li>
<li>does not validate φv~φ.</li>
</ul>
<p>And here are my proofs to double check my work, because this is <i>very, very strange</i>:</p>
<a onblur="try {parent.deselectBloggerImageGracefully();} catch(e) {}" href="http://3.bp.blogspot.com/-88qamqVyWy0/Tg2stNt_stI/AAAAAAAAAFo/idY8kRmiD8g/s1600/dne-101213e.png"><img style="display:block; margin:0px auto 10px; text-align:center;cursor:pointer; cursor:hand;width: 320px; height: 71px;" src="http://3.bp.blogspot.com/-88qamqVyWy0/Tg2stNt_stI/AAAAAAAAAFo/idY8kRmiD8g/s320/dne-101213e.png" border="0" alt=""id="BLOGGER_PHOTO_ID_5624341402432287442" /></a>
<a onblur="try {parent.deselectBloggerImageGracefully();} catch(e) {}" href="http://1.bp.blogspot.com/-d3zCZKGbQMc/Tg2s5ogzAcI/AAAAAAAAAFw/JzXmZo54G6k/s1600/dne-em-101213e.png"><img style="display:block; margin:0px auto 10px; text-align:center;cursor:pointer; cursor:hand;width: 320px; height: 89px;" src="http://1.bp.blogspot.com/-d3zCZKGbQMc/Tg2s5ogzAcI/AAAAAAAAAFw/JzXmZo54G6k/s320/dne-em-101213e.png" border="0" alt=""id="BLOGGER_PHOTO_ID_5624341615783117250" /></a>
<a onblur="try {parent.deselectBloggerImageGracefully();} catch(e) {}" href="http://2.bp.blogspot.com/-TSLYeyrutzY/Tg2tGACiYiI/AAAAAAAAAF4/tZ2fRY3FbQ8/s1600/em-101213e.png"><img style="display:block; margin:0px auto 10px; text-align:center;cursor:pointer; cursor:hand;width: 320px; height: 59px;" src="http://2.bp.blogspot.com/-TSLYeyrutzY/Tg2tGACiYiI/AAAAAAAAAF4/tZ2fRY3FbQ8/s320/em-101213e.png" border="0" alt=""id="BLOGGER_PHOTO_ID_5624341828257079842" /></a>
<p>In fact, the same also holds of D10+D12+D13, without E:</p>
<a onblur="try {parent.deselectBloggerImageGracefully();} catch(e) {}" href="http://4.bp.blogspot.com/--k0plbYOky0/Tg217rNKIGI/AAAAAAAAAGQ/JqAV5nSOogE/s1600/dne-101213.png"><img style="display:block; margin:0px auto 10px; text-align:center;cursor:pointer; cursor:hand;width: 320px; height: 69px;" src="http://4.bp.blogspot.com/--k0plbYOky0/Tg217rNKIGI/AAAAAAAAAGQ/JqAV5nSOogE/s320/dne-101213.png" border="0" alt=""id="BLOGGER_PHOTO_ID_5624351546470441058" /></a>
<a onblur="try {parent.deselectBloggerImageGracefully();} catch(e) {}" href="http://3.bp.blogspot.com/-7U1EGpmg7GE/Tg22VxUov-I/AAAAAAAAAGY/am4pTqQwA4o/s1600/dne-em-101213.png"><img style="display:block; margin:0px auto 10px; text-align:center;cursor:pointer; cursor:hand;width: 320px; height: 98px;" src="http://3.bp.blogspot.com/-7U1EGpmg7GE/Tg22VxUov-I/AAAAAAAAAGY/am4pTqQwA4o/s320/dne-em-101213.png" border="0" alt=""id="BLOGGER_PHOTO_ID_5624351994789019618" /></a>
<a onblur="try {parent.deselectBloggerImageGracefully();} catch(e) {}" href="http://1.bp.blogspot.com/-mV8H4vttPtM/Tg22aqqb2yI/AAAAAAAAAGg/Kq2m0Pa8XcU/s1600/em-101213.png"><img style="display:block; margin:0px auto 10px; text-align:center;cursor:pointer; cursor:hand;width: 320px; height: 56px;" src="http://1.bp.blogspot.com/-mV8H4vttPtM/Tg22aqqb2yI/AAAAAAAAAGg/Kq2m0Pa8XcU/s320/em-101213.png" border="0" alt=""id="BLOGGER_PHOTO_ID_5624352078900747042" /></a>Sara L. Uckelmanhttp://www.blogger.com/profile/14716054827293611237noreply@blogger.com0tag:blogger.com,1999:blog-5371132400241072988.post-3707125630323907772011-07-01T01:48:00.001-07:002011-07-01T01:53:29.844-07:00probably surprising to no one other than me<p>And I wouldn't say it's exactly surprising to <i>me</i>, since that seems to imply I expected the opposite, whereas I didn't have any expectations at all.</p>
<p>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 <i>increase</i> the number of validities (e.g., going from N to CL), it will never <i>decrease</i> 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.</p>
<p>Even if there is, though, it's still something interesting to point out, because it is <i>not</i> 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.</p>Sara L. Uckelmanhttp://www.blogger.com/profile/14716054827293611237noreply@blogger.com2tag:blogger.com,1999:blog-5371132400241072988.post-52536536441155515772011-06-30T03:09:00.001-07:002011-06-30T03:11:01.239-07:00returning to the role of E<p>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?</p>
<p>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?</p>
<p>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:</p>
<ul>
<li>D10: P cannot assert an atom before O does.</li>
<li>D13: A P-statement can be attacked at most once.</li>
<li>D14: A P-attack can be defended at most once.</li>
</ul>
<p>Certainly D10+D13+E implies D10+D13+D14. But D10+D13+D14 does not imply E, since it relaxes the immediate-response constraint.</p>
<p>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 <i>Synthese</i> article which put constraints on the number of times O can repeat a move.</p>
<p>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 <i>repeat</i> a move that he's already made, but rather to <i>re-refer</i> 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.</p>Sara L. Uckelmanhttp://www.blogger.com/profile/14716054827293611237noreply@blogger.com4tag:blogger.com,1999:blog-5371132400241072988.post-71759135128597612502011-06-28T07:21:00.001-07:002011-06-28T07:26:56.812-07:00Teasing rules apartBased on the chart in <a href="http://dialogue-games.blogspot.com/2011/06/fill-in-blanks.html">my previous post</a>, 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 <a href="http://www.dialogical-logic.info/">dialogues site</a>, for the following results (formulas of particular note have been highlighted in <span style="color: rgb(255, 0, 0);">red</span>):
<table border="1">
<tbody><tr><th>Formula</th><th>D10+D12+D13</th><th>D10+D12+D13+E</th></tr>
<tr><td>Excluded middle</td><td>not valid</td><td>not valid</td></tr>
<tr><td style="color: rgb(255, 0, 0);">Peirce</td><td>not valid</td><td>valid</td></tr>
<tr><td>WEM</td><td>not valid</td><td>not valid</td></tr>
<tr><td>Cond. EM</td><td>not valid</td><td>not valid</td></tr>
<tr><td>Dummett</td><td>not valid</td><td>not valid</td></tr>
<tr><td>DNI</td><td>valid</td><td>valid</td></tr>
<tr><td>DNE</td><td>valid</td><td>valid</td></tr>
<tr><td>K</td><td>valid</td><td>valid</td></tr>
<tr><td>B</td><td>valid</td><td>valid</td></tr>
<tr><td>C</td><td>valid</td><td>valid</td></tr>
<tr><td>W</td><td>valid</td><td>valid</td></tr>
<tr><td>Scott</td><td>tried to depth 36</td><td>tried to depth 20</td></tr>
<tr><td style="color: rgb(255, 0, 0);">Smetanich</td><td>tried to depth 24</td><td>valid</td></tr>
<tr><td>DM1</td><td>valid</td><td>valid</td></tr>
<tr><td>DM2</td><td>valid</td><td>valid</td></tr>
<tr><td>DM3</td><td>valid</td><td>valid</td></tr>
<tr><td>DM4</td><td>valid</td><td>valid</td></tr>
</tbody></table>
The ones where I tried to a certain depth I'm pretty sure are <i>not</i> valid because of the existence of infinite branches. I don't have a proof of this yet.Sara L. Uckelmanhttp://www.blogger.com/profile/14716054827293611237noreply@blogger.com0tag:blogger.com,1999:blog-5371132400241072988.post-17122015738936592642011-06-28T04:02:00.000-07:002011-07-05T10:16:05.019-07:00Fill in the Blanks<b>Note: Rather than continuing to update this post, the results can be found in the results paper linked in <a href="http://dialogue-games.blogspot.com/2011/07/summary-of-trip.html">this post</a>.</b>
<table border="1">
<tbody><tr><th>
</th><th>D10</th><th>D11</th><th>D12</th><th>D13</th><th>E</th><th>notes</th></tr>
<tr><td>N</td><td>X</td><td></td><td></td><td>X</td><td></td><td>AU</td></tr>
<tr><td>CL</td><td>X</td><td></td><td></td><td>X</td><td>X</td><td>AKU</td></tr>
<tr><td>not CL</td><td>X</td><td></td><td>X</td><td>X</td><td></td><td>excluded middle, Peirce not valid</td></tr>
<tr><td>not CL</td><td>X</td><td></td><td>X</td><td>X</td><td>X</td><td>validates Peirce, does not validate excluded middle</td></tr>
<tr><td>IL</td><td>X</td><td>X</td><td></td><td>X</td><td></td><td>U, blog post</td></tr>
<tr><td>IL</td><td>X</td><td>X</td><td></td><td>X</td><td>X</td><td>U, blog post</td></tr>
<tr><td>IL</td><td>X</td><td>X</td><td>X</td><td>X</td><td>
</td><td>Felscher</td></tr>
<tr><td>IL</td><td>X</td><td>X</td><td>X</td><td>X</td><td>X</td><td>Felscher</td></tr>
</tbody></table>Sara L. Uckelmanhttp://www.blogger.com/profile/14716054827293611237noreply@blogger.com0tag:blogger.com,1999:blog-5371132400241072988.post-52243684357443444732011-06-28T02:24:00.001-07:002011-06-28T03:17:20.078-07:00make that three conjecturesI'm beginning to wonder if it is the case that for every winning E-strategy s there is an expansion s' of s such that s' is a winning D-strategy.
The example I'm doing is:
<blockquote>(not (not (implies (implies (implies a b) c) (implies (implies (implies b a) c) c)))) </blockquote>
i.e.,
<blockquote>¬¬(((A → B) → C) → (((B → A) → C) → C))</blockquote>
<p>And if I start off by following the E-strategy <a href="http://dialogue-games.blogspot.com/2011/06/some-evidence-for-bold-conjecture.html">we found last week</a> for this formula, I can extend the left-most branch and then close it, but once I get into the middle branch, I'm finding I'm getting into what appears to be a cycle; I'm running out of options which don't provide branching for O, so the width of the tree keeps getting bigger and bigger and bigger.</p>
<p>Of course, maybe I haven't figured out the right algorithm for closing the branches. But I spent a lot of yesterday afternoon, and a good portion of this morning, working on it, and I'm getting into the same rut every single time. This makes me worried.</p>
<p>ETA: <b>I was wrong!</b> (Thank goodness). After at one point exploring the tree down to depth 46 and width I-have-no-idea), I started from scratch for yet another time, and finally found a winning D-strat that extends the E-strat (but only at the leaves, so this may not in fact be a winning D-strat; that's to test next). Unfortunately, the strat is too wide to get a screen shot of and display here. However, I've saved the code and you can view it <a href="http://staff.science.uva.nl/~suckelma/dialogues/strat-280611.html">here</a>.</p>Sara L. Uckelmanhttp://www.blogger.com/profile/14716054827293611237noreply@blogger.com0tag:blogger.com,1999:blog-5371132400241072988.post-61564076097364527822011-06-28T02:18:00.001-07:002011-06-28T02:18:52.081-07:00Characterizing classical logic dialogically<p>Here's a simple question:</p>
<blockquote>Do we know how to characterize classical logic (<strong>CL</strong>) dialogically?</blockquote>
<p>The answer is, thankfully, “yes”. Various proofs are available. Together with a masters student at the ILLC, Aleks Knoks, Sara and I found a correspondence between <strong>LK</strong> deductions (more precisely, deductions in a proof search-friendly variant of <strong>LK</strong>) and (what we called) classical dialogues. (Our proof does not literally use Felscher's notation for dialogue games; instead, we extended Fermüller's notation, found in his “<a href="http://www.springerlink.com/content/ry9c89alfa120l08">Parallel dialogue games and hypersequents for intermediate logics</a>”. It's clear that there's no essential difference between Fermüller-style games and Felscher-style games.</p>
<p>Here's a related question:</p>
<blockquote>
How do we characterize <strong>CL</strong> using Felscher-style dialogues?
</blockquote>
<p>The question is motivated by a desire to find some general framework for dialogues in which we can understand how the E-rule above is redundant. The motivating example is the dialogical characterization of intuitionistic logic (<strong>IL</strong>): it turns out that the E-rule is redundant in the presence of other structural rules. One way to understand the redundance of E is to look at other logics and their dialogical characterizations. Is the E rule redundant for these, too?</p>
<p>Turing to classical logic, the salient structural rules are:</p>
<dl>
<dt>D11</dt>
<dd>Defenses must be against only the most recent open attack. (An attack is said to be <em>open</em> if there is no defensive move in the game that responds to the attack. Non-open attacks are <em>closed</em>.)</dd>
<dt>D12</dt>
<dd>Attacks may be answered at most once.</dd>
<dt>E</dt>
<dd><strong>O</strong> must react to the immediately preceding statment by <strong>P</strong>.</dd>
</dl>
<p>
Based on the work mentioned before, I'm pretty sure that one way to get <strong>CL</strong> is to keep E but remove the other two rules. But this is, for the present discussion, a negative example because the E rule, far from being redundant, is crucial. We can't drop all three of these conditions. The result of doing so is the curiosity <strong>N</strong>; and we have known for some time that <strong>N</strong> ≠ <strong>CL</strong>. This leaves open some other questions: what if we keep D11 or D12? Do we find that E is redundant in those cases as well?</p>
<p>
Sara's <a href="/2011/06/role-of-d11-and-d12-in-il.html" title="How do D and E diverge?">recent slick observation</a> about the redundancy of D12 helps with this, but we still have some work to do.</p>Jesse Alamahttp://www.blogger.com/profile/18300729364134604326noreply@blogger.com8tag:blogger.com,1999:blog-5371132400241072988.post-59799747442529858052011-06-28T02:08:00.000-07:002011-06-28T02:16:27.230-07:00two more conjecturesThe 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 <a href="http://www.dialogical-logic.info/">"search for a strategy (interactively)"</a> functionality, which I am loving) investigating, and it doesn't seem <i>prima facie</i> false:
<blockquote><b>Conjecture</b>: 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.</blockquote>
<p>Check back often for evidence for or against this conjecture.</p>
<p>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 <a href="http://dialogue-games.blogspot.com/2011/06/role-of-d11-and-d12-in-il.html">D10+D12+D13=IL</a>, 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.</p>Sara L. Uckelmanhttp://www.blogger.com/profile/14716054827293611237noreply@blogger.com0tag:blogger.com,1999:blog-5371132400241072988.post-59607315397076251892011-06-24T03:58:00.000-07:002011-06-24T04:07:34.665-07:00Proof of BC #2Proving the second <a href="http://dialogue-games.blogspot.com/2011/06/bold-conjectures.html">bold conjecture</a> from yesterday turned out to be straightforward:
<blockquote>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.
<ul>
<li>s' is an E-strategy: All moves which violate E have been removed. All other rules are unaffected by truncation:
<ul>
<li>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.</li>
<li>D11, D12, D13: Straightforward.</li>
</ul>
</li>
<li>s' is a winning E-strategy. Suppose b' in s' is such that P has not won. Either:
<ol>
<li>The leaf of b' is a move by O, or</li>
<li>The leaf of b' is a move by P, but there is a legal continuation of the branch according to E.</li>
</ol>
(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:
<center>
<table>
<tr><td>b</td><td></td><td>round n (P's move)</td><td></td><td>b*</td></tr>
<tr><td></td><td>/</td><td></td><td>\</td><td></td></tr>
<tr><td>round n+1: E-violating move by O</td><td></td><td></td><td></td><td>round n+1: E-non-violating move by O</td></tr>
</table>
</center>
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:
<center>
<table>
<tr><td>round n (P's move)</td></tr>
<tr><td>|</td></tr>
<tr><td>round n+1: E-non-violating move by O</td></tr>
</table>
</center>
And hence, contra assumption, n is not a leaf in b'.
</li>
</ul>
QED</blockquote>Sara L. Uckelmanhttp://www.blogger.com/profile/14716054827293611237noreply@blogger.com0tag:blogger.com,1999:blog-5371132400241072988.post-51060536508683654022011-06-24T03:11:00.000-07:002011-06-24T03:22:10.149-07:00When P must repeat a moveIn his <a href="http://dialogue-games.blogspot.com/2011/06/new-functionality-on-dialogues-site.html">previous post</a>, 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.Sara L. Uckelmanhttp://www.blogger.com/profile/14716054827293611237noreply@blogger.com0tag:blogger.com,1999:blog-5371132400241072988.post-22803589287765113472011-06-24T02:18:00.001-07:002011-06-24T02:19:32.195-07:00New functionality on the dialogues site: interactively searching for strategies<p>Thanks to some prodding from Sara, I've implemented some new functionality to <a href=http://www.dialogical-logic.info">the dialogues site</a>: 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.</p>
<p>
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 <a href="https://github.com/jessealama/dialogues/blob/master/strategy.lisp#L208"><tt>PLAY-STRATEGY-SEARCH-GAME</tt></a> in the source), but it has not yet been translated to an HTML presentation yet.</p>
<p>
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.</p>
<p>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.</p>Jesse Alamahttp://www.blogger.com/profile/18300729364134604326noreply@blogger.com1tag:blogger.com,1999:blog-5371132400241072988.post-12740740360017650232011-06-23T08:00:00.000-07:002011-06-24T05:14:03.741-07:00Proof of BC 1I was pretty sure that I had an easy way to prove <a href="http://dialogue-games.blogspot.com/2011/06/bold-conjectures.html">Bold Conjecture #1</a>, 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:
<blockquote><i>Proof</i>: Assume round <i>n</i> is the first time where O violates E, that is, he references some round <i>n</i>−<i>i</i> such that <i>i</i>≠ 1. Assume further that this is the first time that round <i>n</i>−<i>i</i> has been referenced. Now, look at round (<i>n</i>−<i>i</i>)+1. What move does O reference here? If it is not <i>n</i>−<i>i</i>, then, contra assumption, round n is not the first round where E has been violated. If it is <i>n</i>−<i>i</i>, then, contra assumption, round <i>n</i> is not the first round where <i>n</i>−<i>i</i> is referenced. QED.</blockquote>Sara L. Uckelmanhttp://www.blogger.com/profile/14716054827293611237noreply@blogger.com0tag:blogger.com,1999:blog-5371132400241072988.post-81592540619310714952011-06-23T07:50:00.001-07:002011-06-23T07:58:00.082-07:00Some evidence for a bold conjectureSara 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
<blockquote>
<i>¬¬(((A → B) → C) → (((B → A) → C) → C))</i>
</blockquote>
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):
<img style="display:block; margin-left:auto; margin-right:auto;" src="http://lh4.ggpht.com/-rxJQCDxp6rU/TgNUZ-3FlII/AAAAAAAAABc/h5VWl_40Tbg/sara-conjecture-not-disconfirmed-selection.jpg?imgmax=800" alt="Sara conjecture not disconfirmed selection" title="sara-conjecture-not-disconfirmed-selection.jpg" border="0" width="500" height="294" />
In this example, see various cases where the E rule is violated:
<ul>
<li>in the left branch at move 15;</li>
<li>in the middle branch also at move 15;</li>
<li>in the right branch at move 9.</li>
</ul>
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.Jesse Alamahttp://www.blogger.com/profile/18300729364134604326noreply@blogger.com0tag:blogger.com,1999:blog-5371132400241072988.post-23701157912005931782011-06-23T06:14:00.000-07:002011-06-24T06:50:41.416-07:00Bold conjecturesBecause 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:
<ul>
<li>[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.</li>
<li>(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.</li>
</ul>
So: The hunt for counterexamples is on!Sara L. Uckelmanhttp://www.blogger.com/profile/14716054827293611237noreply@blogger.com0tag:blogger.com,1999:blog-5371132400241072988.post-19304917325392414232011-06-20T02:45:00.001-07:002011-06-23T06:58:16.013-07:00A simpler caseSome amount of thought on the previous post made it clear to me that my example was way more complicated than it needs to be. The following formula should be IL valid and allows Opp to assert a conditional so that Pro can attack it:
<blockquote>(implies (implies (and p p) q) (implies (and p p) q))</blockquote>
Or, in readable fashion:
<blockquote>(((P ∧ P) → Q) → ((P ∧ P) → Q))</blockquote>
I'm hoping that this example is small enough that the <a href="http://www.dialogical-logic.info/">dialogues website</a> can compute both the D and E strategies for me.
<p>---</p>
ETA: This is still too complicated a formula for the site, so I calculated the D and E strategies by hand; they do differ, but only by the final two moves in two of the three branches [ETA, 23Jun: This is wrong; I did not finish filling out one of the branches]. I came up with a more interesting example:
<blockquote>(implies (implies (and p p) (implies p q)) (implies (and p p) (implies p q)))</blockquote>
Or, readable:
<blockquote>(((P ∧ P) → (P → Q) → ((P ∧ P) → (P → Q))</blockquote>
Here, not only does the game <i>not</i> immediately end when Pro asserts an atom (he does so in the attack on an implication, which means that Opp still has the possibility to defend), but the D and E strategies differ by the final four moves in two of the branches. If I can think of a way to nicely represent the trees in HTML, I'll try to post all four strategies here.Sara L. Uckelmanhttp://www.blogger.com/profile/14716054827293611237noreply@blogger.com0tag:blogger.com,1999:blog-5371132400241072988.post-14249347181888201562011-06-16T03:24:00.001-07:002011-06-16T03:48:16.313-07:00How do D and E diverge?<p>In order to understand how to get from D strategies to E strategies, I've been trying to think about cases where they diverge -- that is, dialogues which are D-strategies, but not already additionally E-strategies. Recall that we are in the presence of D11 and D13; by D11, an attack may be defended at most once, and by D13, a P-assertion can be attacked at most once. These put significant constraints on O. In fact, I've come to the conclusion that the only time when O will be faced with a choice is when P has attacked a conditional; then, and only then, O has a choice between defending the conditional and attacking its antecedent (assuming it is non-atomic). In either of these cases, it follows that the conditional was originally asserted by O.</p>
<p>Under what conditions will a conditional be asserted by O? In defense of \wedge_L, \wedge_R, or ?, or as an attack on a negation. The former imply that O has previously asserted a conjunction or a disjunction one of whose conjuncts/disjuncts is a conditional. Take the latter; this means that P has asserted a negated conditional. I have yet to come up with an example where P actually does so, but I'm wondering if it shouldn't be possible to construct one via substitution of such for an atom in a IL-valid formula. Hmmmm...</p>
<p>Well, I've found a formula which should be IL-valid and allows O to assert a conditional:</p>
<blockquote><p>(implies (not (not (implies (and p p) q))) (not (not (not (not (implies (and p p) q))))))</p></blockquote>
<p>Or, in more readable format:</p>
<blockquote><p> (¬¬((P ∧ P) → Q) → ¬¬¬¬((P ∧ P) → Q))</p></blockquote>
<p>However, at the point where O has a choice of moves, if he <i>doesn't</i> take the option of defending the attack on the conditional, then he loses it; the rest of the dialogue is so full of attacks on negations, which are undefensible and hence always remain open, that D11 will prevent him from going back and re-defending. So, in order for a D strategy to differ from an E strategy, (a) O must assert a conditional, (b) P must attack it, (c) O must defend it immediately.</p>Sara L. Uckelmanhttp://www.blogger.com/profile/14716054827293611237noreply@blogger.com0tag:blogger.com,1999:blog-5371132400241072988.post-49926301158810433642011-06-10T02:50:00.000-07:002011-06-10T02:54:39.097-07:00The role of D11 and D12 in ILThinking more on what I wrote about <a href="http://dialogue-games.blogspot.com/2011/06/this-is-what-happens-when-you-think-too.html">a few days ago</a>, I'm convinced of the redundancy of D12 ("An attack may be answered at most once") in the presence of D11 ("At any round, a player may defend against only the latest open attack made by the other player"). An easy proof:
<blockquote>The proof relies on the fact that once an attack has been defended, it is no longer open. Since D11 requires that every defense be made against an open attack, once an attack has been defended and is closed, no defense will be made against it again. Thus, any attack will be answered at most once.</blockquote>
This shows that D10-D11-D13 is a sufficient ruleset to generate IL. I kind of thought one of the results would be trivial; and this was it. I still think that it may be the case that D10-D12-D13 also characterizes IL, but I haven't had time to work further on that conjecture.Sara L. Uckelmanhttp://www.blogger.com/profile/14716054827293611237noreply@blogger.com1tag:blogger.com,1999:blog-5371132400241072988.post-57952031269147354802011-06-08T05:56:00.001-07:002011-06-08T06:00:32.096-07:00this is what happens when you think too much about dialoguesYou start developing gut feelings; and the problem with gut feelings is that they are hard to transfer. It was a gut feeling about how N worked that led me to the characterization of implications in that system; and Jesse didn't believe me until he'd fully worked out a proof.
Working with N meant focus on D10 and D13. Today, for reasons I'm not still entirely sure, I found myself back in Felscher's article, looking at D11 and D12, and suddenly I'm not seeing how they aren't redundant w.r.t. each other:
<ul>
<li>D11: Only the latest open attack may be defended.</li>
<li>D12: An attack may be answered at most once.</li>
</ul>
I got Jesse to set up two new rulesets on the <a href="http://www.dialogical-logic.info/">dialogues site</a>, D10-D11-D13, and D10-D12-D13, and after some simple playing around with the latter, I'm beginning to develop another feeling in my gut, namely that one or the other of these is sufficient to characterize IL, even though at this point I haven't a clue which. I would LOVE to find a counterexample to this gut feeling, but I've got a feeling there's no systematic way to go about finding one, and thus I must test it via hit-and-miss potential counterexamples.
Hmmm. Or maybe I can find a nice axiomatization of IL and test each axiom in both sets. Would that really be enough?Sara L. Uckelmanhttp://www.blogger.com/profile/14716054827293611237noreply@blogger.com2tag:blogger.com,1999:blog-5371132400241072988.post-2568872939003929052011-05-11T03:11:00.000-07:002011-05-11T03:16:38.367-07:00What we've been up to<ul>
<li>Jesse and I revised our paper from the Inside Arguments Colloquium and submitted it for the proceedings: <a href="http://staff.science.uva.nl/~suckelma/latex/inside-arguments/insideargs.pdf">"What is Dialogical About Dialogical Logic?"</a></li>
<li>The two of us along with Aleks Knoks have had a short paper accepted to <a href="http://www.tableaux11.unibe.ch/">TABLEAUX 2011</a> in July: <a href="http://staff.science.uva.nl/~suckelma/latex/tableaux2011/shortpaper-cl.pdf">"Dialogue Games for Classical Logic"</a>. Either Jesse or Aleks, or both, will be attending the conference.</li>
<li>Jesse presented the long version of this paper at ProDi in Tübingen, as mentioned in an earlier post; Ole Thomassen Hjortland had some <a href="http://hiddenabacus.com/2011/03/tubingen/">nice things to say</a> about our results.</li>
<li>Next big thing on the dialogical horizon is our 6-week visit to Vienna to work with <a href="http://www.logic.at/staff/chrisf/">Chris Fermüller</a>, <a href="http://www.logic.at/staff/roschger/">Christoph Roschger</a>, and <a href="https://tiss.tuwien.ac.at/adressbuch/adressbuch/person_via_oid/944017.html">Friedrich Slivovsky</a>.</li>
</ul>Sara L. Uckelmanhttp://www.blogger.com/profile/14716054827293611237noreply@blogger.com0tag:blogger.com,1999:blog-5371132400241072988.post-19855049959771516872011-03-29T03:53:00.000-07:002011-03-29T03:59:08.122-07:00Inside Arguments, Coimbra, PortugalOn Saturday, March 26, Jesse and I presented our paper <a href="http://staff.science.uva.nl/~suckelma/latex/inside-arguments/insideargs.pdf">"Lorenzen dialogues as logical semantics"</a> at the International Colloquium <a href="http://www.uc.pt/fluc/dfci/international_colloquium_Inside_Arguments">Inside Arguments</a>; our slides are available <a href="http://staff.science.uva.nl/~suckelma/latex/inside-arguments/slides-coimbra.pdf">here</a>.
In this paper, we argue <i>against</i> an argumentation-theoretic understanding of dialogue games. While it may be the case that Lorenzen's original motivation for dialogical semantics came from a desire to connect intuitionistic theoremhood with real principles of dialogue, interaction, and debate, it is unclear to what extent this philosophical foundations can be carried through to the extensions of the approach to classical logic, modal logic, etc. We give three arguments against any strong connection between actual argumentative practice and dialogical semantics:
<ul>
<li> The lack of disagreement on the proper set of structural rules for intuitionistic logic (cf. the wildly different approaches of, e.g., Felscher and Rahman).</li>
<li> The problem, illustrated by <b>N</b>, of the interplays that arise in sets of independently plausible structural rules.</li>
<li> Difficulties in identifying acceptable criteria which allow us to rule out particle rules for connectives like tonk, but which do not force us to rule out, e.g., the particle rules for negation.</li>
</ul>
Unfortunately we had to leave almost immediately after our talk in order to get the train back to Lisbon, so there was not much time for discussion, but judging from the reactions of the audience during the presentation, the reaction was favorable.Sara L. Uckelmanhttp://www.blogger.com/profile/14716054827293611237noreply@blogger.com0tag:blogger.com,1999:blog-5371132400241072988.post-46697425374401316352011-03-01T04:50:00.001-08:002011-03-02T05:27:39.958-08:00Presentation on dialogue games for classical logic at ProDi<p>
I presented the result (joint with Sara and Aleks Knoks, whom <a href="http://dialogue-games.blogspot.com/2011/01/recent-news.html">we snagged</a> to work on dialogues with us) on an extension of what I've been calling Fermüller-style dialogue games to classical logic. Fermüller gave a nice presentation of a dialogue game for intuitionistic logic, and presented a proof of the soundness and completeness of his games in his “<a href="http://www.springerlink.com/content/ry9c89alfa120l08/">Parallel Dialogue Games and Hypersequents for Intermediate Logics</a>” (which was discussed earlier [<a href="http://dialogue-games.blogspot.com/2010/10/some-notes-on-c-fermuller-parallel.html">Part 1</a>], [<a href="http://dialogue-games.blogspot.com/2010/10/some-notes-on-c-fermuller-parallel_25.html">Part 2</a>], [<a href="http://dialogue-games.blogspot.com/2010/11/some-notes-on-c-fermuller-parallel.html">Part 3</a>], [<a href="http://dialogue-games.blogspot.com/2010/11/some-notes-on-c-fermuller-parallel_05.html">Part 4</a>]). Chris Fermüller was at the workshop and attended my talk. He didn't much like the name “Fermüller-style dialogues”, the idea being that his dialogues are at most a notational variant of ordinary dialogue games. I defended the choice of term by pointing out that the idea of extending his intuitionistic games to classical logic was more attractive and feasible than it is for other formalisms for dialogues. I think this is a case where a change of notation is significant.</p>
<p>
As I expected, there was some pushback at the basic motivation of the paper, which is that our result is worthwhile owing to the extremely small number of explicit proofs in the dialogue literature of the correspondence between classical logic and classical dialogues (in whatever form one likes). We know of only two proofs, one by Fermüller himself, and another by Sørensen and Urzyczyn. Our proof has the advantage that it works with a standard sequent calculus, rather than with hypersequents (Fermüller) or one that is specially tuned for the purpose of establishing the correspondence (Sørensen and Urzyczyn).</p>
<p>
It was an honor to present the work to an audience that contained several experts on dialogical logic. <a href="http://centria.di.fct.unl.pt/~alama/materials/2011-02-27-prodi/dialogue-games-for-classical-logic.pdf">Here are the slides</a>. The presentation was rather less than ideal: there were so many talks on dialogues preceding mine (not to mention that Fermüller himself presented his games <a href="http://www-ls.informatik.uni-tuebingen.de/prodi/schedule.html">immediately before me</a>) that the first several slides could have been cut, and other interesting issues from the paper could have been dealt with. The paper on which the slides are based can be found <a href="http://staff.science.uva.nl/~suckelma/latex/tableaux2011/clproof.pdf">on Sara's homepage</a> or <a href="http://centria.di.fct.unl.pt/~alama/materials/preprints/dialogue-games-for-classical-logic.pdf">on my homepage</a>.</p>Jesse Alamahttp://www.blogger.com/profile/18300729364134604326noreply@blogger.com0tag:blogger.com,1999:blog-5371132400241072988.post-62255278730086578692011-02-25T09:01:00.000-08:002011-02-25T09:20:39.322-08:00Live Blogging: ProDi Day 1, part 3<b>Tero Tulenheimo</b> is speaking on "Remarks on Game-Based Theories of Meaning".
He points out how game-theoretic semantics are importantly connected with truth-conditional theories of meaning. Interesting, dialogue games like those for N indicate, or at least seem to, that truth-conditional semantics are <i>not</i> necessary for a class of dialogue games to be able to capture a logic. But perhaps this just means (as many people have argued), that N is meaningless.
The talk now veers to the realism/anti-realism debate, and the connections with Hintikka's game-theoretic semantics. Unfortunately, my battery will be dying soon, so I doubt I'll be able to finish blogging this talk.Sara L. Uckelmanhttp://www.blogger.com/profile/14716054827293611237noreply@blogger.com0tag:blogger.com,1999:blog-5371132400241072988.post-47463333503426148002011-02-25T08:17:00.000-08:002011-02-25T08:53:11.642-08:00Live Blogging - ProDi Day 1, part 2<p>Next up, <b>Laurent Keiff</b>, "Dialogues and Trivializing Connectives". This should be interesting, as one of the questions he's asking is "What are the limits of the framework?", which is closely related to questions Jesse and I explored last fall.</p>
<p>His definition of dialogue games follows the approach of Fermüller; there is an initial <i>set</i> of assertions by the Opponent, and he indicates positions of games via dialogue sequents. However, he only allows one assertion of Proponent in the initial state, so his dialogues are, at base, intuitionistic.</p>
<p>For Keiff, particle rules must be "anonymous"; this is just player neutrality at the local level. Unfortunately, he doesn't give sufficiently precise definitions of the particle and structural rules to evaluate whether the same worry that I have from Rahman's paper is present here.</p>
<p>Much of his talk is focusing on developing rules for tonk, and tonk-like operators. I have to confess, I'm not entirely sure I understand the fascination the Lille people have with tonk. It seems like it will always be possible to allow, or not allow, tonk rules. This, in and of itself, is not problematic, any more than the fact that classical proof theory allows the introduction of a tonk rules. What's important is that we <i>can</i> block the adoption of tonk, that we're not forced to use it. So, if we're interested in investigating interesting logics that arise from the dialogical tradition, we should avoid adding trivializing connectives like tonk.</p>Sara L. Uckelmanhttp://www.blogger.com/profile/14716054827293611237noreply@blogger.com0