We give a normalizing system of natural deduction for positive contraction-less relevant logic RW+⁰ . The specific 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.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.