Alternative Arithmetics

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.

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.

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.