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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Gentzen’s Dissertation

  • Curtis Franks

摘要

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.