Alternative Arithmetics

Question

Although, beyond any doubts, $ZFC$ is by and large the predominantly accepted theory of sets, there have been a few attempt to establish some serious competitors in town.

I just quote two of them (there are several more): $NF$ by Quine and Alternative Set Theory by Petr Vopenka. I think those attempts are epistemologically interesting, in that they open doors to quite different views about the world of sets and how we conceptualize them (and therefore on the entire cathedral of mathematics grounded in set theory).

Now, here is my question: is there something like it in formal arithmetics?

Are there Alternative Formal Arithmetical theories?

I do NOT mean the various fragments of arithmetics, which essentially start from Robinson Arithmetics $Q$ (or even Pressburger's Arithmetics) and then consider some limitation of the infamous Induction Rule (IOpen, $I\Delta_0$, $I\Sigma_n$, etc.). All those share the common denominator $N$, and of course they differ in the "nonstandard models", as well as their proof theoretical strength.

I mean some formal systems of numbers which substantially move away from the traditional picture of $N$, all the while retaining some basic intuition of counting, ordering, arithmetical operations.

To give you an idea of what I am after: systems in which it is not true that all numbers have a successor, or it is not always true that $Sn\succ n$, or one in which the ordering of natural numbers is not linear or even not total, or an arithmetical first order theory whose intended model are the countable ordinals.

Or perhaps even wildest animals.

Answer 1

Recall that $NFU$ is the Quine-Jensen system of set theory with a universal set; it is based on weakening the extensionality axiom of Quine's $NF$ so as to allow urelements.

Let $NFU^-$ be $NFU$ plus "every set is finite". As shown by Jensen (1969), $NFU^-$ is consistent relative to $PA$ (Peano arithmetic). $NFU^-$ provides a radically different "picture" of finite sets and numbers, since there is a universal set and therefore a last finite cardinal number in this theory.

The following summarizes our current knowedge of $NFU^-$.

1. [Solovay, unpublished]. $NFU^-$and $EFA$ (exponential function arithmetic) are equiconsistent. Moreover, this equiconsistency can be vertified in $SEFA$ (superexponential function arithmetic), but $EFA$ cannot verify that Con($EFA$) implies Con($NFU^-$). It can verify the other half of the equiconsistency.

2. [Joint result of Solovay and myself]. $PA$ is equiconsistent with the strengthening of $NFU^-$ obtained by adding the statement that expresses "every Cantorian set is strongly Cantorian". Again, this equiconsistency can be verified in $SEFA$, but not in $EFA$.

3. [My result]. There is a "natural" extension of $NFU^-$ that is equiconistent with second order arithmetic $\sf Z_2$.

For more detail and references, you can consult the following paper:

A. Enayat. From Bounded Arithmetic to Second Order Arithmetic via Automorphisms, in Logic in Tehran, Lecture Notes in Logic, vol. 26, Association for Symbolic Logic, 2006.

A preprint can be found here.

Answer 2

You are (implicitly) limiting yourself to classical logic, I think. If you are willing to let go of classical logic, then your options are much wider and many more interesting phenomena arise.

One example in which (higher-order) arithmetic behaves differently from what classical mathematicians are used to is the effective topos. It is a model of intuitionistic higher-order arithmetic in which, for example:

1. There are countably many countable subsets of $\mathbb{N}$.
2. All maps $\mathbb{N}^\mathbb{N} \to \mathbb{N}$ are continuous, where $\mathbb{N}^\mathbb{N}$ is the Baire space, equipped with a complete metric.
3. There is an infinite binary tree in which every path is finite (this is essentially Kleene's tree and is a direct violation of Koenig's Lemma).
4. There is a subset $T \subseteq \mathbb{N}$ and a surjection from $T$ onto $\mathbb{N}^\mathbb{N}$.

This is just one example of an "alternative" mathematical world. Anther important one is synthetic differential geometry in which nilpotent infinitesimals exist. (And you probably know about the non-standard models constructed as ultrapowers, but those do not give you nilpotent infinitesimals.)

I have devoted some time to being able to think "natively" as if I were inside the effective topos. It takes some effort because in the beginning one has to constantly check one's intuition by computing things "from the outside". But eventually, when one does get used to the new world, it is like visiting a different planet (not that I have ever been to one, Ij just watched Avatar and Star Wars): bizarre and beautiful at the same time. At least for me, the lesson learned is that the "ZFC cathedral" is just one among many.

Answer 3

Since you mentioned Vopenka's Alternative Set Theory, you probably already know that it provides an unusual picture of the natural numbers, in which some but not all the numbers are finite. The natural numbers are, as usual, the smallest set containing 0 and closed under successor, but that set properly includes the class of finite natural numbers, the smallest class containing 0 and closed under successor. (A key feature of the Alternative Set Theory is that subclasses of sets need not be sets.)

You might want to be more specific about your stipulation that you want theories "retaining some basic intuition of counting, ordering, and arithmetical operations" yet moving away from the traditional picture of $N$. As it stands, this seems to allow the theory of real-closed fields (also describable as the set of all first-order sentences true in the ordered field of real numbers). Admittedly, it has counting only in the rather weak sense of having 0 and the operation of adding 1, but that seems to suffice for a "basic intuition". I suspect this sort of example, replacing $N$ by the real line, isn't what you intended.

Finally, it seems worth mentioning that some of the "bounded arithmetic" theories that you don't want provide a distinction between "small" and "large" natural numbers, roughly reminiscent of what you get in the Alternative Set Theory (though I don't know any rigorous connection between the two). Any theory of natural numbers in which exponentiation is not provably total lets you distinguish between the small numbers, those $n$ for which $2^n$ exists, and the larger numbers that can't be exponentiated.

