The Recursive Finite Mathematics Program

Pauca sed matura. (Gauss)

It is curious how the following philosophical position of strict or bounded recursive finitism also called ultrafinitism (whose roots can be traced back to Gauss, Kant, Leibniz, Hume,  Proclus, Euclid, Aristotle, Plato and perhaps Chrysippus) has received little attention (apart from Bishop, Maddy and Alexander Yessenin-Volpin) within the broader context of finitism, constructivism and intuitionism. It is wrong to associate Kronecker's philosophically dogmatic and naive empiricist and materialist view of mathematics (never actually worked out, nor the concept of algorithm and computation elucidated) with philosophically and logically reflected finitism or ultrafinitism. Kronecker's views from the end of the 19th century - which had no relationship to the ideas of formal logic - were a crude perversion of the ideal of computability and finitude (which were, due to Kronecker's power and influence, historically harmful to the progress of mathematics) and they cannot be invoked as an anti-finitist argument. They also produced a harmful misconception that ultrafinitism is somehow connected to empiricism and naturalism. Also Kronecker's legitimate and correct focus on effective procedures in number theory is not original but was already, for instance,  at the heart of Gauss' methodology and philosophy, which in turn can be traced back to Euclid. The great names of finitism and the ideal of computability include (besides Maddy, Bishop and Yessenin-Volpin) Skolem, Hilbert, Brouwer, Church, Turing and Martin-Löf among many others. But far more historical research is called for.

We need to recognize the co-implicitness between logic, arithmetic and algorithms and that all mathematics must be subject to bounded finite and computable criteria and rules but at the same time recognize with Leibniz that the fictive imaginary non-finite entities in bounded finite theories, definitions and proofs can be reduced to actual bounded finite numerical computations. But this must not be confused with a pragmatic viewpoint such as as Weyl's in physics.  Because such a reduction with its associated computable elimination of fictive entity symbols,  has to be effective and transparent. The situation is quite different for physics in which even an experimental confirmation of theoretically predicated outcomes does not in the least rule out the radical revision or improvement of the theory in question as well as a healthy methodological skepticism.

The fictive freedom and realism of the birds adds to the perfection of their own finite bounded realization.

 

 1. All legitimate mathematical objects must be bounded, both "extensionally" and "intensionally" (i.e. with regards to their definition). Thus there are intensionally defined natural numbers which are too large to actually exist.

2. All logical expressions, proofs, rules, axioms and instantiations of rules and axioms must be have precise bounds on size.

3. All meaningful quantification must be finitely bounded and interpreted constructively. Constructivism gives us a meaningful way to interpret quantification. But linear logic and other subtstructual logics as well as paraconsistent logic also gives vital contributions. We must replace the exponentials !,? with their bounded finite versions. And the distinction between distributive and non-distributive (intensional) versions of linear version of the quantifiers (corresponding to additive and multiplicative connectives) is of great importance.

4. All valid mathematics must be given either by finite enumeration or finite (possible recursive) specification. Mathematical objects are algorithms (programs) specifiable within a finite bound (this must not be forgotten). One program can be seen as a type of another program. The finding of proofs or construction of proof-terms (with controlled resources) is analogous to assembling the traditional Chinese Luban puzzles.

5. All finite specifications and proofs must be able to be checked by a finite program (proof assistant and proof checker).

6. Valid mathematics corresponds to what can be formalized and checked by a (necessarily finite) proof checker. All valid mathematics must be able to be given direct, concrete, intuitive, operational-combinatorial justification and presentation.

7. The finite and recursive is boostrapping, meta-reflexive, self-referential and self-transcendent guided by regulative ideas (convenient fictions) and synthetic pure a priori principles. We can automatically check proof checkers themselves. But this hierarchy can itself only have finitely many levels. 

Even if a system is inconsistent in the usual sense, may it not have a finite fragment (conditioned by finite rule applications) which derives something coherent and meaningful? 

Finitism may solve the traditional problems of the foundations of analysis (cf. the undecidability of equality for the reals). We need a pure formal algebraic treatment of so-called "approximation",  numerical analysis and implementations of numerical computation. 

The above 7 propositions give rise to countless (but hopefully not exceeding the corresponding finite bounds!) philosophical, logical and mathematical problems, and possibilities of radical criticism of contemporary practices and ideas (we can question the usefulness of traditional complexity classes) - all of which we can only  begin to understand. 

Many-valued logics can be exemplified by a statistical or probabilistic logic based on finite data-sets. 

They permit an intimate fusion between computer science, logic, linguistics, mathematics, cognitive psychology and philosophy as well as art (is there a big difference between mathematical or computational elegance and efficiency and human aesthetic value?). 

"All men are mortal" means that there is an accepted finite process by which from the finite concept "man"  we can extract the finite concept "mortal".  Extensional, distributive readings are untenable. But what about the proposition: "If all A is B and all B is C then all A is C". The quantifiers can be interpreted as above, but what about this whole proposition which is quantified over "monadic predicates" A,B and C ? This gives us another legitimate interpretation of bounded universal quantification: as a postulated rule, an algorithm within finite bounds, i.e., a logical rule, a rule of inference.