Gentzen’s Dissertation
摘要
We provide an overview of the agenda and main results of Gentzen’s doctoral thesis. Situating these in their historical context highlights the centrality in Gentzen’s thought of what Schoenfield would later call the “characterization problem” of deductive proof systems. The scheme that emerges is seen to be an inversion of the more familiar program of providing soundness and completeness proofs for such systems. Several abbreviations introduced in this chapter (HK, HI, NK, NI, LK, LI, \(\text {LK}_{\text {CF}}\)) will be referred to continuously in later chapters.