Diploma Thesis:
Proof Nets for Intuitionistic Logic

by Matthias Horbach

Advisor: Lutz Straßburger
Responsible Professor: Gert Smolka
Research Unit: Programming Systems Lab, Department of Computer Science, Saarland University


Thesis (ps.gz, pdf), BibTeX


At the beginning of the 20th century, there was no way to reason formally about proofs. In particular, the question of proof equivalence had never been explored. When Hilbert asked in 1920 for an answer to this very question in his famous program, people started looking for proof formalizations.

Natural deduction and sequent calculi, which were invented by Gentzen in 1935, quickly became two of the main tools for the study of proofs. Gentzen's Hauptsatz on normal forms for his sequent calculi, and later on Prawitz' analog theorem for natural deduction, put forth a first notion of equivalent proofs in intuitionistic and classical logic.

However, natural deduction only works well for intuitionistic logic. This is why Girard invented proof nets in 1986 as an analog to natural deduction for (the multiplicative fragment of) linear logic. Their universal structure made proof nets also interesting for other logics. Proof nets have the great advantage that they eliminate most of the bureaucracy involved in deductive systems and so are probably closer to the essence of a proof. There has recently been an increasing interest in the development of proof nets for various kinds of logics. In 2005 for example, Lamarche and Straßburger were able to express sequent proofs in classical logic as proof nets.

In this thesis, I will, starting from proof nets for classical logic, turn the focus back on intuitionistic logic and propose proof nets that are suited as an extension of natural deduction. I will examine these nets and characterize those corresponding to natural deduction proofs. Additionally, I provide a cut elimination procedure for the new proof nets and prove termination and confluence for this reduction system, thus effectively a new notion of the equivalence of intuitionistic proofs.

Further Information

Slides of my Antrittsvortrag (where I described a task that turned ouf to be unsolvable) Slides of my final talk