I don't know whether emphasising so much computational complexity is the right
thing to do.
[...] There is one thing that this complexity view doesn't require, namely the
kind of compositionality which is usually associated to deduction.
Compositionality seems central to me. While I would certainly expect
that the task of verifying a proof is computationally easy, I think that
I expect something more.
When I have to check a proof and in the middle of it I have to pop out
for lunch then I can put a check mark on the lemmas that I've already
checked such that when I come back I can resume where I left, without
having to do anything twice. Of course there's a way to do the same
thing with proof nets. But the question is: what does that mean,
logically, to have checked half of the correctness criterion?
Shouldn't this be the difference between deductive, compositional (say
sequent calculus) and non-deductive, global (say proof nets, connection
method)? In the first case you do half of the work and you get some
intermediate theorem from which the original theorem follows once you've
done the other half. In the second case doing half the work doesn't get
you that intermediate theorem, as far as I can see.
-Kai
