A natural deduction and its corresponding sequent calculus for positive contraction{less relevant logic
A natural deduction and its corresponding sequent calculus for positive contraction{less relevant logic

Summary/Abstract: We give a normalizing system of natural deduction for positive contraction{less relevant logic RW+. The specific characteristic of our calculus is that it has a simple translational relationship to a particular sequent calculus for RW+, such that normal natural deduction derivations correspond to cut-free sequent calculus derivations and vice versa. By translations from natural deduction to sequent calculus derivations, and back, together with cut{elimination, we obtain an indirect proof of the normalization.

• Details
• Contents