Taking the Pirahã seriously

• We provide first order theories axiomatizing a bounded universe of finite or infinite natural numbers.
• The theories are undecidable, and consistent if Nelson’s predicative arithmetic is.
• In these theories some of the basic features of the theory of grossone can be proved.
• We can prove that each set has cardinality bigger than every proper subset.
• Every series converges, and is invariant under any rearrangement of its terms.

We propose first order formal theories ΓnΓn, with n⩾1n⩾1, and Γ=⋃n⩾1ΓnΓ=⋃n⩾1Γn, which can be roughly described as follows: each one of these theories axiomatizes a bounded universe, with a greatest element, modeled on Sergeyev’s so-called grossone; each such theory is consistent if predicative arithmetic IΔ0+Ω1IΔ0+Ω1 is; inside each such theory one can represent (in a weak, precisely specified, sense) the partial computable functions, and thus develop computability theory; each such theory is undecidable; the consistency of ΓnΓn implies the consistency of Γn∪{ConΓn}Γn∪{ConΓn}, where ConΓnConΓn “asserts” the consistency of ΓnΓn (this however does not conflict with Gödel’s Second Incompleteness Theorem); if n>1n>1, then there is a precise way in which we can say that ΓnΓn proves that each set has cardinality bigger than every proper subset, although two sets have the same cardinality if and only if they are bijective; if n>2n>2, inside ΓnΓn there is a precise sense in which we can talk about integers, rational numbers, and real numbers; in particular, we can develop some measure theory; we can show that every series converges, and is invariant under any rearrangement of its terms (at least, those series and those rearrangements we are allowed to talk about); we also give a basic example, showing that even transcendental functions can be approximated up to infinitesimals in our theories: this example seems to provide a general method to replace a significant part of the mathematics of the continuum by discrete mathematics.