Weak Systems of Arithmetic
Posted by John Baez
The recent discussion about the consistency of arithmetic made me want to brush up on my logic. I’d like to learn a bit about axioms for arithmetic that are weaker than Peano arithmetic. The most famous is Robinson arithmetic:- Robinson arithmetic, Wikipedia.
Instead of Peano arithmetic’s axiom schema for mathematical induction, Q only has inductive definitions of addition and multiplication, together with an axiom saying that every number other than zero is a successor. It’s so weak that it has computable nonstandard models! But, as the above article notes:
Q fascinates because it is a finitely axiomatized first-order theory that is considerably weaker than Peano arithmetic (PA), and whose axioms contain only one existential quantifier, yet like PA is incomplete and incompletable in the sense of Gödel’s Incompleteness Theorems, and essentially undecidable.
But there are many interesting systems of arithmetic between PA and Q in strength. I’m hoping that if I tell you a bit about these, experts will step in and tell us more interesting things—hopefully things we can understand!
For example, there’s primitive recursive arithmetic, or PRA:
- Primitive recursive arithmetic, Wikipedia.
This system lacks quantifiers, and has a separate predicate for each primitive recursive function, together with an axiom recursively defining it.
What’s an interesting result about PRA? Here’s the only one I’ve seen: its proof-theoretic ordinal is $ω^ω$. This is much smaller than the proof-theoretic ordinal for Peano arithmetic, namely $\epsilon_0$.
What’s $\epsilon_0$? It’s a big but still countable ordinal which I explained back in week236. And what’s the proof-theoretic ordinal of a theory?
Ordinal analysis concerns true, effective (recursive) theories that can interpret a sufficient portion of arithmetic to make statements about ordinal notations. The proof theoretic ordinal of such a theory T is the smallest recursive ordinal that the theory cannot prove is well founded — the supremum of all ordinals $\alpha$ for which there exists a notation $o$ in Kleene’s sense such that T proves that $o$ is an ordinal notation.
For more details, try this wonderfully well-written article:
- Michael Rathjen, The art of ordinal analysis, International Congress of Mathematicians, II, Eur. Math. Soc., Zurich, pp. 45–69.
Climbing down the ladder we eventually meet elementary function arithmetic, or EFA:
- Elementary function arithmetic, Wikipedia.
Its proof-theoretic ordinal is just $\omega^3$. It’s famous because Harvey Friedman made a grand conjecture about it:
Every theorem published in the Annals of Mathematics whose statement involves only finitary mathematical objects (i.e., what logicians call an arithmetical statement) can be proved in EFA. EFA is the weak fragment of Peano Arithmetic based on the usual quantifier-free axioms for 0, 1, +, $\times$, exp, together with the scheme of induction for all formulas in the language all of whose quantifiers are bounded.
Does anyone know yet if Fermat’s Last Theorem can be proved in EFA? I seem to remember early discussions where people were wondering if Wiles’ proof could be formalized in Peano arithmetic.
But let’s climb further down the ladder. How low can we go? I guess $\omega$ is too low to be the proof-theoretic ordinal of any theory “that can interpret a sufficient portion of arithmetic to make statements about ordinal notations.” Is that right? How about $\omega + 1$, $2 \omega$, and so on?
There are some theories of arithmetic whose proof-theoretic ordinal is just $\omega^2$. One of them is called IΔ_{0}. This is Peano arithmetic with induction restricted to predicates where all the for-alls and there-exists quantify over variables whose range is explicitly bounded, like this:
$\forall i \le n \; \forall j \le n \; \forall k \le n \; (i^3 + j^3 \ne k^3)$
Every predicate of this sort can be checked in an explicitly bounded amount of time, so these are the most innocuous ones.
Such predicates lie at the very bottom of the arithmetical hierarchy, which is a way of classifying predicates by the complexity of their quantifiers. We can also limit induction to predicates at higher levels of the arithmetic hierarchy, and get flavors of arithmetic with higher proof-theoretic ordinals.
But you can always make infinities bigger — to me, that gets a bit dull after a while. I’m more interested in life near the bottom. After all, that’s where I live: I can barely multiply 5-digit numbers without making a mistake.
There are even systems of arithmetic too weak to make statements about ordinal notations. I guess Q is one of these. As far as I can tell, it doesn’t even make sense to assign proof-theoretic ordinals to these wimpy systems. Is there some other well-known way to rank them?
Much weaker than Q, for example, is Presburger arithmetic:
- Presburger arithmetic, Wikipedia.
This is roughly Peano arithmetic without multiplication! It’s so simple you can read all the axioms without falling asleep:
$\not (0 = x + 1)$
$x + 1 = y + 1 \implies x = y$
$x + 0 = x$
$(x + y) + 1 = x + (y + 1)$
and an axiom schema for induction saying:
$(P(0) \; \& \; (P(x) \implies P(x + 1))) \; \implies \; P(y)$
for all predicates $P$ that you can write in the language of Presburger arithmetic.
Presburger arithmetic is so simple, Gödel’s first incompleteness theorem doesn’t apply to it. It’s consistent. It’s complete: for every statement in Presburger arithmetic, either it or its negation is provable. But it’s also decidable: there’s an algorithm that decides which of these two alternatives holds!
However, Fischer and Rabin showed that no algorithm can do this for all statements of length $n$ in less than $2^{2^{c n}}$ steps. So, Presburger arithmetic is still fairly complicated from a practical perspective. (In 1978, Derek Oppen showed an algorithm with triply exponential runtime can do the job.)
Presburger arithmetic can’t prove itself consistent: it’s not smart enough to even say that it’s consistent! However, there are weak systems of arithmetic that can prove themselves consistent. I’d like to learn more about those. How interesting can they get before the hand of Gödel comes down and smashes them out of existence?
Re: Weak Systems of Arithmetic
Does anyone know yet if Fermat’s Last Theorem can be proved in EFA? I seem to remember early discussions where people were wondering if Wiles’ proof could be formalized in Peano arithmetic.
I’ve heard Angus MacIntyre talking about this. He is working on a paper arguing that Wiles’ proof translates into PA. I say ‘arguing’ rather than ‘proving’ because all he plans to do is show that the central objects and steps can be formalised in PA, rather than translate the entirety of Wiles’ proof, which would be a a ridiculously Herculean task. I don’t know if his paper is available yet, but there’s some discussion of it here.