Sequent Calculus and Cut-Elimination
Cheong Kye-Seop · Journal for History of Mathematics · 2010
Sequent Calculus is a symmetrical version of the Natural Deduction which Gentzen restructured in 1934, where he presents 'Hauptsatz'. In this thesis, we will examine why the Cut-Elimination Theorem has such an important status in Proof Theory despite of the efficiency of the Cut Rule. Subsequently, the dynamic side of Curry-Howard correspondence which interprets the system of Natural Deduction as 'Simply typed -calculus', so to speak the correspondence of Cut-Elimination and -reduction in -calculus, will also be studied. The importance of this correspondence lies in matching the world of program and the world of mathematical proof. Also it guarantees the accuracy of program.