I’m at the Moscow-Vienna Workshop on Logic and Computation. We’re on the second day. Yesterday was started off with a way-over-my-head talk by Sergei Adian on his and Novikov’s solution to the Burnside problem. Today, Michel Parigot just gave a very interesting talk on a constructive, but classical proof system. His aim is to develop a system in which you can reason classically but still have nice properties like the disjunction property and the witness property. Of course, you don’t have those in general. So the aim is to have a classical proof system in which you have constructive disjunction and existential quantifiers as well. Then you can get the properties you’re looking for: if you can prove A ∨ B (where ∨ is constructive), then you have a constructive classical proof, and you either get a proof of A or a proof of B. I’m looking forward to the paper.
Now I’ll have to pay attention to Lev Beklemishev talking about provability logic.