Baby arithmetic

Since chapter 7 in Peter Smith's book is so short, I'll summarize it quickly and then start discussing chapter 8.

Chapter 7 starts by comparing the two incompleteness theorems discussed in previous chapters (let's call these "Smith's theorems") to Gödel's first incompleteness theorem as follows:

1. Each one of Smith's theorems states that formal systems that satisfy two conditions are incomplete. In Smith's first theorem, the formal system must be sound and its language must be sufficiently expressive. In Smith's second theorem, the formal system must be consistent (a syntactic property that is weaker than soundness, a semantic property) and sufficiently strong (a property that is stronger than sufficient expressiveness). Smith states that Gödel's first theorem also comes in two varieties, with a similar trade-off between the strengths of two conditions.
2. Unlike Gödel's proof, the proofs of Smith's theorems do not involve self-reference through the arithmetization of meta-mathematics. On the other hand, Gödel's proof is constructive: it includes a method for building a true sentence that is unprovable. Smith's proofs are much easier; but they are not constructive.
3. Gödel's proof does not rely on the whole class of decidable numerical properties and relations as Smith's proofs do, through the definitions of sufficient expressiveness and sufficient strength. Instead, Gödel's proof relies on the class of so-called primitive recursive properties and relations, which is a strict subset of the decidable ones.

The rest of Chapter 7 is a road map for the next 10 chapters or so, which culminate in the proof of Gödel's first theorem, but start with two well-known formal systems of arithmetic, namely "Robinson Arithmetic" and "First-Order Peano Arithmetic," which are both based on the formal language L_A,

But first, Smith describes a simpler formal system, called Baby Arithmetic (or BA), which is the part of Chapter 8 that I want to discuss in the rest of this post.

• The language of BA, let's call it L_B, is a strict subset of the language L_A. They have the same non-logical vocabulary, namely the symbols 0, S, + and ×. However, the logical vocabulary of L_B is missing numerical variables and quantifiers (it still contains the equality symbol and the usual connectives). The interpretation of L_B is identical to that of the corresponding components of L_A.
• The deductive apparatus of BA can include any of the usual inference rules of propositional logic, together with rules for the equality predicate; for example, from any sentence φ and the identity ρ = τ, where ρ and τ are terms, Leibniz's law enables us to infer the sentence obtained by substituting in φ every occurrence of ρ by τ.
• BA contains 6 non-logical axioms that specify the structure of the natural number sequence and define the addition and multiplication functions. Since BA does not contain quantifiers nor variables, each axiom is a template or schema using the Greek letters α and β as placeholders for numerical expressions. So each schema generates an infinite number of sentences, one for each possible substitution of the Greek letter(s). For example, the first schema below generates the sentences 0 ≠ S0, 0 ≠ SS0, 0 ≠ SSS0, 0 ≠ S(S0 × SS0), etc. Here are the 6 axiom schemata of BA:
• Schema 1: 0 ≠ Sα
• i.e., 0 is not the successor of any number
• Schema 2: (Sα = Sβ) → (α = β)
• i.e., by contraposition, any two distinct numbers have distinct successors
• Schema 3: α + 0 = α
• i.e., base case for the definition of addition
• Schema 4: α + Sβ = S(α + β)
• i.e., recursive case for the definition of addition
• Schema 5: α × 0 = 0
• i.e., base case for the definition of multiplication
• Schema 6: α × Sβ = (α × β) + α
• i.e., recursive case for the definition of multiplication

Note that BA meets all of the requirements of an axiomatized formal theory (or AFT). For example, it is decidable whether or not a sentence of  L_B is an instance of an axiom schema of BA.

Then, Smith proves that BA is negation-complete, that is, for any sentence φ in L_B, either BA ⊢ φ or BA ⊢ ¬ φ. In fact, Smith proves that BA correctly decides all sentences in L_B.

Finally, since BA is negation-complete, we can automatically infer, using a previously discussed theorem, that BA is decidable.

In conclusion, BA is complete: it can prove every true statement that its language can express. Unfortunately, its language can express little. It can express specific statements, such as: 2 + 3 = 5, 4 ≠ 2 × 3, the successor of 0 is not 0, the successor of 1 is not 0, the successor of 2 is not 0, etc. However, it cannot express general statements, such as: all natural numbers have a successor that is different from 0. Nevertheless, stronger AFTs of arithmetic can be obtained by extending BA.