MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

Are there books or survey articles explaining the subject to a non-expert? To clarify what I mean, here is a couple of issues that I would like to read about. (I am mainly interested in references but would appreciate answers to these specific questions.)

1) As far as I remember, PA do not have a "built-in" scheme for inductive definitions. So I assume that it is not immediately clear how to define things like $x^n$ or the $n$th Fibonacci number. How do they do things like that? One can define some specific coding of finite sequences of numbers and use that, but this is so ugly and so specific to aritmetics, it there a better way?

2) I vaguely remember that there are arithmetic facts provable in ZF but not in PA. Is this indeed the case? Are there simple explicit examples? Is there a way to understand, at least informally, why PA is not enough? (E.g. a proof may use analysis but why cannot it be reformulated in terms of some kind of "constructible" numbers and functions?)

Background: I am as far from logic as a mathematician can be.

share|cite|improve this question
Well,the old classics-namely Elliott Mendelson's THE NUMBER SYSTEMS and AN INTRODUCTION TO MATHEMATICAL LOGIC as well as Herbert Enderton's ELEMENTS OF SET THEORY all have excellent in-depth discussions of these matter,Sergei. – The Mathemagician Mar 21 '10 at 19:14
“One can define some specific coding of finite sequences of numbers and use that, but this is so ugly and so specific to aritmetics” Really? This seems to me like the fact that using the binary logic of transistors, one can encode arbitrary computation, not to mention text and cat videos. Any specific encoding will be ad hoc and a little ugly — but the fact one can do it is fundamental and beautiful! – Peter LeFanu Lumsdaine Jan 31 at 14:03
up vote 8 down vote accepted

For obvious reasons, foundations textbooks (undergraduate or beginning graduate level) tend to have essentially no prerequisites, so I suspect you will find most of them to be accessible.

Here are some higher level recommendations that are more to the point. These assume some rudimentary knowledge of Computability Theory and Model Theory. One well-written book that directly addresses your question is Richard Kaye's Models of Peano Arithmetic (Oxford Logic Guides 15, OUP, 1991). It's pretty accessible, but I think it's out of print. Another is Metamathematics of First-Order Arithmetic (available on Project Euclid) by Hájek and Pudlák. This one is still available but I wouldn't recommend it to a beginner. For second-order arithmetic and it's relationship to mainstream mathematics, Simpson's Subsystems of Second-Order Arithmetic (2nd ed, CUP, 2010) is the canonical choice. The early parts are very accessible but the later chapters are much denser.

Examples for (2) include:

share|cite|improve this answer
Thank you. Although I am yet to find at least the ToC of Kaye's book, I managed to get Simpson's book - it looks like a great book on foundations. But I actually meant something of more popular level, maybe guide-style rather than textbook-style. – Sergei Ivanov Mar 21 '10 at 23:00
I'm afraid what you're asking is a rather broad and technical, so not typical "tour guide" material. You can find decent short presentations of specific results, e.g. Goodstein's Theorem, Paris-Harrington Theorem, Hydra Games, etc. – François G. Dorais Mar 21 '10 at 23:45
Probably you are right and I'm asking too much (although there are tour guides to deep math, Frank Morgan's "Beginner's geometric measure theory" comes to mind). Anyway, I learned a lot from your answer (G\"odel thm not provable in PA was especially surprising). Thanks a lot. – Sergei Ivanov Mar 22 '10 at 8:56

Several people have given excellent answers to your second question, so let me address the first.

2) As far as I remember, PA do not have a "built-in" scheme for inductive definitions. So I assume that it is not immediately clear how to define things like $x_n$ or the $n$-th Fibonacci number. How do they do things like that? One can define some specific coding of finite sequences of numbers and use that, but this is so ugly and so specific to aritmetics, it there a better way?

Permitting definitions by primitive recursion moves you from Peano arithmetic to Godel's System T. This is a conservative extension of Peano arithmetic, which also allows defining functions by recursion over the natural numbers.

