Penn Arts & Sciences Logo

Logic and Computation Seminar

Monday, October 11, 2021 - 3:30pm

Dale Miller

Inria-Saclay, France


University of Pennsylvania


Gentzen's sequent calculi LK and LJ are landmark-proof systems. They identify the structural rules of weakening and contraction as notable inference rules, and they allow for an elegant statement and proof of both cut-elimination and consistency for classical and intuitionistic logics. Among the undesirable features of those sequent calculi is the fact that their inference rules are very low-level and that they frequently permute over each other. As a result, large-scale structures within sequent calculus proofs are hard to identify. In this talk, I will present a different approach to designing a sequent calculus for classical logic. Starting with Gentzen's LK proof system, I first examine the proof search meaning of his inference rules and classify those rules as involving either don't care non-determinism or don't know nondeterminism. Based on that classification, I design the focused proof system LKF in which inference rules belong to one of two phases of proof construction depending on which flavor of nondeterminism they involve. We then prove that the cut rule and the general form of the initial rule are admissible in LKF. Finally, by showing that the rules of inference for LK are all admissible in LKF, we can give a completeness proof for LKF provability with respect to LK provability. We shall also apply these properties of the LKF proof system to establish other meta-theoretic properties of classical logic, including Herbrand's theorem. This talk is based on a recent draft paper co-authored with Chuck Liang.