Tuesday, August 24, 2010
I still have a half-written blog post from when I was in Lisbon last week, but I think it will have to wait, as now I'm thinking about something else, namely, how to handle assumptions in dialogical logic. While preparing a short note on the sound proof rules of N, I noticed that none of them have anything on the left-hand side of the turnstile; that is, none of the rules model anything like reasoning from assumptions. At this point, I have no idea if this is something specific to N, because we don't know enough about N, and how much of this is specific to the dialogical approach, which doesn't, on the face of it, allow for any type of reasoning from assumptions. Now what about IL and CL? They have dialogical characterizations and allow reasoning from assumptions, both in their ordinary semantics and in their proof theory. So why is it that they can be dialogically characterized, if ordinary structural/particle rules don't allow for assumptions? My suspicion is that it's because both logics satisfy a deduction theorem -- $\Gamma\vdash\phi$ iff $\vdash\Gamma\rightarrow\phi$, and hence you can "do away" with assumptions. Now, the fact that the proof rule from $\vdash\phi\rightarrow\psi$ infer $\vdash(\gamma\rightarrow\phi)\rightarrow(\gamma\rightarrow\psi)$ is not sound in N shows that N cannot have an ordinary deduction theorem, and so it is important to find a way to handle reasoning from assumptions in N in a dialogical way. Here is a naive approach, which I will ask Jesse to implement so I can test it via the website: - Fix a set of formulas $\Gamma$ such that Proponent can assert $\phi\in\Gamma$ at any time, as either an attack or as a defense. Essentially then $\Gamma\vDash\psi$ says "if you (Opponent) grant me (Proponent) the info in $\Gamma$, I can prove $\psi$ to you. Being that this is a naive approach, I do not know how well it will work. Luckily, since we know how reasoning from assumptions should work in IL and CL, we can use them as test cases for this approach.