Friday, April 20, 2007

Gentzen and Kripke and a coincidence?

I noticed a little symmetry recently and I'm not sure how to explain it yet. The symmetry is between intuitionistic and classical logic. In the Gentzen presentation for classical logic, you have \Gamma => \Delta, where \Delta and \Gamma are multisets. The inference rules for classical and intuitionstic logic are the same with one exception. The rules of intuitionistic logic restrict \Delta to singleton sets. So, proof theoretically (in Gentzen) we have (potentially) several formulas in conclusions for classical logic and only one in intuitionistic logic. Switch gears to semantics. Suppose we have a Kripke tree (W, ≤) for intuitionistic logic. This gives the semantics for intuitionistic logic. Restrict the set of worlds W to a singleton and it becomes classical semantics. So, semantically (in Kripke) we have several worlds for intuitionistic logic and only one world for classical. (You get the same thing if ≤ is an equivalence relation, but this just makes W behave as if it had only one world.)

Why would this be? In proof theory, allowing multiple conclusions lets you move formulas back and forth at will from antecedent to consequent, e.g. p=>p,\bot goes to =>p, ~p which goes to =>pv~p. Restricting to one conclusion means you can't derive the law of excluded middle for arbitrary formulas like that, since the first step is blocked. In the semantics, you get ~p only if all the worlds ≤ the world of evaluation do not verify p. This means that you can have a world w that doesn't verify p but also doesn't verify ~p since some w'≥w does verify p. Restricting to one world eliminates this wiggle room, since there will not be any such w'≥w if w is the only world. If w verifies p, then p. If w doesn't verify p, then ~p. Classical. Why there should be any sort of symmetry I don't know.


Ole Thomassen Hjortland said...

There is an interesting article about Gentzen's observation by Peter Milne, 'Harmony, Purity, Simplicity and a "Seemingly Magical Fact"' (2002), The Monist, vol. 85. The 'seemingly magical fact' is a phrase used by Ian Hacking in 'What is logic?' about the fact that you CL from IL by restricting the succedent's cardinality in sequent calculus.

Shawn said...

Thanks Ole. I will try to check those out. I think I have a handle on why Kripke semantics for intuitionistic logic becomes classical when you restrict to one world, but the "seemingly magical fact" still sort of mystifies me. Oddly, I don't remember that phrase from Hacking's paper.