Normal derivations and sequent derivations (Q1029828)

Normal proofs in natural deduction systems for intuitionistic logic roughly correspond to cut-free sequent derivations. This article elaborates on this correspondence. First, a system \(\mathcal{N}\) for natural deductions and a system \(\mathcal{S}\) for sequent derivations are introduced. Then, functions \(\phi\) and \(\varphi\) are defined that map natural deductions of \(\mathcal{N}\) to sequent derivations of \(\mathcal{S}\) and vice versa, so that \(\varphi\circ\phi\) is the identity on natural deductions, and further, the following relationship holds true: If \(\mathcal{D}\) is a sequent derivation without maximum cuts (i.e. cuts that correspond to maximum segments from natural deductions), then \(\varphi\mathcal{D}\) is a normal derivation, and, conversely, if \(\varphi\mathcal{D}\) is a normal derivation, then \(\mathcal{D}\) is a sequent derivation without maximum cuts. The author concludes that therefore sequent derivations without maximum cuts and normal derivations ``are the same''.