Avigad Archives - Logic Matters

Avigad MLC — 6: Arithmetics

Books, MLC / Leave a Comment / December 29, 2022

Chs 1 to 7 of MLC, as we’ve seen, give us a high-level and often challenging introduction to core first-order logic with a quite strongly proof-theoretic flavour. Now moving on, the next three chapters are on arithmetics — Ch. 8 is on primitive recursion, Ch. 9 on PRA, and Ch. 10 on richer first-order arithmetics.

I won’t pause long over Ch. 8, as the basic facts about p.r. functions aren’t wonderfully exciting! Avigad dives straight into the general definition of p.r. functions, and then it’s shown that the familiar recursive definitions of addition, exponentiation, and lots more, fit the bill. We then see how to handle finite sets and sequences in a p.r. way. §8.4 discusses other recursion principles which keep us within the set of p.r. functions, and §8.5 discusses recursion along well-founded relations — these two sections are tersely abstract, and it would surely have been good to have more by way of motivating examples. Finally §8.6 tells us about diagonalizing out of the p.r. functions to get a computable but not primitive recursive function, and says just a little about fast-growing functions. All this is technically fine, it goes without saying; though once again I suspect that many students will find this chapter more useful if they have had a preliminary warm-up with a gentler first introduction to the topic first.

But while Ch. 8 might be said to be relatively routine (albeit quite forgiveably so!), Ch. 9 is anything but. It is the most detailed and helpful treatment of Primitive Recursive Arithmetic that I know.

Avigad first presents an axiomatization of PRA in the context of a classical quantifier-free first-order logic. Hence

The logic has the propositional connectives, axioms for equality, plus a substitution rule (wffs with variables are treated as if universally quantified, so from $A(x)$ we can infer $A(t)$ for any term).
We then have a symbol for each p.r. function — and we can think of these added iteratively, so as each new p.r. function is defined by composition or primitive recursion from existing functions, a symbol for the new function is introduced along with its appropriate defining quantifier-free equations in terms of already-defined functions.
We also have a quantifer-free induction rule: from $A(0)$ and $A(x) \to A(Sx)$ , infer $A(t)$ for any term.

§§9.1–9.3 explore this version of PRA in some detail, deriving a lot of arithmetic, showing e.g. that PRA proves that if $p$ is prime, and $p \mid xy$ then either $p \mid x$ or $p \mid y$ , and noting along the way that we could have used an intuitionistic version of the logic without changing what’s provable.

Then the next two sections very usefully discuss two variant presentations of PRA. §9.4 enriches the language and the logic by allowing quantifiers, though induction is still just for quantifier-free formulas. It is proved that this is conservative over quantifier-free PRA for quantifier-free sentences. And there’s a stronger result. Suppose full first-order PRA proves the $\Pi_2$ sentence $\forall x \exists y A(x, y)$ , then for some p.r. function symbol $f$ , quantifier-free PRA proves $A(x, f(x))$ (and we can generalize to more complex $\Pi_2$ sentences).

By contrast §9.5 weakens the language and the logic by removing the connectives, so all we are left with are equations, and we replace the induction rule by a rule which in effect says that functions satisfying the same p.r. definition are everywhere equal. This takes us back — as Avigad nicely notes — to the version of PRA presented in Goodstein’s (now unread?) 1957 classic Recursive Number Theory, which old hands might recall is subtitled ‘A Development of Recursive Arithmetic in a Logic-Free Equation Calculus’.

All this is done in an exemplary way, I think. Perhaps Avigad is conscious that in this chapter he is travelling over ground that it is significantly less well-trodden in other textbooks, and so here he allows himself to be rather more expansive in his motivating explanations, which works well.

The following Ch. 10 is the longest in the book, some forty two pages on ‘First-Order Arithmetic’. Or rather, the chapter is on arithmetics, plural — for as well as the expected treatment of first-order Peano Arithmetic, with nods to Heyting Arithmetic, there is also a perhaps surprising amount here about subsystems of classical PA.

In more detail, §10.1 briefly introduces PA and HA. You might expect next to get a section explaining how PA (with rather its minimal vocabulary) can be in fact seen as extending the PRA which we’ve just met (with all its built-in p.r. functions). But we have to wait until §10.4 to get the story about how to define p.r. functions using some version of the beta-function trick. In between, there are two longish sections on the arithmetical hierarchy of wffs, and on subsystems of PA with induction restricted to some level of the hierarchy. Then §10.5 shows e.g. how truth for $\Sigma_n$ sentences can be defined in a $\Sigma_n$ way, and shows e.g. that I $\Sigma_{n+1}$ (arithmetic with induction for $\Sigma_{n + 1}$ wffs) can prove the consistency of I $\Sigma_{n}$ , and also — again using truth-predicates — it is shown e.g. that I $\Sigma_{n}$ is finitely axiomatizable. (There’s a minor glitch. In the proof of 10.3.5 there is a reference to the eighth axiom of $Q$ — but Robinson arithmetic isn’t in fact introduced until Chapter 12.)

The material here is all stuff that is very good to know. Your won’t be surprised by this stage to hear that the discussion is a bit dense in places; but up to this point it should all be pretty manageable because the ideas are, after all, straightforward enough.

However, the chapter ends with another ten pages whose role in the book I’m not at all so sure about. §10.6 proves three theorems using cut elimination arguments, namely (1) that I $\Sigma_{1}$ is conservative over PRA for $\Pi_2$ formulas; (2) Parikh’s Theorem, (3) that so-called B $\Sigma_{n+1}$ is conservative over I $\Sigma_{n}$ for $\Pi_{n+2}$ wffs. What gives these results, in particular the third, enough interest to labour through them? They are, as far as I can see, never referred to again in later chapters of the book. And yet §10.7 then proves the same theorems again using model theoretic arguments. I suppose that these pages give us samples of the kinds of conservation results we can achieve and some methods for proving them. But I’m not myself convinced they really deserve this kind of substantial treatment in a book at this level.