Answer 4

Two systems in which the successor operation is altered are Sazonov's arithmetic over a finite row, in "A logical approach to the problem 'P=NP?'" http://www.csc.liv.ac.uk/~sazonov/papers.html and Boucher's "Arithmetic without the Successor Axiom", http://www.andrewboucher.com/papers/.

In Sazonov's system, there is a total successor operation that is explicitly assumed to stop at the last number $\square+1 = \square$, whereas in Boucher's system the successor relation is just not assumed to be total.

Then there are ways to designate numbers up to $2^\square$ via binary strings or second-order variables. Because of course even though we can't feasibly reach, say, $2^{1000}$ starting from zero and repeatedly adding one, computers manipulate binary representations of numbers of that order and larger all the time, and we should be able to prove theorems about these representations.

But if you don't like restrictions on induction, there's a problem. With unrestricted induction even up to $\square$, it seems we just define a second-order zero and successor, and derive unrestricted induction up to $2^\square$. Now if, from $P(0)$ and $\forall n . P(n) \to P(n+1)$, you conclude, $P(2^{1000})$, then you're admitting that, in principle, you can reach $2^{1000}$ from zero by repeatedly adding one.

Which lets me segue to an idea that I had. Caveat lector.

Start with cyclic induction: if $\exists n. P(n)$ and $\forall n . P(n) \to P(S(n))$ then $\forall n. P(n)$. If $X$ and $Y$ are types with unrestricted cyclic induction, then $X^Y$ (the type of all functions from $Y$ to $X$) has unrestricted cyclic induction. And of course unrestricted cyclic induction is valid for a two-element domain. So this suggests the theory of finite-order types over 2 (something like $\mathbf{HA}^\omega$, the constructive theory of finite-order types over $\mathbb{N}$.)

One way this may be of interest is that, as Theo Johnson-Freyd mentions, computers generally work with a cyclic domain like $2^{32} = (2^{2^{2^2}})^2$. They can also work with larger integer size. And in fact there are "big integer" implementations which are sometimes said to work with arbitrary integers. And I notice someone claims above that the C programming model has infinite memory! But that's sort of an insult to $\mathbb{N}$. If they are implemented with, say, 32-bit pointers, then your big integer type really has a size approximately $2^{2^{32}}$ - even if your computer has more than 4GB of memory you can't use it. Taking this even further, if you can imagine a computer with a truly vast address space, which has to be accessed using "big pointers" made from small 32-bit pointers, and then defining "really big integers" over that, well, that's still just a finite type of something like $2^{2^{2^{32}}}$.

From the other side, you can accept a truly arbitrary integer with an interactive spefication, but you're really dealing with something like the one-point compactification of $\mathbb{N}$. There doesn't seem to be a way to express the specification that the input stream must terminate "eventually" without cutting it off at a large but finite bound, or circularly referring to $\mathbb{N}$.

Another way this may be of interest is that instead of talking of the "finite" types over 2 in terms of a meta-theory involving $\mathbb{N}$, we can then use it as its own meta-theory, so we're dealing with a large but finite set of formulas. That should be a viable proof theory.

Of course this alternative arithmetic may suit a finitist, but you're an ultrafinitist and this is not what you really want. I think what you really want doesn't exist: as I've ranted elsewhere it seems we need induction up to infeasible numbers to prove theorems about feasible computations.

Answer 5

I mean my answer to be only partly tongue-in-cheek.

Many modern computers / computer languages have robust built-in implementations of arithmetic. Actually, most have a number of different kinds of arithmetic, but one of them is a particularly central and basic notion of "number" used for counting. For this central implementation of arithmetic, the computer has (hard-coded) a precise finite number of "numbers". $2^{32}$ is standard, if memory serves --- in any case, it's small enough that personal computers can fairly easily run through all of them and create complete look-up tables for many functions. Indeed, it is important to keep in mind that certain types of numbers are in finite supply when writing algorithms, as it means that many algorithms run not in exponential or even polynomial time, but actually in bounded time (and with look-up tables you can often make that time quite low).