Cut elimination and normalization for generalized single and multi-conclusion sequent and natural deduction calculi

TL;DR

This paper develops systematic methods for constructing sequent calculus, natural deduction, and lambda calculus systems for various logical connectives, ensuring cut-elimination, normalization, and classical/intuitionistic variants.

Contribution

It introduces a general framework for generating sequent calculus rules from truth tables, leading to unified systems with cut-elimination and proof-term correspondences.

Findings

Cut-elimination and normalization are proven for the systems.

Generalized lambda calculi are derived for proof terms.

Classical and intuitionistic variants are obtained by restrictions.

Abstract

Any set of truth-functional connectives has sequent calculus rules that can be generated systematically from the truth tables of the connectives. Such a sequent calculus gives rise to a multi-conclusion natural deduction system and to a version of Parigot's free deduction. The elimination rules are "general," but can be systematically simplified. Cut-elimination and normalization hold. Restriction to a single formula in the succedent yields intuitionistic versions of these systems. The rules also yield generalized lambda calculi providing proof terms for natural deduction proofs as in the Curry-Howard isomorphism. Addition of an indirect proof rule yields classical single-conclusion versions of these systems. Gentzen's standard systems arise as special cases.