arXiv · math/0504028
Classical Logic = Fibred MLL
Abstract
This paper represents classical propositional proofs as *combinatorial proofs*, which are more abstract than proof nets: superposition (contraction/weakening) is modelled mathematically, as a lax form of fibration, rather than syntactically (as in proof nets, which involve contraction and weakening nodes). A combinatorial proof is a `fibred' multiplicative linear proof net, hence the slogan in the title. Cut elimination retains its richness from sequent calculus: its non-determinism does not collapse to become confluent. [Note: this is merely a 2-page synopsis, accepted for a short presentation at Logic in Computer Science '05.]
Explore related subjects
Keep this discovery
Dominic Hughes. 2005-04-01. Classical Logic = Fibred MLL. https://arxiv.org/abs/math/0504028
Cite the original work for its findings. Save a collection to share your selection of sources.