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, 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 (which also did not produce any notable technical contributions to the finitist framework) with philosophically and logically reflected finitism or ultrafinitism. This has produced a harmful misconception that ultrafinitism is somehow connected to empiricism and naturalism. Its great names include Skolem, Hilbert, Brouwer, Turing and Martin-Löf.
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 is analogous to 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.
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.
