The stack calculus : a fundamental (and simple !) calculus for Classical Logic

Around April 1 (but doesn't seem like a joke) 2013, on arxiv:
Alberto Carraro, Thomas Erhard, Antonino Salibra,
The stack calculus
(direct PDF link)

We introduce a functional calculus with simple syntax and operational semantics in which the calculi introduced so far in the Curry–Howard correspondence for Classical Logic can be faithfully encoded. Our calculus enjoys confluence without any restriction. Its type system enforces strong normalization of expressions and it is a sound and complete system for full implicational Classical Logic. We give a very simple denotational semantics which allows easy calculations of the interpretation of expressions.

I haven't looked at the details yet, but the result are surprisingly simple and look deeply interesting -- if you're into that sort of thing. I was always a bit rebuted the relatively large size of classical calculi, with lots of rules on top of the lambda-calculus. This one doesn't have a lambda primitive (a bit like System L in this respect) and is surprisingly concise.

(Fun fact: intuitionistic calculi are structured by the fact that there is only one hypothesis on the right of the turnstile. They have at most one hypothesis on the left of the turnstile.)

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Sequel

One of the authors seems to have tweaked the (untyped) calculus:
http://rvg.web.cse.unsw.edu.au/eptcs/paper.cgi?LSFA2012.9

Nice

Was a little bit distracted by the aprils fool hint, but didn't find an indication that it is not sound or not complete so far(*).

But does it have cut-elimination? Respectively does normalization result in a cut-free proof?

(*) The [mu, alfa] rule looks like double negation elimination:

G, ~A |- f
----------
G |- A

For classical logic this would make the [bot i] rule redundant.