In Proofs Without Syntax Dominic Hughes introduced combinatorial (graph-theoretical) proofs for classical propositional logic. In Towards Hilbert’s 24th Problem Hughes approaches the question of simplicity of proofs with combinatorial proofs as abstract invariants for sequent calculus proofs, analogous to homotopy groups as abstract invariants for topological spaces.

In a continuing series of short papers, we want to provide a small tutorial in combinatorial (graph-theoretical) proofs and explore its use and connections to proof-theoretical questions as the simplicity of proofs.