Proof Normalization I: Gentzen's Hauptsatz


Author: Amos Omondi
Pages: 39
Source: GZipped PostScript (135kb); Adobe PDF (549kb)

This paper is the first of a two-part introductory discussion of Gentzen's Hauptsatz, Prawitz's Normalization Theorem, and related results, which are concerned with the elimination of cuts in the calculi of sequents and the calculi of natural deduction. Cuts correspond to detours in proofs and hence there is undoubtedly some philosophical interest in being able to eliminate them. These results also have mathematical interest and applications that are of use in computation and this is the underlying motivation for this paper.

[Up to Computer Science Technical Report Archive: Home Page]