Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It only takes a minute to sign up.
Sign up to join this community
Consider the classical propositional calculus over the alphabet $\{\bot,\top,\neg,\land,\lor,\rightarrow\}$ with the following inference rules (together with the initial sequent):
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$.
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.
