[pdf - ps.gz]

Proceedings of WoLLIC 2006, ENTCS 165, 2006.

**Abstract**

Proofs Without Syntax [Ann. Math. '06]
introduced polynomial-time checkable combinatorial proofs for
classical propositional logic. This sequel approaches Hilbert's
*24 ^{th}
Problem* with combinatorial
proofs as abstract invariants for sequent calculus proofs, analogous
to homotopy groups as abstract invariants for topological spaces.

The paper lifts a simple, strongly normalising cut elimination from combinatorial proofs to sequent calculus, factorising away the mechanical commutations of structural rules which litter traditional syntactic cut elimination.

Sequent calculus fails to be surjective onto combinatorial proofs: the
paper extracts a semantically motivated closure of sequent calculus
from which there is a surjection, pointing towards an abstract
combinatorial refinement of Herbrand's theorem.

[Here is an earlier draft version of January 2006: Combinatorial Proof Semantics.]