Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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.

share|improve this question
add comment

5 Answers 5

up vote 11 down vote accepted

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.

share|improve this answer
    
@Ali + @ Andreas GREAT!!! Yes, this is probably the starting point: looking at arithmetic from within an Alternative Set Theory. Ali, I will definitely look into your paper –  Mirco Mannucci Jun 3 '11 at 0:00
add comment

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.

share|improve this answer
    
Andrej, yes, but only here. I am sure you have not failed to realize that my question on the polytime subcategory of the effective topos is along similar lines, only there I do not limit myself to either classical logic or set theory as background. Now, back to your answer: yes, the effective topos is pretty amazing, the objects inside feel exactly as the ones constructive math always thought of them. Unfortunately, for my agenda, all this is way too "standard", way too infinitary: NNO exists, and looks and feels like the natural numbers, at least the ones seen through constructivistic glasses –  Mirco Mannucci Jun 3 '11 at 10:49
    
PS I am still waiting for your answer on my other question (feasible cat). If there is somebody here that can answer that one, that is you. –  Mirco Mannucci Jun 3 '11 at 10:51
    
There are many kinds of constructive math, the effective topos embodies the Russian school of constructivism. Another topos embodies Brouwerian intuitionism, for example. Anyhow, I think I convinced myself at some point that polytime realizer screw up logic, and from that point onwards I wasn't too interested in them anymore. I will try to remember what I thought went wrong. –  Andrej Bauer Jun 3 '11 at 12:58
    
Please do let me know. If by "screwing up" logic you mean that some basic rules are broken, such as for instance heyting implication, that sound like HEAVENLY MUSIC to me!!! Polytime, and even more extreme restrictions, SHOULD mess up the logic.I suspect that what went "wrong" is that you wanted to build another topos, and it did not work. PS Yes, I know, there are different brands of constructivism, but they are all "above" the level I am interested in, no topos would do. But something else may.. –  Mirco Mannucci Jun 3 '11 at 14:05
add comment

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.

share|improve this answer
    
@ Andreas Yes, I am quite familiar with AST. Many years ago Antonin Sochor tutored me on it in Praha. My only problem with AST is this: as you know, it can be developed from "limit universes" and from "witnessed universes" (wording of Vopenka). It is usually developed from the limit universe perspective, because postulating that a finite set (say the finite ordinal 2^1000) has a proper semiset inside makes it inconsistent (classically). –  Mirco Mannucci Jun 3 '11 at 0:06
    
However, as Vopenka pointed out in his book, the situation is more interesting: like Parikh's PA + F, the witnessed universe may be "feasibly consistent", in other words, proofs of its inconsistence may be all unfeasible (ie their internal coding may be "infinite" in AST sense). I am not aware of any research from the AST Team which developed witnessed universes, beyond its initial stage. Yes, bounded arithmetics enables one to consider the cut of small numbers. But this is not what I need, because in all models of Bounded arithmetics the cut contains all of N. –  Mirco Mannucci Jun 3 '11 at 0:10
    
According to the paper below (which provides many interesting connections betbetween $AST$ and orthodox foundational systems), $AST$ is mutually intepretable (and therefore equiconsistent with) THIRD order arithmetic: P. Pudlák and A. Sochor, Models of the alternative set theory. J. Symbolic Logic 49 (1984), no. 2, 570–585. –  Ali Enayat Jun 3 '11 at 2:02
    
Thanks Ali. I have never read the paper, but Pavel Pudlak told me about it. For many people this was a turn-off, they thought: -ok, so AST is "just" some higher order arithmetics in disguise-. But read my comment to Andreas: this interpretation works only for the "limit universe" AST, whereas the really hot AST is the "witnessed universe" one (ie the classically inconsistent AST where concrete sets have proper semisets inside. Basically a theory where a Cantorian finite set is infinite in Vopenka sense), which unfortunately seems to be still in its infancy. –  Mirco Mannucci Jun 3 '11 at 14:17
add comment

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.

share|improve this answer
    
Thanks Dan! I knew about Sazonov's system, and that is course relevant, though not exactly to my taste. Sazonov and I have had plenty of back-and-forth on FOM: he is a real ultrafinitist, or perhaps an actualist, he does believe there are PHYSICAL limitations to the size of numbers. I do not. The BOX number is sharp and fixed, I need something more fuzzy, and most important, I do not believe we should have a unique distinction between feasible and unfeasible, but a contextual one (something like degrees of feasibility). Perhaps Boucher's proposal is more akin to my needs. –  Mirco Mannucci Jun 4 '11 at 18:47
    
I think you're being unimaginative in how to devise a data format for truly arbitrarily large integers. Off the top of my head, the only thing in the C standard that implies a bounded memory space is the existence of the macro INTPTR_MAX (and similar macros). –  Hurkyl Jun 4 '11 at 23:37
    
@Hurkyl: Maybe I am being unimaginative. On the other hand $\aleph_0$ has a lot of large cardinal properties. As far as C goes, what about "sizeof", as in, "malloc(4*sizeof(T*))" ? –  Daniel Mehkeri Jun 5 '11 at 18:34
add comment

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).

share|improve this answer
    
Actually, your answer is relevant to my question: one of my motivations behind searching all possible venues toward ultrafinitistic math is that the usual blah blah blah that computers are (modeled by ) Turing machines is patently bogus: computer have very FINITE computational resources, so their internal number system is also finite (even linear-time functions are not really computable, only finite portions thereof). Now, my issue is: have we developed the formal math to describe the "world" of a finite computer? So far it looks like the answer is no. –  Mirco Mannucci Jun 3 '11 at 1:25
    
@Mirco: Well, I'm certainly not an expert in this area --- I have friends who have thought (and complained) about this stuff a lot more than I have. –  Theo Johnson-Freyd Jun 3 '11 at 2:10
1  
These finite limitations are not really present in the model of computation presented to the programmer. While any particular computer may have finite memory, the virtual machine embodied in a language such as C, etc. has infinite memory (which must be requested through appropriate memory allocations). In addition, although individual words have a finite number of bits (32 or 64), multiprecise arithmetic combines multiple words to allow an essentially unlimited arithmetic range. –  David Harris Jun 3 '11 at 11:21
3  
I like " $2^{32}$ is standard, if memory serves "; if memory doesn't serve, we might be limited to $2^{16}$. –  Andreas Blass Jun 3 '11 at 15:49
    
@Andreas: C.f. "I am not an expert" :) –  Theo Johnson-Freyd Jun 6 '11 at 1:42
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.