The main objective of this thesis is to give an analysis of certain forms of the view in the Philosophy of Mathematics usually called Mathematical Instrumentalism. For this purpose we obtain the following technical results relevant for our philosophical arguments. ; The proofs of variable free equations involving primitive recursive functions in $I\Sigma\sb1$ are much shorter than the proofs of the same equations in the Primitive Recursive Arithmetic. More precisely, we show that $I\Sigma\sb1$ has a non-elementary speed-up over the Primitive (...) Recursive Arithmetic. ; $RCA\sb0$ has no significant speed-up over $I\Sigma\sb1$. ;These results are relevant to how useful some mathematical instruments are, and we use them to show that certain forms of the instrumentalist view are not tenable. ;The second part of the thesis deals with the main concern of an instrumentalist, the consistency proof. We show that a proposal for proving the consistency of theories put forward by M. Detlefsen is not viable as originally formulated, but that a variant of it leads to a partial program, not justifiable on purely finitistic grounds. We also discuss a suggestion of Godel to replace the consistency proofs by "practical reductions". We show that while his original proposal is related to some open questions in Complexity Theory, a philosophically more acceptable form of it has a very limited potential. The relevant technical results for the second part of the thesis are the following ones. ; If T is a theory extending PRA, then $PRA\vdash Con \leftrightarrow Con$ iff there exists a primitive recursive function f such that $PRA \vdash\forall xPrf\sb{PRA}$, $\lceil\neg Prf\sb{T}\rceil).$ ; $PRA\vdash\forall x)Prf\sb{PRA}\rceil).$ ; For all natural numbers n the following incompleteness results holds:$$PRA\not\vdash\forall x\exists y <2\sbsp{\ \ n}{2\quad\sp{x}} Prf\sb{PRA}\rceil).$$. (shrink)

Let CKDT be the assertion that for every countably infinite bipartite graph G, there exist a vertex covering C of G and a matching M in G such that C consists of exactly one vertex from each edge in M. (This is a theorem of Podewski and Steffens [12].) Let ATR0 be the subsystem of second-order arithmetic with arithmetical transfinite recursion and restricted induction. Let RCA0 be the subsystem of second-order arithmetic with recursive comprehension and restricted induction. We show that (...) CKDT is provable in ART0. Combining this with a result of Aharoni, Magidor, and Shore [2], we see that CKDT is logically equivalent to the axioms of ATR0, the equivalence being provable in RCA0. (shrink)

Herbrand's Theorem, in the form of $$\underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{\exists } $$ -inversion lemmata for finitary and infinitary sequent calculi, is the crucial tool for the determination of the provably total function(al)s of a variety of theories. The theories are (second order extensions of) fragments of classical arithmetic; the classes of provably total functions include the elements of the Polynomial Hierarchy, the Grzegorczyk Hierarchy, and the extended Grzegorczyk Hierarchy $\mathfrak{E}^\alpha $ , α < ε0. A subsidiary aim of the paper is to show (...) that the proof theoretic methods used here are distinguished by technical elegance, conceptual clarity, and wide-ranging applicability. (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)