T i 2 = S i +1 2 implies ∑ p i +1 ⊆ Δ p i +1 ⧸poly. S 2 and IΔ 0 ƒ are not finitely axiomatizable. The main tool is a Herbrand-type witnessing theorem for ∃∀∃ П b i -formulas provable in T i 2 where the witnessing functions are □ p i +1.

This comprehensive monograph is a cornerstone in the area of mathematical logic and related fields. Focusing on Gentzen-type proof theory, the book presents a detailed overview of creative works by the author and other 20th-century logicians that includes applications of proof theory to logic as well as other areas of mathematics. 1975 edition.

Using set theory in the first part of his book, and proof theory in the second, Gaisi Takeuti gives us two examples of how mathematical logic can be used to obtain results previously derived in less elegant fashion by other mathematical techniques, especially analysis. In Part One, he applies Scott- Solovay's Boolean-valued models of set theory to analysis by means of complete Boolean algebras of projections. In Part Two, he develops classical analysis including complex analysis in Peano's arithmetic, (...) showing that any arithmetical theorem proved in analytic number theory is a theorem in Peano's arithmetic. In doing so, the author applies Gentzen's cut elimination theorem. Although the results of Part One may be regarded as straightforward consequences of the spectral theorem in function analysis, the use of Boolean- valued models makes explicit and precise analogies used by analysts to lift results from ordinary analysis to operators on a Hilbert space. Essentially expository in nature, Part Two yields a general method for showing that analytic proofs of theorems in number theory can be replaced by elementary proofs. Originally published in 1978. The Princeton Legacy Library uses the latest print-on-demand technology to again make available previously out-of-print books from the distinguished backlist of Princeton University Press. These paperback editions preserve the original texts of these important books while presenting them in durable paperback editions. The goal of the Princeton Legacy Library is to vastly increase access to the rich scholarly heritage found in the thousands of books published by Princeton University Press since its founding in 1905. (shrink)

The foundations of mathematics are divided into proof theory and set theory. Proof theory tries to justify the world of infinite mind from the standpoint of finite mind. Set theory tries to know more and more of the world of the infinite mind. The development of two subjects are discussed including a new proof of the accessibility of ordinal diagrams. Finally the world of large cardinals appears when we go slightly beyond girard's categorical approach to proof theory.

In 1963, the first author introduced a course in set theory at the University of Illinois whose main objectives were to cover Godel's work on the con sistency of the Axiom of Choice (AC) and the Generalized Continuum Hypothesis (GCH), and Cohen's work on the independence of the AC and the GCH. Notes taken in 1963 by the second author were taught by him in 1966, revised extensively, and are presented here as an introduction to axiomatic set theory. Texts in (...) set theory frequently develop the subject rapidly moving from key result to key result and suppressing many details. Advocates of the fast development claim at least two advantages. First, key results are high lighted, and second, the student who wishes to master the subject is com pelled to develop the detail on his own. However, an instructor using a "fast development" text must devote much class time to assisting his students in their efforts to bridge gaps in the text. (shrink)

A Frege proof systemFis any standard system of prepositional calculus, e.g., a Hilbert style system based on finitely many axiom schemes and inference rules. An Extended Frege systemEFis obtained fromFas follows. AnEF-sequence is a sequence of formulas ψ1, …, ψκsuch that eachψiis either an axiom ofF, inferred from previous ψuand ψv by modus ponens or of the formq↔ φ, whereqis an atom occurring neither in φ nor in any of ψ1,…,ψi−1. Suchq↔ φ, is called an extension axiom andqa new extension (...) atom. AnEF-proof is anyEF-sequence whose last formula does not contain any extension atom. In [12], S. A. Cook and R. Reckhow proved that the pigeonhole principlePHPhas a simple polynomial sizeEF-proof and conjectured thatPHPdoes not admit polynomial sizeF-proof. In [5], S. R. Buss refuted this conjecture by furnishing polynomial sizeF-proof forPHP. Since then the important separation problem of polynomial sizeFand polynomial sizeEFhas not shown any progress.In [11], S. A. Cook introduced the systemPV, a free variable equational logic whose provable functional equalities are ‘polynomial time verifiable’ and showed that the metamathematics ofFandEFcan be developed inPVand the soundness ofEFproved inPV. In [3], S. R. Buss introduced the first order systemand showed thatis essentially a conservative extension ofPV. There he also introduced a second order system. (shrink)

A Frege proof systemFis any standard system of prepositional calculus, e.g., a Hilbert style system based on finitely many axiom schemes and inference rules. An Extended Frege systemEFis obtained fromFas follows. AnEF-sequence is a sequence of formulas ψ1, …, ψκsuch that eachψiis either an axiom ofF, inferred from previous ψuand ψv by modus ponens or of the formq↔ φ, whereqis an atom occurring neither in φ nor in any of ψ1,…,ψi−1. Suchq↔ φ, is called an extension axiom andqa new extension (...) atom. AnEF-proof is anyEF-sequence whose last formula does not contain any extension atom. In [12], S. A. Cook and R. Reckhow proved that the pigeonhole principlePHPhas a simple polynomial sizeEF-proof and conjectured thatPHPdoes not admit polynomial sizeF-proof. In [5], S. R. Buss refuted this conjecture by furnishing polynomial sizeF-proof forPHP. Since then the important separation problem of polynomial sizeFand polynomial sizeEFhas not shown any progress.In [11], S. A. Cook introduced the systemPV, a free variable equational logic whose provable functional equalities are ‘polynomial time verifiable’ and showed that the metamathematics ofFandEFcan be developed inPVand the soundness ofEFproved inPV. In [3], S. R. Buss introduced the first order systemand showed thatis essentially a conservative extension ofPV. There he also introduced a second order system. (shrink)