Por Serena Delli (Faculdade de Ciências e Tecnologia, Universidade Nova de Lisboa).

Abstract: Proof theory, unlike other mathematical disciplines, seeks a clear and well-defined notion of identity for formal proofs. This is because logical bureaucracy allows the formalisation of the same argument in several different ways. In response to this problem, proof-theorists have tried to design new, lighter, bureaucracy-free formalisms. Girard’s proof-nets constitute one of the first attempts in this direction. A considerable step forward on this topic has been made by Dominic Hughes, who introduced the notion of combinatorial proof. Combinatorial proofs are a mathematical formulation of first-order classical logic, where proofs are graph-theoretic and combinatorial, instead of syntactic.
Combinatorial proofs are explicitly designed to avoid the wild diversification generated by bureaucracy, making clear some patterns that in others formalisms were hidden by the syntax. In this talk, I am going to introduce the notion of combinatorial proof, and discuss its benefits and limits.