This paper presents proof that Buss's S22 can prove the consistency of a fragment of Cook and Urquhart's PV from which induction has been removed but substitution has been retained. This result improves Beckmann's result, which proves the consistency of such a system without substitution in bounded arithmetic S12. Our proof relies on the notion of "computation" of the terms of PV. In our work, we first prove that, in the system under consideration, if an equation is proved (...) and either its left- or right-hand side is computed, then there is a corresponding computation for its right- or left-hand side, respectively. By carefully computing the bound of the size of the computation, the proof of this theorem inside a bounded arithmetic is obtained, from which the consistency of the system is readily proven. This result apparently implies the separation of bounded arithmetic because Buss and Ignjatović stated that it is not possible to prove the consistency of a fragment of PV without induction but with substitution in Buss's S12. However, their proof actually shows that it is not possible to prove the consistency of the system, which is obtained by the addition of propositional logic and other axioms to a system such as ours. On the other hand, the system that we have considered is strictly equational, which is a property on which our proof relies. (shrink)

Partial consistency statements can be expressed as polynomial-size propositional formulas. Frege proof systems have polynomial-size partial self-consistency proofs. Frege proof systems have polynomial-size proofs of partial consistency of extended Frege proof systems if and only if Frege proof systems polynomially simulate extended Frege proof systems. We give a new proof of Reckhow's theorem that any two Frege proof systems p-simulate each other. The proofs depend on polynomial size propositional formulas defining the truth of propositional (...) formulas. These are already known to exist since the Boolean formula value problem is in alternating logarithmic time; this paper presents a proof of this fact based on a construction which is somewhat simpler than the prior proofs of Buss and of Buss-Cook- Gupta-Ramachandran. (shrink)

In 5, Tait identifies a set of reflection principles called equation image-reflection principles which Peter Koellner has shown to be consistent relative to the existence of κ, the first ω-Erdős cardinal 1. Tait also defines a set of reflection principles called equation image-reflection principles; however, Koellner has shown that these are inconsistent when m > 2, but identifies restricted versions of them which he proves consistent relative to κ 2. In this paper, we introduce a new large-cardinal property, the α-reflective (...) cardinals. Their definition is motivated by Tait's remarks on parameters of third or higher order in reflection principles. We prove that if κ is ℶκ + α + 1-supercompact and 0 < α < κ then κ is α-reflective. Furthermore we show that α-reflective cardinals relativize to L, and that if κ exists then the set of cardinals λ < κ, such that λ is α-reflective for all α such that 0 < α < λ, is a stationary subset of κ. We show that an ω-reflective cardinal satisfies some restricted versions of equation image-reflection, as well as all the reflection properties proved consistent in 2. (shrink)

We give a consistency proof within a weak fragment of arithmetic of elementary algebra and geometry. For this purpose, we use EFA (exponential function arithmetic), and various first order theories of algebraically closed fields and real closed fields.

We show that the consistency of the first order arithmetic $PA$ follows from the pointwise induction up to the Howard ordinal. Our proof differs from U. Schmerl [Sc]: We do not need Girard's Hierarchy Comparison Theorem. A modification on the ordinal assignment to proofs by Gentzen and Takeuti [T] is made so that one step reduction on proofs exactly corresponds to the stepping down $\alpha\mapsto\alpha [1]$ in ordinals. Also a generalization to theories $ID_q$ of finitely iterated inductive (...) definitions is proved. (shrink)

LetCbe an axiom system formalized within the first order functional calculus, and letC′ be related toCas the Bernays-Gödel set theory is related to the Zermelo-Fraenkel set theory. Ilse Novak [5] and Mostowski [8] have shown that, ifCis consistent, thenC′ is consistent. Mostowski has also proved the stronger result that any theorem ofC′ which can be formalized inCis a theorem ofC.The proofs of Novak and Mostowski do not provide a direct method for obtaining a contradiction inCfrom a contradiction inC′. We (...) could, of course, obtain such a contradiction by proving the theorems ofCone by one; the above result assures us that we must eventually obtain a contradiction. A similar process is necessary to obtain the proof of a theorem inCfrom its proof inC′. The purpose of this paper is to give a new proof of these theorems which provides a direct method of obtaining the desired contradiction or proof.The advantage of the proof may be stated more specifically by arithmetizing the syntax ofCandC′. (shrink)

This paper gives a Gentzen-style proof of the consistency of Heyting arithmetic in an intuitionistic sequent calculus with explicit rules of weakening, contraction and cut. The reductions of the proof, which transform derivations of a contradiction into less complex derivations, are based on a method for direct cut-elimination without the use of multicut. This method treats contractions by tracing up from contracted cut formulas to the places in the derivation where each occurrence was first introduced. Thereby, Gentzen’s heightline argument, (...) which introduces additional cuts on contracted compound cut formulas, is avoided. To show termination of the reduction procedure an ordinal assignment based on techniques of Howard for Gödel’s T is used. (shrink)

An Introduction to Proof Theory provides an accessible introduction to the theory of proofs, with details of proofs worked out and examples and exercises to aid the reader's understanding. It also serves as a companion to reading the original pathbreaking articles by Gerhard Gentzen. The first half covers topics in structural proof theory, including the Gödel-Gentzen translation of classical into intuitionistic logic, natural deduction and the normalization theorems, the sequent calculus, including cut-elimination and mid-sequent theorems, and various applications (...) of these results. The second half examines ordinal proof theory, specifically Gentzen's consistency proof for first-order Peano Arithmetic. The theory of ordinal notations and other elements of ordinal theory are developed from scratch, and no knowledge of set theory is presumed. The proof methods needed to establish proof-theoretic results, especially proof by induction, are introduced in stages throughout the text. Mancosu, Galvan, and Zach's introduction will provide a solid foundation for those looking to understand this central area of mathematical logic and the philosophy of mathematics. (shrink)

In this paper, I will argue from a historical perspective that Gentzen’s 1935 consistency proof of 1st order Peano Arithmetic PA principally aimed to give a finitist interpretation of implication and this aspect of the 1935 proof emerged as the attempt to cope with the non-finiteness in BHK-interpretation of implication. My argument consists of two parts. First, I will explain that the fundamental idea of the 1935 proof is to show the soundness of PA on some finitist interpretation and (...) Gentzen had attempted to use BHK-interpretation as such an interpretation. It is claimed that he eventually thought that there is a ‘circularity’ which is due to the non-finiteness of BHK-interpretation of implication, so it cannot be used as a finitist interpretation. Secondly, I will argue that the principal aim of the 1935 proof is to give his own finitist interpretation of implication which avoids such a ‘circularity’. Finally, this paper’s conclusion and an open question are presented. (shrink)

After a brief flirtation with logicism around 1917, David Hilbertproposed his own program in the foundations of mathematics in 1920 and developed it, in concert with collaborators such as Paul Bernays andWilhelm Ackermann, throughout the 1920s. The two technical pillars of the project were the development of axiomatic systems for everstronger and more comprehensive areas of mathematics, and finitisticproofs of consistency of these systems. Early advances in these areaswere made by Hilbert (and Bernays) in a series of lecture courses (...) atthe University of Göttingen between 1917 and 1923, and notably in Ackermann's dissertation of 1924. The main innovation was theinvention of the -calculus, on which Hilbert's axiom systemswere based, and the development of the -substitution methodas a basis for consistency proofs. The paper traces the developmentof the ``simultaneous development of logic and mathematics'' throughthe -notation and provides an analysis of Ackermann'sconsistency proofs for primitive recursive arithmetic and for thefirst comprehensive mathematical system, the latter using thesubstitution method. It is striking that these proofs use transfiniteinduction not dissimilar to that used in Gentzen's later consistencyproof as well as non-primitive recursive definitions, and that thesemethods were accepted as finitistic at the time. (shrink)

A loose analogy relates the work of Laplace and Hilbert. These thinkers had roughly similar objectives. At a time when so much of our analytic effort goes to distinguishing mathematics and logic from physical theory, such an analogy can still be instructive, even though differences will always divide endeavors such as those of Laplace and Hilbert.

To appear in the Proceedings of Logic Colloquium 2006. (28 pages).

We have seen that despite Feferman's results Gödel's second theorem vitiates the use of Hilbert-type epistemological programs and consistency proofs as a response to mathematical skepticism. Thus consistency proofs fail to have the philosophical significance often attributed to them.This does not mean that consistency proofs are of no interest to philosophers. We know that a ‘non-pathological’ consistency proof for a system S will use methods which are not available in S. When S is (...) as strong a system as we are willing to entertain seriously then a consistency proof for it will yield no epistemological gain. But in other cases philosophers might argue that the proof uses methods which are merely different rather than stronger than those available in the system in question. This claim has been made, for example, in the case of the constructive consistency proofs for elementary number theory. Similar philosophical investigations can be made on relative consistency proofs, since these differ from each other in the principles they employ. For example, most relative consistency proofs can be carried out within elementary number theory, but without using the theory of real numbers, no one has been able to prove the consistency of Quine's ML relative to that of his NF.What about the consistency of all mathematics or of some strong system for set theory? How do we answer the skeptic? Since here a convincing proof is not possible, we have established that the skeptic demands too much. We cannot be certain that our axioms are free from contradiction and must treat them as hypotheses which may be abandoned or modified in the face of further mathematical experience. This attitude is taken by many foundational workers who also go on to voice opinions about thelikelihood that various systems are consistent. Since these opinions are variously supported by appeals to the clarity of the mathematical concept formalized, the existence or non-existence of ‘weird’ models for the system and actual empirical experience with the system, this is surely a fruitful area for philosophical research. (shrink)

In the 1920s, Ackermann and von Neumann, in pursuit of Hilbert's programme, were working on consistency proofs for arithmetical systems. One proposed method of giving such proofs is Hilbert's epsilon-substitution method. There was, however, a second approach which was not reflected in the publications of the Hilbert school in the 1920s, and which is a direct precursor of Hilbert's first epsilon theorem and a certain "general consistency result" due to Bernays. An analysis of the form of (...) this so-called "failed proof" sheds further light on an interpretation of Hilbert's programme as an instrumentalist enterprise with the aim of showing that whenever a "real" proposition can be proved by ?ideal? means, it can also be proved by "real", finitary means. (shrink)

The last section of “Lecture at Zilsel’s” [9, §4] contains an interesting but quite condensed discussion of Gentzen’s first version of his consistency proof for P A [8], reformulating it as what has come to be called the no-counterexample interpretation. I will describe Gentzen’s result (in game-theoretic terms), fill in the details (with some corrections) of Godel's reformulation, and discuss the relation between the two proofs.

We introduce a nonstandard arithmetic $NQA^-$ based on the theory developed by R. Chuaqui and P. Suppes in [2] (we will denote it by $NQA^+$ ), with a weakened external open minimization schema. A finitary consistency proof for $NQA^-$ formalizable in PRA is presented. We also show interesting facts about the strength of the theories $NQA^-$ and $NQA^+$ ; $NQA^-$ is mutually interpretable with $I\Delta_0 + EXP$ , and on the other hand, $NQA^+$ interprets the theories IΣ1 and $WKL_0$.

Gentzen's three consistency proofs for elementary number theory have a common aim that originates from Hilbert's Program, namely, the aim to justify the application of classical reasoning to quantified propositions in elementary number theory. In addition to this common aim, Gentzen gave a “finitist” interpretation to every number-theoretic proposition with his 1935 and 1936 consistency proofs. In the present paper, we investigate the relationship of this interpretation with intuitionism in terms of the debate between the Hilbert (...) School and the Brouwer School over the significance of consistency proofs. First, we argue that the interpretation had the role of responding to a Brouwer-style objection against the significance of consistency proofs. Second, we propose a way of understanding Gentzen's response to this objection from an intuitionist perspective. (shrink)

I trace the development of arguments for the consistency of non-Euclidean geometries and for the independence of the parallel postulate, showing how the arguments become more rigorous as a formal conception of geometry is introduced. I analyze the kinds of arguments offered by Jules Hoüel in 1860-1870 for the unprovability of the parallel postulate and for the existence of non-Euclidean geometries, especially his reaction to the publication of Beltrami’s seminal papers, showing that Beltrami was much more concerned with the (...) existence of non-Euclidean objects than he was with the formal consistency of non-Euclidean geometries. The final step towards rigorous consistency proofs is taken in the 1880s by Henri Poincaré. It is the formal conception of geometry, stripping the geometric primitive terms of their usual meanings, that allows the introduction of a modern fully rigorous consistency proof. (shrink)

In treatises or advanced textbooks on theoretical physics, it is apparent that the way mathematics is used is very different from what is to be found in books of mathematics. There is, for example, no close connection between books on analysis, on the one hand, and any classical textbook in quantum mechanics, for example, Schiff, [11], or quite recent books, for example Ryder, [10], on quantum field theory. The differences run a good deal deeper than the fact that the books (...) on theoretical physics are not written in the definition-theorem-proof style characteristic of pure mathematics. Although a good many propositions are proved in the books on physics, there are almost with exception no existential proofs, and consequently there is no really serious systematic use of quantifiers. Another important characteristic is the free use of infinitesimals. In fact, most results would not lose anything, from a physicist's point of view, by leaving them in approximate form, i.e., instead of strict equalities or inequalities, using equalities or inequalities only up to an infinitesimal.The discrepancy between the way mathematics is ordinarily done in theoretical physics and the way it is built up from a foundational standpoint in any of the standard modern views raises the question of whether it might be possible to construct quite directly a rigorous foundation that reflects a significant part of this standard practice in theoretical physics. Other parts of standard practice in physics, for example, the use of physically intuitive but nonrigorous arguments, are not present in our system. (shrink)