Just as the logical sequent rules of conjuction (tensor) and disjunction (par) are represented explicitly in the net, so are the structural rules, contraction and weakening. Unfortunately, this explicit representation of structural rules retains some of the redundancy (or `syntactic bureaucracy') of sequent calculus. For example, in the net presentation of classical categories in [FP05] one has to quotient by equations on nets, involving contraction and weakening. Thus, proof nets for classical logic fail to achieve the same elegance as the proof nets for MLL. We present a representation of a proof which is more abstract than a proof net, which we call a combinatorial proof : superposition is modelled mathematically, as a lax form of fibration, rather than syntactically (as in proof nets, which involve contraction and weakening nodes). This draws a nice boundary between logical rules and structural rules: the former are modeled with explicit nodes, the latter as actual superposition, in an abstract mathematical sense, without nodes. We can summarise the situation thus: The arrows represent the abstraction from sequent calculus to proof nets, and from proof nets to combinatorial proofs. To the right, we list the form of `bureaucracy' present at that layer, that is, the connectives involved in representation redundancy, i.e., sensible rule transpositions for identifying proofs. ( $\text{C}$  and $\text{W}$  stand for contraction and weakening.) The definition of combinatorial proof is very simple, so we can give it in full here.

Let $A$  be a formula of propositional classical logic, generated by $\wedge$  and $\vee$  from literals (variables $P,Q,\dots$  and their negations $\overline{P},\overline{Q},\dots$  ). We identify a formula $A$  with its parse tree, a tree labelled with literals at the leaves and $\wedge$  or $\vee$  at internal vertices. An $\vee$  -resolution (or $\vee$  -strategy) of $A$  is any result of deleting one argument subtree from each $\vee$  (cf. [HG03] ). A set $L$  of leaves of $A$  is a clique of $A$  if it is the set of leaves of a $\vee$  -resolution of $A$  . A combinatorial proof of $A$  is an MLL proof net on a formula $A^{\prime }$  (viewed as an MLL formula, i.e., $\wedge$  = tensor, $\vee$  = par), equipped with a labeland clique-preserving function from the leaves of $A^{\prime }$  to the leaves of $A$  . For example, here is a combinatorial proof of Peirce's law, $\left(\right(P\Rightarrow Q)\Rightarrow P)\Rightarrow P=\left(\right(\overline{P}\vee Q)\wedge \overline{P})\vee P$  :

$$\begin{array}{c}\overline{P}\wedge \overline{P}\vee (P\vee P)\end{array}$$

$$\begin{array}{c}\left(\right(\overline{P}\vee Q)\wedge \overline{P})\vee P\end{array}$$

The MLL proof net is drawn above, with two axiom links. The labeland clique-preserving function is shown by the vertical lines.

Theorem 1 (Soundness and Completeness)A formula of classical propositional logic is true (valid) iff it has a combinatorial proof.

The labeland clique-preserving function is a lax form of fibration. (We prove this via [Hug04] ). Thus a combinatorial proof is a `fibred' MLL proof net, and we obtain the slogan in the title of the paper:

Classical logic = Fibred MLL

Any sequent calculus proof translates to a combinatorial proof in a relatively obvious way. For a suitable variant of sequent calculus, one obtains a surjection (i.e., sequentialisation theorem). Cut elimination for combinatorial proofs retains the richness of sequent calculus: its non-determinism is not confluent. In contrast, direct translation of a sequent proof to a linking (the set of axiom links traced down from the axioms) leads to a certain degeneracy: cut elimination becomes confluent [LS05] . Also in contrast to [LS05] , the MIX rule in this setting is optional.

Combinatorial proofs, in a somewhat different guise, were first presented in [Hug04] , with MIX implicit.

References

1. C. Führmann and D. Pym. Order-enriched categorical models of the classical sequent calculus. J. Pure and Applied Algebra, 2005. To appear.
2. J.-Y. Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.
3. J.-Y. Girard. A new constructive logic: Classical logic. Mathematical Structures in Computer Science, 1(3):255–296, 1991.
4. D. J. D. Hughes and R. J. van Glabbeek. Proof nets for unit-free multiplicative additive linear logic (extended abstract). Proc. Logic in Computer Science '03, 2003.
5. D. J. D. Hughes. Proofs without syntax. Submitted for publication. Archived as math.LO/0408282 at arXiv.org, http://boole.stanford.edu/d͂ominic/papers, August 2004.
6. F. Lamarche and L. Straßburger. Naming proofs in classical propositional logic. In Proc. Typed Lambda Calculus '05, Lecture Notes in Computer Science, 2005. To appear.
7. E. Robinson. Proof nets for classical logic. J. Logic and Computation, 13(5):777–797, 2003.