Fragments of First and Second-Order Arithmetic and Length of Proofs

Dissertation, University of California, Berkeley (1990)
  Copy   BIBTEX

Abstract

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).$$

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,897

External links

  • This entry has no external links. Add one.
Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Analytics

Added to PP
2015-02-07

Downloads
0

6 months
0

Historical graph of downloads

Sorry, there are not enough data points to plot this chart.
How can I increase my downloads?

Citations of this work

Formalizing forcing arguments in subsystems of second-order arithmetic.Jeremy Avigad - 1996 - Annals of Pure and Applied Logic 82 (2):165-191.

Add more citations

References found in this work

No references found.

Add more references