Consider the classical propositional calculus over the alphabet $\{\bot,\top,\neg,\land,\lor,\rightarrow\}$ with the following inference rules (together with the initial sequent):

enter image description here

Is cut-elimination for this particular calculus proved somewhere in the literature? All I could find were proofs for calculi without the $0$-ary connectives $\bot$ and $\top$.


1 Answer 1


A standard reference is Mark Pfenning's paper "Structural Cut Elimination I. Intuitionistic and Classical Logic", Information and Computation 157, 84-141 (2000).

It proves cut-elimination for classical and intuitionistic sequent calculi whose rules are very similar to the ones you posted. The details of the proof are in the appendix of that paper.

The calculi have the $0$-ary connectives $\top$ and $\bot$, but also quantifiers (you can skip them). The paper also presents a formalization of the proof in Elf, but you should be able to follow this paper by ignoring the material regarding the formalization.

The introduction also contains further references.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .