First published in 1974. Despite the tendency of contemporary analytic philosophy to put logic and mathematics at a central position, the author argues it failed to appreciate or account for their rich content. Through discussions of such mathematical concepts as number, the continuum, set, proof and mechanical procedure, the author provides an introduction to the philosophy of mathematics and an internal criticism of the then current academic philosophy. The material presented is also an illustration of a new, more general method (...) of approach called substantial factualism which the author asserts allows for the development of a more comprehensive philosophical position by not trivialising or distorting substantial facts of human knowledge. (shrink)

We establish by elementary proof-theoretic means the conservativeness of two subsystems of analysis over primitive recursive arithmetic. The one subsystem was introduced by Friedman [6], the other is a strengthened version of a theory of Minc [14]; each has been shown to be of considerable interest for both mathematical practice and metamathematical investigations. The foundational significance of such conservation results is clear: they provide a direct finitist justification of the part of mathematical practice formalizable in these subsystems. The results are (...) generalized to relate a hierarchy of subsystems, all contained in the theory of arithmetic properties, to a corresponding hierarchy of fragments of arithmetic. The proof theoretic tools employed there are used to re-establish in a uniform, elementary way relationships between various fragments of arithmetic due to Parsons, Paris and Kirby, and Friedman. (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)

KPM is a subsystem of set theory designed to formalize a recursively Mahlo universe of sets. In this paper we show that a certain ordinal notation system is sufficient to measure the proof-theoretic strength ofKPM. This involves a detour through an infinitary calculus RS(M), for which we prove several cutelimination theorems. Full cut-elimination is available for derivations of $\Sigma (L_{\omega _1^c } )$ sentences, whereω 1 c denotes the least nonrecursive ordinal. This paper is self-contained, at least from a technical (...) point of view. (shrink)

Die Leitgedanken meiner Untersuchungen über die Grundlagen der Mathematik, die ich - anknüpfend an frühere Ansätze - seit 1917 in Besprechungen mit P. BERNAYS wieder aufgenommen habe, sind von mir an verschiedenen Stellen eingehend dargelegt worden. Diesen Untersuchungen, an denen auch W. ACKERMANN beteiligt ist, haben sich seither noch verschiedene Mathematiker angeschlossen. Der hier in seinem ersten Teil vorliegende, von BERNAYS abgefaßte und noch fortzusetzende Lehrgang bezweckt eine Darstellung der Theorie nach ihren heutigen Ergebnissen. Dieser Ergebnisstand weist zugleich die Richtung (...) für die weitere Forschung in der Beweistheorie auf das Endziel hin, unsere üblichen Methoden der Mathematik samt und sonders als widerspruchsfrei zu erkennen. Im Hinblick auf dieses Ziel möchte ich hervorheben, daß die zeit weilig aufgekommene Meinung, aus gewissen neueren Ergebnissen von GÖDEL folge die Undurchführbarkeit meiner Beweistheorie, als irrtüm lich erwiesen ist. Jenes Ergebnis zeigt in der Tat auch nur, daß man für die weitergehenden Widerspruchsfreiheitsbeweise den finiten Stand punkt in einer schärferen Weise ausnutzen muß, als dieses bei der Be trachtung der elementaren Formallsmen erforderlich ist. Göttingen, im März 1934 HILBERT Vorwort zur ersten Auflage Eine Darstellung der Beweistheorie, welche aus dem HILBERTschen Ansatz zur Behandlung der mathematisch-logischen Grundlagenpro bleme erwachsen ist, wurde schon seit längerem von HILBERT ange kündigt. (shrink)

This paper is divided into two parts. Part I provides a resumé of the evolution of the notion of predicativity. Part II describes our own work on the subject.Part I§1. Conceptions of sets.Statements about sets lie at the heart of most modern attempts to systematize all (or, at least, all known) mathematics. Technical and philosophical discussions concerning such systematizations and the underlying conceptions have thus occupied a considerable portion of the literature on the foundations of mathematics.

Does science justify any part of mathematics and, if so, what part? These questions are related to the so-called indispensability arguments propounded, among others, by Quine and Putnam; moreover, both were led to accept significant portions of set theory on that basis. However, set theory rests on a strong form of Platonic realism which has been variously criticized as a foundation of mathematics and is at odds with scientific realism. Recent logical results show that it is possible to directly formalize (...) almost all, if not all, scientifically applicable mathematics in a formal system that is justified simply by Peano Arithmetic (via a proof-theoretical reduction). It is argued that this substantially vitiates the indispensability arguments. (shrink)

A notion of finitary inductively presented (f.i.p.) logic is proposed here, which includes all syntactically described logics (formal systems)met in practice. A f.i.p. theory FS0 is set up which is universal for all f.i.p. logics; though formulated as a theory of functions and classes of expressions, FS0 is a conservative extension of PRA. The aims of this work are (i)conceptual, (ii)pedagogical and (iii)practical. The system FS0 serves under (i)and (ii)as a theoretical framework for the formalization of metamathematics. The general approach (...) may be used under (iii)for the computer implementation of logics. In all cases, the work aims to make the details manageable in a natural and direct way. (shrink)