Focusing on Contraction
Alessandro Avellone, Camillo Fiorentini, Alberto Momigliano · BOA (University of Milano-Bicocca) · 2013
Focusing is a proof-theoretic device to structure proof search in the sequent calculus: it provides a normal form to cut-free proofs in which the application of invertible and non-invertible inference rules is structured in two separate and disjoint phases. It is commonly believed that every “reasonable” sequent calculus has a natural focused version. Although stemming from proof-search considerations, focusing has not been thoroughly investigated in actual theorem proving, in par- ticular w.r.t. termination, if not for the folk observations that only neg- ative formulas need to be duplicated (or contracted if seen from the top down) in the focusing phase. We present a contraction-free (and hence terminating) focused proof system for multi-succedent propositional intu- itionistic logic, which refines the G4ip calculus of Vorob’ev, Hudelmeier and Dyckhoff. We prove the completeness of the approach semantically and argue that this offers a viable alternative to other more syntactical means.