In this talk I will present a notion of proof nets for classical propositional logic. The basic motivation is that two classical proofs are represented by the same proof net if and only if they use the same argument. This should be independent from the formal system in which the proofs are given. More technically, we have the following results: a confluent cut elimination, a geometric correctness criterion, a sequentialization theorem, and a nontrivial categorical axiomatization, i.e. we get a category of classical proofs which does not collapse into a boolean algebra. Besides that, all the nice symmetries (in particular the De Morgan duality between conjunction and disjunction) of classical logic are present in the proof nets.
(joint work with François Lamarche)