## Author: Dominic Hughes

## Paper Information

Title: | Some incoherent musings on deep inference and combinatorial proofs |

Authors: | Dominic Hughes |

Proceedings: | TYDI-0 Abstracts |

Editor: | Lutz Straßburger |

Keywords: | categorical logic, linear distributivity, deep inference, combinatorial proofs, intuitionistic combinatorial proofs, first-order combinatorial proofs, linear logic, classical logic |

Abstract: | 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 |

Pages: | 1 |

Talk: | Jul 07 16:00 (Session 31R: Contraction) |

Paper: |