In the modern presentation (due to Tait, IIRC), the idea is that we move from a first-order logic with a domain of natural numbers, to a multi-sorted first-order logic, where quantification is permitted over functions of higher type in addition. So the sorts of the logic are types like $\mathbb{N}$, $\mathbb{N} \to \mathbb{N}$, $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$, and so on. The terms of higher type are given by a simple typed lambda calculus (i.e., a simple functional programming language).

One of the nice things about System T is that even though it is conservative over Peano arithmetic, it also makes the step from arithmetic to analysis much easier to see. Since a real number can be represented by a term of type $\mathbb{N} \to \mathbb{N} \times \mathbb{N}$ (e.g, as a Cauchy sequence of rationals), in this setting it's easy to understand exactly how much extra axiomatic strength various theorems of analysis need beyond basic Peano arithmetic. As F.G. Dorais has already mentioned, Simpson's Subsystems of Second-Order Arithmetic is the standard reference here.

share|cite|improve this answer
I am confused by what you say about primitive recursion. Why do you need an extension? If f is primitive recursive, one could define the relation "y=f(x)" as "there is a sequence $z_0$, ..., $z_x$ such that ..." where finite sequences are coded by numbers. Then one could prove the existence and uniqueness by induction. What is wrong with this approach? No suitable coding? – Sergei Ivanov Mar 22 '10 at 14:25
Nothing at all is wrong with what you suggest -- it works! I only wanted to illustrate how to directly represent the notion of definition within a formal system, as opposed to treating it as an encoding or "figure of speech" in a smaller logic lacking such a feature. In the case of PA, adding definitions does not change its strength -- but in other cases, it can. – Neel Krishnaswami Mar 22 '10 at 14:48
System T is stronger than primitive recursion: system T extends PRA by allowing recursors at all finite types, while PRA only allows them over the natural numbers. But yes, I agree and to emphasise: system T is the equational theory corresponding to PA, and defines just the functions that PA proves total. – Charles Stewart Mar 30 '10 at 9:20

There are people far more expert on this than I, but for the answer to (2), Goodstein's theorem is a famous example. There's a bit about it here

share|cite|improve this answer

If one adopts a higher order attitude towards PA, then one makes the transition from reasoning within PA to wanting to understand the structure of all the models of PA, of which there is a rich diversity. This move is analogous to the common change in viewpoint one undergoes in abstract algebra, moving at first from studying an individual group or ring from inside, using the axioms directly, to studying structure theorems about all groups or all rings from the outside, and exploring especially how they relate to each other.

Indeed, many of the most fascinating aspects of PA as a first order theory, such as the independence results mentioned in the other answers, flow from the fact that there are so many different models of PA. Perhaps the most authoritive book on the structure of the models of Peano Arithmetic is:

This book investigates the collection of all models of PA, analyzing their substructure lattices, saturation properties, various kinds of extensions, cuts, automorphisms, order types and so on. I highly recommend it. It appears to be aimed at students who have had already had some exposure to basic mathematical logic, and for this reason may be more advanced than you wanted.

share|cite|improve this answer

Regarding your first question ("How to define things like $x^n$ or the $n$-th Fibonacci number; one can define a coding of finite sequences but this is so ugly, is there a better way?")

No, that's the way. Using e.g. Gödel's "beta function" (which is based on the Chinese remainder theorem) you can code a finite sequence $(a_1, \ldots, a_k)$ by a pair of numbers $(a,m)$ (which, if desired, can be encoded as a single number using a pairing function).

Then, to write "$a^b=c$" you write "There exists a sequence $(a_0, \ldots, a_b)$ such that $a_0=1$, $a_b=c$, and $a_{i+1} = a\cdot a_i$ for each $i<b$."

(Or else you can write "For every finite sequence $(a_0, \ldots)$, if $a_0=1$ and $a_{i+1} = a\cdot a_i$ for each $i<b$, then $a_b=c$" -- if a "$\forall$" suits better than an "$\exists$" for your particular purpose.)

(There are other alternatives besides the beta function; see e.g. Nelson for a cute way of representing finite sets using binary notation inside base-4 notation.)

share|cite|improve this answer

Your Answer


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.