ABSTRACT. In this talk I shall make every effort to be provocative and controversial, in an attempt to fuel introspection at the 20 year mark of deep inference. The talk has three parts:

(1) Is deep inference "incoherent categorical logic"? Here "incoherent" refers to the omission of proof equality, covered by the coherence laws of categorical logic [1]. Is deep inference in danger of isolating itself as a community by not preserving the original language of categorical logic? Hilbert's 24th problem is on proof equality [2]; does deep inference short-change itself by not retaining proof equality as a first-class citizen, as it was in categorical logic?

(2) Linear distributivity (originally known as weak distributivity) [3] is core to the categorical approach to linear logic, hence also deep inference, where it has become known as switch. Classical logic follows with contraction and weakening. Combinatorial proofs [4] are an irredundant abstraction [2] of classical syntactic proofs, yet there is no natural interpretation of switch on combinatorial proofs, while there *is* a natural interpretation of sequent calculus conjunction. Could there be a deeper computational meaning to this, which reflects back on the standard switch-based formulations of deep inference for linear and classical logic?

(3) Extensions of combinatorial proofs. In part (2) I will have shown how easily one may translate a classical propositional syntactic proof into a combinatorial proof (literally a 30-second definition - I promise!). I will then talk about two extensions, where the translation from syntactic proofs is also very easy to explain to a lay audience: (a) intuitionistic combinatorial proofs (joint work with Heijltjes and Strassburger), and (b) classical first-order combinatorial proofs [5].

References and background reading:

[1] Deep inference proof theory equals categorical proof theory minus coherence. http://boole.stanford.edu/~dominic/papers/di/di.pdf

[2] Towards Hilbert's 24th problem: combinatorial proof invariants. http://boole.stanford.edu/~dominic/papers/invar/invar.pdf

[3] Robin Cockett, Robert Seely. Weakly Distributive Categories, JPAA 114 (1997)2. http://www.math.mcgill.ca/rags/linear/wdc.ps.gz

[4] Proofs without syntax. Annals of Mathematics, 164 (2006). http://annals.math.princeton.edu/wp-content/uploads/annals-v164-n3-p09.pdf

[5] First-order Proofs Without Syntax. Slides for the Berkeley Logic Colloquium, Oct. 17, 2014. http://boole.stanford.edu/~dominic/papers/fopws-blc-2014