A system of finite mathematics is proposed that has all of the power of classical mathematics. I believe that finite mathematics is not committed to any form of infinity, actual or potential, either within its theories or in the metalanguage employed to specify them. I show in detail that its commitments to the infinite are no stronger than those of primitive recursive arithmetic. The finite mathematics of sets is comprehensible and usable on its own terms, without appeal to any form (...) of the infinite. That makes it possible to, without circularity, obtain the axioms of full Zermelo-Fraenkel Set Theory with the Axiom of Choice (ZFC) by extrapolating (in a precisely defined technical sense) from natural principles concerning finite sets, including indefinitely large ones. The existence of such a method of extrapolation makes it possible to give a comparatively direct account of how we obtain knowledge of the mathematical infinite. The starting point for finite mathematics is Mycielski's work on locally finite theories. (shrink)

I consider here several versions of finitism or conceptions that try to work around postulating sets of infinite size. Restricting oneself to the so-called potential infinite seems to rest either on temporal readings of infinity (or infinite series) or on anti-realistic background assumptions. Both these motivations may be considered problematic. Quine’s virtual set theory points out where strong assumptions of infinity enter into number theory, but is implicitly committed to infinity anyway. The approaches centring on the indefinitely large and the (...) use of schemata would provide a work-around to circumvent usage of actual infinities if we had a clear understanding of how schemata work and where to draw the conceptual line between the indefinitely large and the infinite. Neither of this seems to be clear enough. Versions of strict finitism in contrast provide a clear picture of a (realistic) finite number theory. One can recapture standard arithmetic without being committed to actual infinities. The major problem of them is their usage of a paraconsistent logic with an accompanying theory of inconsistent objects. If we are, however, already using a paraconsistent approach for other reasons (in semantics, epistemology or set theory), we get finitism for free. This strengthens the case for paraconsistency. (shrink)

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

A critique of Shaughan Lavine's attempt in /Understanding the Infinite/ to reduce talk about the infinite to finitely comprehensible terms.

The nominalistic ontology of Kotarbinski, Slupecki and Tarski does not provide any direct interpretations of the sets of higher types which play important roles in type theory and in set theory. For this and other reasons I will interpret those theories as descriptions of some finite structures which are actually constructed in human imaginations and stored in their memories. Those structures will be described in this lecture. They are hinted by the idea of Skolem functions and Hilbert's -symbols, and they (...) constitute a finitistic modification of Tarski's concept of a model. They suggest also a form of the evolutionary process which leads to the development of human intelligence and language. (shrink)

Ratajczyk, Z., Subsystems of true arithmetic and hierarchies of functions, Annals of Pure and Applied Logic 64 95–152. The combinatorial method coming from the study of combinatorial sentences independent of PA is developed. Basing on this method we present the detailed analysis of provably recursive functions associated with higher levels of transfinite induction, I, and analyze combinatorial sentences independent of I. Our treatment of combinatorial sentences differs from the one given by McAloon [18] and gives more natural sentences. The same (...) method give also a combinatorial technique with no use of the cut-elimination theorem which is appropriate to study proof-theoretic strength of subsystems of first order arithmetic and some of their expansions. It was used to analyze iterated reflection principle and system of transfinite induction with a satisfaction class. (shrink)