NECESSARILY NON-ANALYTIC INDUCTION PROOFS──SUMMARY OF SOME RESULTS ══════════════════════════════════════════════════════════════════ version: 2020-01-22 Anders Lundstedt anders.lundstedt@philosophy.su.se Contents ──────── §1 Introduction §2 Two results proved by non-analytic induction §3 Tail-recursion §4 Definitions §5 Fact 2.2 must be proved by non-analytic induction §6 Fact 2.4 must be proved by non-analytic induction §7 Fact 3.2c must be proved by non-analytic induction §8 Facts 3.2a, 3.2b and 3.6 must be proved by non-analytic induction §9 Discussion and future work §A Some definitions and results §B Proofs of Lemmas 5.7 and 5.8 §C Proofs of Lemmas 6.10, 6.11 and 6.13 References §1 Introduction ─────────────── Some mathematical facts seem to not lend themselves to a "straightforward" induction proof──the proof attempt gets "stuck" at the induction step──but instead a "straightforward" induction proof of a "stronger" fact succeeds. The fact we originally wanted to prove then follows from this "stronger" fact. This proof method is usually called something like "strengthening of the induction hypothesis". However, there need not always be a precise sense in which the "stronger" fact is, in fact, stronger. Thus, following Hetzl and Wong (2017), I use the more general terminology "non-analytic induction proofs" for such proofs. Consequently, I will use "analytic induction proofs" to refer to ordinary "straightforward" induction proofs. ∗∗ Faced with a non-analytic induction proof, a natural question is whether the non-analyticity is necessary──that is, could we have proved what we wanted to prove by analytic induction, without the "detour" proving some other fact? Hetzl and Wong have made precise sense of such questions in the setting of first-order arithmetic. ∗∗ In §2 we look at two examples of non-analytic induction proofs, proving the two facts: (F1) For all natural numbers n: 1+3+5+⋅⋅⋅+(2n-1) = k² for some natural number k. (F2) For all natural numbers n: 1+2⁻²+3⁻²+⋅⋅⋅+(n+1)⁻² < 2. ∗∗ In §3 we look at more examples of non-analytic induction proofs: correctness proofs for "tail-recursive" definitions of multiplication, of exponentiation, and of the factorial. ∗∗ In §4 I present a slight generalization and reformulation of some of the notions introduced by Hetzl and Wong. ∗∗ Using the notions introduced in §4 I show that there are precise senses in which the example facts may only be proved by non-analytic induction. ─ In §5 I show that (F1) may only be proved by non-analytic induction. ─ In §6 I show that (F2) may only be proved by non-analytic induction. ─ In §7 and §8 I show that the correctness properties from §3 may only be proved by non-analytic induction. ∗∗ In §9 I discuss the results and present some ideas for future work. ∗∗ The lazy, or busy, reader may wish to skip §§6–8, as the core ideas of §§6–8 are present in simpler form in §5. Then §3 may be skipped as well since it is a prerequisite only for §7 and §8. ∗∗ §2 Two results proved by non-analytic induction ─────────────────────────────────────────────── For our first case, we have that the sum of any initial segment of the odd natural numbers is a perfect square, that is, for all natural numbers n: 1+3+5+⋅⋅⋅+(2n-1) = k² for some natural number k, or, avoiding ellipsis notation, the following. ∗∗ DEFINITION 2.1. f₂ : ℕ → ℕ is defined recursively by f₂(0) := 0, f₂(n+1) := f₂(n)+2n+1. ∗∗ FACT 2.2. For all natural numbers n: f₂(n) = k² for some natural number k. PROOF ATTEMPT. "Straightforward" induction: ─ Base case: We have f₂(0) = 0 (by Definition 2.1) = 0² so f₂(0) = k² for k = 0. ─ Induction step: f₂(n+1) = f₂(n)+2n+1 (by Definition 2.1) = k²+2n+1 (for some k, by induction hypothesis). But k²+2n+1 is not a perfect square for all natural numbers k and n so how do we proceed from here? ACTUAL PROOF. It suffices to prove the following stronger fact, of which Fact 2.2 is a logical consequence. f₂(n) = n² for all natural numbers n. (This fact is not a logical consequence of Fact 2.2, so it is stronger than Fact 2.2 in at least that sense.) We prove this fact by induction. ─ Base case: f₂(0) = 0 (by Definition 2.1) = 0². ─ Induction step: f₂(n+1) = f₂(n)+2n+1 (by Definition 2.1) = n²+2n+1 (by induction hypothesis) = (n+1)². □ ∗∗ For our second case, we have 1+2⁻²+3⁻²+⋅⋅⋅+(n+1)⁻² < 2 for all natural numbers n, or, avoiding ellipsis notation, the following. ∗∗ DEFINITION 2.3. g₂ : ℕ → ℚ is defined recursively by g₂(0) := 1, g₂(n+1) := g₂(n)+(n+2)⁻². ∗∗ FACT 2.4. g₂(n) < 2 for all natural numbers n. PROOF ATTEMPT. "Straightforward" induction: ─ Base case: g₂(0) = 1 (by Definition 2.3) < 2. ─ Induction step: g₂(n+1) = g₂(n)+(n+2)⁻² (by Definition 2.3) < 2+(n+2)⁻² (by induction hypothesis). But 2+(n+2)⁻² ≮ 2 for any natural number n so how do we proceed from here? ACTUAL PROOF. It clearly suffices to prove the stronger fact g₂(n) ≤ 2-(n+1)⁻¹ for all natural numbers n. (In what sense is this fact stronger than Fact 2.4? It is at least stronger in the sense that for all g : ℕ → ℚ, g(n) ≤ 2-(n+1)⁻¹ for all n implies g(n) < 2 for all n, while the converse implication does not hold for all g : ℕ → ℚ.) We prove this fact by induction. ─ Base case: g₂(0) = 1 (by Definition 2.3) ≤ 1 = 2-(0+1)⁻¹. ─ Induction step: g₂(n+1) = g₂(n)+(n+2)⁻² (by Definition 2.3) ≤ 2-(n+1)⁻¹+(n+2)⁻² (by induction hypothesis) = 2-(n+2)⁻¹-(n+1)⁻¹(n+2)⁻² (by elementary arithmetic) ≤ 2-(n+2)⁻¹ = 2-((n+1)+1)⁻¹. □ ∗∗ §3 Tail-recursion ───────────────── For practical reasons one might want to implement recursive functions such that they are "tail-recursive". I am not overly familiar with "tail-recursion" but for present purposes what matters is that we have non-standard "tail-recursive" definitions of common functions. We will consider tail-recursive definitions of multiplication, of exponentiation, and of the factorial. For each definition one naturally desires a correctness proof. It turns out that such correctness proofs seem to require non-analytic induction. ∗∗ The technique we will use to convert the standard recursive definitions to tail-recursive definitions is to introduce an extra "accumulator" argument. ∗∗ DEFINITION 3.1. (a) Multiplication × : ℕ² → ℕ is defined recursively by n×0 := 0, n×(m+1) := n×m+n. (b) Exponentiation –⁻ : ℕ² → ℕ is defined recursively by n⁰ := 1, nᵐ⁺¹ := nᵐ×n. (c) The factorial ! : ℕ → ℕ is defined recursively by 0! := 1, (n+1)! := (n+1)×n!. (d) The function m-acc : ℕ³ → ℕ is defined recursively by m-acc(a,n,0) := a, m-acc(a,n,m+1) := m-acc(a+n,n,m), (e) The function e-acc : ℕ³ → ℕ is defined recursively by e-acc(a,n,0) := a, e-acc(a,n,m+1) := e-acc(a×n,n,m), (e) The function f-acc : ℕ² → ℕ is defined recursively by f-acc(a,0) := a, f-acc(a,m+1) := f-acc(a×(m+1),m). ∗∗ EXAMPLE. m-acc(0,5,3) = m-acc(0,5,2+1) = m-acc(0+5,5,2) (by Definition 3.1d) = m-acc(0+5,5,1+1) = m-acc(0+5+5,5,1) (by Definition 3.1d) = m-acc(0+5+5,5,0+1) = m-acc(0+5+5+5,5,0) (by Definition 3.1d) = 0+5+5+5 (by Definition 3.1d) = 5×3. ∗∗ FACT 3.2. For all natural numbers n and m: (a) n×m = m-acc(0,n,m), (b) nᵐ = e-acc(1,n,m), (c) n! = f-acc(1,n). PROOF ATTEMPT. We try to prove (a) by induction on m. The base case is immediate. For the induction step we have n×(m+1) = n×m+n (by Definition 3.1a) = m-acc(0,n,m)+n (by induction hypothesis) and m-acc(0,n,m+1) = m-acc(0+n,n,m) (by Definition 3.1d) = n-acc(n,n,m). It seems we cannot get any further and that we are "stuck". Similarly one gets "stuck" when attempting "straightforward" induction proofs of (b) and (c). ACTUAL PROOF. (a)–(c) are immediate consequences of the following stronger facts. For all natural numbers a, n and m: (a') m-acc(a,n,m) = a+n×m, (b') e-acc(a,n,m) = a×nᵐ, (c') f-acc(a,n) = a×n!. We prove (a'). The proof of (c') is similar and the proof of (b') is exactly the same up to substitution of function symbols and constants. For (a'), induction on m gives the following. ─ Base case: m-acc(a,n,0) = a (by Definition 3.1d) = a+0 = a+n×0 (by Definition 3.1a). ─ Induction step: m-acc(a,n,m+1) = m-acc(a+n,n,m) (by Definition 3.1d) = (a+n)+n×m (by induction hypothesis) = a+(n×m+n) (by associativity and commutativity) = a+n×(m+1) (by Definition 3.1a). □ ∗∗ The above proof uses additive identity of 0 and associativity and commutativity of addition. These properties are in fact not necessary. We state and prove a more general fact as follows. ∗∗ ASSUMPTION 3.3. ─ Let A be any set. ─ Let a₀ be an element in A. ─ Let ∙ : A² → A. ∗∗ DEFINITION 3.4. (a) The function ∙∙ : A×ℕ → A is defined recursively by a∙∙0 := a₀, a∙∙(n+1) := (a∙∙n)∙a. (b) The function acc : A²×ℕ → A is defined recursively by acc(a,b,0) := a, acc(a,b,n+1) := acc(a∙b,b,n). ∗∗ LEMMA 3.5. For all a and b in A and for all natural numbers n: acc(a,b,n)∙b = acc(a∙b,b,n). PROOF. Induction on n. ─ Base case: acc(a,b,0)∙b = a∙b (by Definition 3.4b) = acc(a∙b,b,0) (by Definition 3.4b). ─ Induction step: acc(a,b,n+1)∙b = acc(a∙b,b,n)∙b (by Definition 3.4b) = acc((a∙b)∙b,b,n) (by induction hypothesis) = acc(a∙b,b,n+1) (by Definition 3.4b). □ ∗∗ FACT 3.6. For all a in A and all natural numbers n: a∙∙n = acc(a₀,a,n). PROOF. With Lemma 3.5 at our disposal, "straightforward" induction on n will work. ─ Base case: a∙∙0 = a₀ (by Definition 3.4a) = acc(a₀,a,0) (by Definition 3.4b). ─ Induction step: a∙∙(n+1) = (a∙∙n)∙a (by Definition 3.4a) = acc(a₀,a,n)∙a (by induction hypothesis) = acc(a₀∙a,a,n) (by Lemma 3.5) = acc(a₀,a,n+1) (by Definition 3.4b). □ ∗∗ REMARK. The above proof is an analytic induction proof. However, as is shown in §8, without first proving, by induction, something like Lemma 3.5, an analytic induction proof is not possible. ∗∗ §4 Definitions ────────────── This section presents a reformulation and slight generalization of some of the notions introduced by Hetzl and Wong (2017). I choose to introduce some non-conventional machinery, allowing for rich languages in order to be able to conveniently and transparently represent mathematical facts and proofs. ∗∗ DEFINITION 4.1. ─ The ∗full (first-order) language of arithmetic∗, notation ℒ[full], is the first-order language with the following vocabulary. For each natural number n: ─ n is a constant symbol, ─ for each function f : ℕⁿ⁺¹ → ℕ: f is a function symbol of arity n+1, ─ for each relation P ⊆ ℕⁿ⁺¹: P is a relation symbol of arity n+1. ─ The ∗minimal (first-order) language of arithmetic∗, notation ℒ[min], is the ℒ[full]-reduct with signature ⟨0,1,+⟩. ─ The ∗standard (first-order) language of arithmetic∗, notation ℒ₀, is the ℒ[full]-reduct with signature ⟨0,1,+,×,<⟩. ─ A first-order language is a ∗(first-order) language of arithmetic∗ if and only if it is an ℒ[min]-expansion. ─ Let L be a language of arithmetic. ─ If L is an ℒ[full]-reduct then L is ∗pure∗; otherwise L is ∗impure∗. ─ pure(L) := L∩ℒ[full] is the ∗pure part∗ of L. ─ impure(L) := L-ℒ[full] is the ∗impure part∗ of L. ∗∗ Thus any pure language of arithmetic has as symbols natural numbers and operations and relations on natural numbers. This is just a convenient "trick" which allows us to easily define the standard model for these languages. ∗∗ DEFINITION 4.2. ─ Let L be a pure language of arithmetic. ─ The ∗standard L-model∗ has domain ℕ and each symbol interpreted as itself. ─ Let M be an L-model. If M is isomorphic to the standard L-model then M is ∗standard∗; otherwise M is ∗non-standard∗. ─ The L-theory ∗true L-arithmetic∗ is the theory of the standard L-model. ─ Any subset of true L-arithmetic is a ∗theory of L-arithmetic∗. ─ Let L be an impure language of arithmetic, let M be an L-model and let T be an L-theory. ─ M is ∗standard∗ if its pure(L)-reduct is; otherwise M is ∗non-standard∗. ─ T is a ∗theory of L-arithmetic∗ if and only if T is true in some standard L-model. ∗∗ REMARKS. Let L be an impure language. ─ There are infinitely many non-isomorphic standard L-models──one for each way of expanding the standard pure(L)-model to L. (Similarly, there are infinitely many standard L-models that are not elementary equivalent. Thus there are also infinitely many non-compatible theories of L-arithmetic.) ─ For an L-theory T there may be none, one, or many non-isomorphic standard models of T (and T is a theory of L-arithmetic if and only if there is at least one such standard model). ∗∗ NOTATIONS. ─ ℕ₀ is the standard ℒ₀-model. ─ ℕ[min] is the standard ℒ[min]-model. ─ ℕ[full] is the standard ℒ[full]-model. ─ T₀ is true ℒ₀-arithmetic. ─ T[min] is true ℒ[min]-arithmetic. ─ T[full] is true ℒ[full]-arithmetic. ∗∗ DEFINITION 4.3. Let L be a language of arithmetic and let φ(x) be an L-formula in the free variable x. The ∗induction instance∗ for φ(x) is the L-sentence IND(φ) :≡ φ(0)∧∀x(φ(x)→φ(x+1))→∀x.φ(x). ∗∗ DEFINITION 4.4. Let L be a language of arithmetic and let T be an L-theory. Let φ(x) be an L-formula in the free variable x. Say that ∗T proves ∀x.φ(x) by necessarily non-analytic induction∗ if and only if there is an L-formula ψ(x) in the free variable x such that (1) T,IND(φ) ⊬ ∀x.φ(x), (2) T ⊢ φ(0), (3) T ⊢ ψ(0), (4) T ⊢ ∀x: ψ(x)→ψ(x+1), (5) T ⊢ ∀x.ψ(x)→∀x.φ(x). Under conditions (1)–(5) we also say that ∗ψ(x) witnesses that T proves ∀x.φ(x) by necessarily non-analytic induction∗. ∗∗ REMARKS. ─ The above definition does not require T to be a theory of arithmetic (that is, T could contain sentences that are false in all standard L-models). I will of course require T to be a theory of arithmetic when using this definition to make precise sense of the necessary non-analyticity of non-analytic induction proofs (of arithmetic) found in the wild. But I do not rule out that there might be interesting uses of the above definition with T not a theory of arithmetic. – As we saw when proving Fact 3.6, an analytic induction proof may be possible once an appropriate lemma has been proved (by induction). Such cases could qualify as necessarily non-analytic induction proofs under Definition 4.4 (and indeed, the proof of Fact 3.6 does, as shown in §8). This is because for any two induction axioms there is always an induction axiom logically equivalent to their conjunction. Thus any proof along the lines of "induction proof of a lemma followed by an analytic induction proof" could be rewritten as a single non-analytic induction proof (but that proof would probably not look very "natural"). In light of this, perhaps I should rethink the terminology, since it might seem a bit inappropriate to call proofs such as the proof of Fact 3.6 for "non-analytic induction proofs". ∗∗ An alternative way of phrasing condition (1), provided by the following lemma, might be more intuitive. ∗∗ LEMMA 4.5. (1) and (2) are equivalent to (2) and (1') T ⊬ ∀x: φ(x)→φ(x+1). PROOF. The direction from left (that is, from (1) and (2)) to right (that is, to (1') and (2)) is immediate. The direction from right to left is an easy (but non-trivial) exercise in propositional logic. □ ∗∗ REMARK. I chose (1) instead of (1') in the definition precisely because the direction (1) ⇒ (1') is immediate (given (2)) while the direction (1') ⇒ (1) (given (2)) is not. ∗∗ When trying to prove that typical T and φ(x) satisfy the above definition, the hardest part will be──as far as I can tell at least──to show condition (1) (or condition (1')). Therefore it makes sense to break out a lemma that captures the idea of using non-standard models to establish (1). ∗∗ LEMMA 4.6. ─ Let L be a language of arithmetic. ─ Let T be an L-theory. ─ Let φ(x) be an L-formula in the free variable x. ─ Suppose T ⊢ φ(n) for all numerals n. The following are then equivalent. ─ T,IND(φ) ⊬ ∀x.φ(x). ─ There is a non-standard L-model M ⊨ T and a non-standard number c in M such that M ⊨ φ(c) and M ⊭ φ(c+1). PROOF. Since T ⊢ φ(0), Lemma 4.5 gives that T,IND(φ) ⊬ ∀x.φ(x) is equivalent to T ⊬ ∀x: φ(x)→φ(x+1), which by soundness and completeness is equivalent to there is M ⊨ T and c in M such that M ⊨ φ(c) and M ⊭ φ(c+1) which, since T ⊢ φ(n) for all numerals n, is equivalent to there is nonstandard M ⊨ T and a non-standard number c in M such that M ⊨ φ(c) and M ⊭ φ(c+1). □ ∗∗ REMARK. The direction from the existence of a non-standard "countermodel" to T,IND(φ) ⊬ ∀x.φ(x) holds even if we drop the requirement (∗) T ⊢ φ(n) for all numerals n. This direction is the one we will use so we need not worry about (∗) when applying the lemma (but nevertheless, (∗) will hold every time we apply the lemma). ∗∗ §5 Fact 2.2 must be proved by non-analytic induction ──────────────────────────────────────────────────── DEFINITION 5.1. The language L₅ of arithmetic is ℒ[full] expanded with the unary function symbol 'f'. ∗∗ REMARK. L₅ is thus an impure language, with impure(L₅) = {f} (and with pure(L₅) = ℒ[full]). ∗∗ DEFINITION 5.2. ─ The L₅-sentences DEF₀(f) and DEF₊(f) are defined by DEF₀(f) :≡ f(0) = 0. DEF₊(f) :≡ ∀x. f(x+1) = f(x)+2x+1. ─ The theory T₅ of L₅-arithmetic is defined by T₅ :≡ T[full],DEF₀(f),DEF₊(f). ─ The L₅-formulas φ₅(x) and ψ₅(x) are defined by φ₅(x) :≡ ∃y. f(x) = y², ψ₅(x) :≡ f(x) = x². ∗∗ The reader who finds the following fact puzzling or even contradictory might want to jump ahead to the remark after the proof. ∗∗ FACT 5.3. ψ₅(x) witnesses that T₅ proves ∀x.φ₅(x) by necessarily non-analytic induction. PROOF. We need to show (1)–(5) of Definition 4.4. (2)–(5) are easy. To show (1) we appeal to Lemma 4.6 and exhibit a non-standard L₅-model M ⊨ T₅ with an element c such that M ⊨ φ₅(c) and M ⊭ φ₅(c+1). The following construction is due to Matt Kaufmann (private communication). Let M₀ ⊨ T[full] be a non-standard ℒ[full]-model and let c be any non-standard number in M₀. We expand M₀ to an L₅-model M by defining the interpretation fᴹ : M₀ → M₀ as follows. fᴹ(n) := n²-9c² if n = 5c+z for some integer z, fᴹ(n) := n² otherwise. We need to verify that this definition is well-formed──that is, we need to verify that n²-9c² is never negative when n = 5c+z for some integer z. We have fᴹ(5c+z) = (5c+z)²-9c² = 25c²+10zc+z²-9c² = 16c²+10zc+z² = c(16c+10z)+z² which is positive since c > 0 (since c is non-standard), 16c+10z > 0 (since c is non-standard and z is not), z² ≥ 0 (since z² is c square). With fᴹ so defined it is easy to verify that M ⊨ T₅. We have M ⊨ φ₅(5c) since φ₅(5c) = (5c)²-16c² = 25c²-16c² = 9c² = (3c)². It remains to show M ⊭ φ₅(5c+1). We have φ₅(5c+1) = (5c+1)²-16c² = 25c²+10c+1-16c² = 9c²+10c+1. This is not a perfect square in M since ∀x∀y: x > 0 → 9x²+10x+1 ≠ y² is a theorem of T[full]. Thus we have M ⊭ φ₅(5c+1). □ ∗∗ REMARK. Fact 5.3 might seem contradictory. After all, there is a unique standard L₅-model, namely ℕ[full] with f interpreted by f₂ (from §2), and in this model ∀x.φ₅(x) is of course true. The catch is that T₅ is weaker than the theory of this standard model, since T₅ does not contain any induction axioms involving the symbol f. In particular, T₅ does not prove that f is equal to f₂ (which, being a function ℕ → ℕ, is a symbol of ℒ[full] and thus also of L₅). For more discussion of this phenomenon see §9. ∗∗ The following alternative proof of Fact 5.3 might be useful for the reader, since it demonstrates the proof idea used in §6, but in a simpler setting. The alternative proof is roughly the following. Suppose we have a non-standard model M ⊨ T₅-DEF₀(f) with a non-standard c such that M ⊨ φ₅(c) and M ⊭ φ₅(c+1). Whether M ⊨ DEF₀(f) holds depends only on the values fᴹ takes on the standard numbers. Furthermore, whether DEF₊(f) holds on the non-standard numbers does not depend on the values fᴹ takes on the standard numbers. Thus, by reinterpreting (if necessary) f only on the standard numbers of M, we can turn M into a model M' ⊨ T₅. Since fᴹ and fᴹ' will then agree on the non-standard numbers, we will have M' ⊨ φ₅(c) and M' ⊭ φ₅(c+1). Thus, appealing to Lemma 4.6 (and the fact that conditions (2)–(5) of Definition 4.4 are easy), we are done. Thus to prove Fact 5.3 it suffices to construct such a non-standard model M, which can be done by applying the compactness theorem in the usual way. In more detail, we do as follows. ∗∗ DEFINITION 5.4. ─ L₅' is L₅ expanded with the constant symbol 'c'. ─ The L₅'-theories T₅' and T₅'' are defined by T₅' :≡ T₅,φ₅(c),¬φ₅(c+1),c>0,c>1,c>2,... T₅'' :≡ T₅'-DEF₀(f). ∗∗ LEMMA 5.5. If T₅'' has a model then so does T₅'. PROOF. Suppose M ⊨ T₅''. We construct an L₅'-model N from M by reinterpreting f: fᴺ(0) := 0, fᴺ(n+1) := fᴺ(n)+2n+1 if n is standard, fᴺ(n) := fᴹ(n) if n is non-standard. Then we have N ⊨ T₅', as the reader can easily verify. □ ∗∗ To construct the model required to apply Lemma 5.5 we will use the compactness theorem. For each natural number m we will provide an L₅'-expansion N(m) ⊨ T₅'' of ℕ[full] with cᴺ⁽ᵐ⁾ = m. This shows that any finite fragment of T₅'' has a model (namely, N(m) for a large enough m). Thus the whole of T₅'' has a model, by the compactness theorem. A key to the construction of the models N(m) is that since DEF₀(f) is omitted from T₅'', we need not set fᴺ⁽ᵐ⁾(0) := 0. It turns out that setting fᴺ⁽ᵐ⁾(0) := 2m+1 (while obeying DEF₊(f)) we get that fᴺ⁽ᵐ⁾(m) is a perfect square while fᴺ⁽ᵐ⁾(m+1) is not. ∗∗ DEFINITION 5.6. For each natural number m, the function βₘ : ℕ → ℕ is defined recursively by βₘ(0) := 2m+1, βₘ(n+1) := βₘ(n)+2n+1. ∗∗ LEMMA 5.7. For all natural numbers m: βₘ(m) = (m+1)². PROOF. See §B. □ ∗∗ LEMMA 5.8. For all natural numbers m: βₘ(m+1) is not a perfect square. PROOF. See §B. □ ∗∗ DEFINITION 5.9. For any natural number m, N(m) is the L₅'-expansion of ℕ[full] defined by fᴺ⁽ᵐ⁾ := βₘ, cᴺ⁽ᵐ⁾ := m. ∗∗ LEMMA 5.10. For all natural numbers m: (1) N(m) ⊨ T[full], (2) N(m) ⊨ DEF₊(f), (3) N(m) ⊨ φ(c), (4) N(m) ⊨ ¬φ(c+1). PROOF. We have (1) since N(m) is an ℕ[full]-expansion. We have (2) immediately from definitions (Definitions 5.2, 5.4, 5.6 and 5.9). We have (3) and (4) by Lemmas 5.7 and 5.8, respectively. □ ∗∗ ALTERNATIVE PROOF OF FACT 5.3. By Lemmas 4.6 and 5.5 (and since (2)–(5) of Definition 4.4 are easy) it suffices to exhibit a model of T₅''. Let T be a finite fragment of T₅''. Then we have N(m) ⊨ T for m sufficiently large, by Lemma 5.10 (and Definitions 5.2, 5.4 and 5.9). Thus any finite fragment of T'' has a model and thus, by compactness, so does T₅. □ ∗∗ §6 Fact 2.4 must be proved by non-analytic induction ──────────────────────────────────────────────────── Since Fact 2.4 is a statement involving rationals, a little work is needed to phrase it as a natural statement in first-order arithmetic (that is, without involving any coding). ∗∗ DEFINITION 6.1. g₆ : ℕ → ℕ and h₆ : ℕ → ℕ are defined recursively by g₆(0) := 1, g₆(n+1) := (n+2)²g₆(n)+h₆(n), h₆(0) := 1, h₆(n+1) := (n+2)²h₆(n). ∗∗ By induction, we have g₂(n) = g₆(n)/h₆(n) so the inequality g₂(n) < 2 can be rewritten as g₆(n) < 2h₆(n). Similarly, the inequality g₂(n) ≤ 2-(n+1)⁻¹ becomes (n+1)g₆(n) ≤ (2n+1)h₆(n). ∗∗ All in all, we have the following rephrasings of Fact 2.4 and its proof attempt and proof. ∗∗ LEMMA 6.2. For all natural numbers n, if (n+1)g₆(n) ≤ (2n+1)h₆(n) then g₆(n) < 2h₆(n). PROOF. Suppose (n+1)g₆(n) ≤ (2n+1)h₆(n). Since (2n+1)h₆(n) < 2(n+1)h₆(n) we then have (n+1)g₆(n) < 2(n+1)h₆(n) so we must have g₆(n) < 2h₆(n). □ ∗∗ FACT 6.3. g₆(n) < 2h₆(n) for all n. PROOF ATTEMPT. Induction on n. ─ Base case: g₆(0) = 1 (by Definition 6.1) < 2 = 2×1 = 2h₆(0) (by Definition 6.1). ─ Induction step: g₆(n+1) = (n+2)²g₆(n)+h₆(n) (by Definition 6.1) < (n+2)²×2h₆(n)+h₆(n) (by induction hypothesis) But for any n we have (n+2)²×2h₆(n)+h₆(n) ≮ 2h₆(n+1) = 2(n+2)²h₆(n). Thus we are "stuck". ACTUAL PROOF. By Lemma 6.2, it suffices to prove (n+1)g₆(n) ≤ (2n+1)h₆(n) for all n. We prove this by induction on n. ─ Base case: (0+1)g₆(0) = (0+1)×1 (by Definition 6.1) = 1 ≤ 1 = (2×0+1)×1 = (2×0+1)h₆(0) (by Definition 6.1). ─ Induction step: Our induction hypothesis is (IH) (n+1)g₆(n) ≤ (2n+1)h₆(n) and we must show (GOAL) (n+2)g₆(n+1) ≤ (2n+3)h₆(n+1). We have (n+2)g₆(n+1) = (n+2)((n+2)²g₆(n)+h₆(n)) (by Definition 6.1) = (n+2)³g₆(n)+(n+2)h₆(n) and (2n+3)h₆(n+1) = (2n+3)(n+2)²h₆(n) (by Definition 6.1) = (2n+3)(n+2)(n+2)h₆(n) = (2n²+7n+6)(n+2)h₆(n) = (2n²+7n+5)(n+2)h₆(n)+(n+2)h₆(n) so (GOAL) is equivalent to (n+2)³g₆(n) ≤ (2n²+7n+5)(n+2)h₆(n), which is equivalent to (n+2)²g₆(n) ≤ (2n²+7n+5)h₆(n), which we have by (n+2)²g₆(n) = ((n+1)+1)²g₆(n) = ((n+1)²+2(n+1)+1)g₆(n) = ((n+1)²+2(n+1))g₆(n)+g₆(n) = (n+3)(n+1)g₆(n)+g₆(n) ≤ (n+3)(2n+1)h₆(n)+g₆(n) (by (IH)) ≤ (n+3)(2n+1)h₆(n)+2h₆(n) (by Lemma 6.2 and (IH)) = (2n²+7n+5)h₆(n). □ ∗∗ REMARK. I find it a bit curious that the proof of Fact 2.4 uses only one application of the induction hypothesis, while the above proof of Fact 6.3 uses two applications. Is there a proof of Fact 6.3 which, in some sensible precise sense, uses only one application of the induction hypothesis? ∗∗ DEFINITION 6.4. ─ The language L₆ of arithmetic is ℒ[full] expanded with the unary function symbols 'g' and 'h'. ─ The L₆-sentences DEF₀(g), DEF₊(g), DEF₀(h) and DEF₊(h) are defined by DEF₀(g) :≡ g(0) = 1, DEF₊(g) :≡ ∀x. g(x+1) = (x+2)²×g(x)+h(x), DEF₀(h) :≡ h(0) = 1, DEF₊(h) :≡ ∀x. h(x+1) = (x+2)²×h(x). ─ The theory T₆ of L₆-arithmetic is defined by T₆ :≡ T[full],DEF₀(g),DEF₊(g),DEF₀(h),DEF₊(h). ─ The L₆-formulas φ₆(x) and ψ₆(x) are defined by φ₆(x) :≡ g(x) < 2×h(x), ψ₆(x) :≡ (x+1)×g(x)+h(x) ≤ 2×(x+1)×h(x). ∗∗ FACT 6.5. ψ₆(x) witnesses that T₆ proves ∀x.φ₆(x) by necessarily non-analytic induction. ∗∗ To prove Fact 6.5 we will proceed similarly to the alternative proof of Fact 5.3. ∗∗ DEFINITION 6.6. ─ L₆' is L₆ expanded with the constant symbol 'c'. ─ The L₆'-theories T₆' and T₆'' are defined by T₆' :≡ T₆,φ₆(c),¬φ₆(c+1),c>0,c>1,c>2,... T₆'' :≡ T₆'-DEF₀(g). ∗∗ LEMMA 6.7. If T₆'' has a model then so does T₆'. PROOF. Similar to the proof of Lemma 5.5. □ ∗∗ To easier make sense of the following two definitions, first recall that g₂ : ℕ → ℚ was recursively defined (in §2) such that for all n: g₂(n) = 1+2⁻²+3⁻²+⋅⋅⋅+(n+1)⁻². Then recall Euler's famous solution to "the Basel problem" (Lemma C.1): g₂(n) → π²/6 as n → ∞. ∗∗ DEFINITION 6.8. For each natural number m, ξₘ : ℕ → ℝ is defined by ξₘ(n) := 2+(m+1)⁻¹+g₂(n)-π²/6. ∗∗ DEFINITION 6.9. For each natural number m, γₘ : ℕ → ℝ is defined recursively by γₘ(0) := 3+(m+1)⁻¹-π²/6, γₘ(n+1) := (n+2)²γₘ(n)+h₆(n). ∗∗ LEMMA 6.10. For all natural numbers m: γₘ(n)/h₆(n) = ξₘ(n). PROOF. See §C. □ ∗∗ LEMMA 6.11. For each natural number m there is a unique natural number n such that ξₘ(n) < 2 and ξₘ(n+1) ≮ 2. PROOF. See §C. □ ∗∗ DEFINITION 6.12. μ : ℕ → ℕ μ(m) := the n such that ξₘ(n) < 2 and ξₘ(n+1) ≮ 2. ∗∗ LEMMA 6.13. μ is unbounded. PROOF. See §C. ∗∗ We now reuse the notation 'N(m)' (that is, Definition 5.9 does not apply anymore). ∗∗ DEFINITION 6.14. For each natural number m, N(m) is the L₆'-expansion of ℕ[full] defined by gᴺ⁽ᵐ⁾ := γₘ, hᴺ⁽ᵐ⁾ := h₆, cᴺ⁽ᵐ⁾ := μ(m). ∗∗ LEMMA 6.15. For all natural numbers m: (a) N(m) ⊨ T[full], (b) N(m) ⊨ DEF₊(g), (c) N(m) ⊨ DEF₀(h), (d) N(m) ⊨ DEF₊(h), (e) N(m) ⊨ φ₆(c), (f) N(m) ⊨ ¬φ₆(c+1). PROOF. We have (a) since N(m) is an ℕ[full]-expansion. We have (b) by Definitions 6.4, 6.9 and 6.14. We have (c) and (d) by Definitions 6.1, 6.4 and 6.14. By Lemma 6.10 (and Definitions 6.4 and 6.14), (e) and (f) are equivalent to ξₘ(μ(m)) < 2 and ξₘ(μ(m)+1) ≮ 2, respectively, which we have by Definition 6.12. □ ∗∗ LEMMA 6.16. T₆'' has a model. PROOF. Let T be a finite fragment of T₆''. By Lemmas 6.13 and 6.15 (and by Definitions 6.4, 6.6 and 6.14), we have N(m) ⊨ T for m sufficiently large. Thus any finite fragment of T₆'' has a model and thus, by compactness, T₆'' has a model. □ ∗∗ PROOF OF FACT 6.5. Conditions (2)–(5) of Definition 4.4 are easy. Condition (1) follows from Lemmas 4.6, 6.7 and 6.16. □ ∗∗ Is there a "more direct" construction of a non-standard model satisfying the conditions of Lemma 4.6? I have not been able to come up with one. We might try to adapt the method used to prove Fact 5.3──that is, we might try to cleverly expand an arbitrary non-standard ℒ[full]-model M₀ ⊨ T[full] to an L₆-model M ⊨ T₆ such that there is a non-standard c such that M ⊨ φ₆(c) and M ⊭ φ₆(c+1). Thus we need a c in M₀ and interpetations gᴹ,hᴹ : M₀ → M₀ such that (a) gᴹ(0) = hᴹ(0) = 1, (b) for all n in M₀: ─ gᴹ(n+1) = (n+2)²gᴹ(n)+hᴹ(n), ─ hᴹ(n+1) = (n+2)²hᴹ(n), (c) gᴹ(c) < 2hᴹ(c), (d) gᴹ(c+1) ≮ 2hᴹ(c+1). By (c) we must have hᴹ(c) ≠ 0. Then we must have hᴹ(c) = hᴹ((c-1)+1) = (c+1)²hᴹ(c-1) (by (b)) = (c+1)²hᴹ((c-2)+1) = (c+1)²c²hᴹ(c-2) (by (b)) = (c+1)²c²(c-1)²hᴹ(c-3) (by (b)) = (c+1)²c²(c-1)²(c-2)²hᴹ(c-4) (by (b)) ⋮ Thus it is necessary that hᴹ(c) is non-zero and divisible by each of (c+1)²,c²,(c-1)²,(c-2)²,... We get similar requirements on gᴹ. This makes it tricky to come up with explicit definitions that simultaneously satisfy (a)–(d)──or at least, I have not been able to do so. ∗∗ §7 Fact 3.2c must be proved by non-analytic induction ───────────────────────────────────────────────────── DEFINITION 7.1. ─ The language L₇ of arithmetic is ℒ[full] expanded with the binary function symbol 'acc₇'. ─ The L₇-sentence DEF(acc₇) is defined by DEF(acc₇) :≡ ∀a. acc₇(a,0) = a ∧ ∀a∀x. acc₇(a,x+1) = acc₇(a×(x+1),x). ─ The theory T₇ of L₇-arithmetic is defined by T₇ :≡ T[full],DEF(acc₇). ─ The L₇-formulas φ₇(x) and ψ₇(x) are defined by φ₇(x) :≡ x! = acc₇(1,x), ψ₇(x) :≡ ∀a. acc₇(a,x) = a×x!. ∗∗ FACT 7.2. ψ₇(x) witnesses that T₇ proves ∀x.φ₇(x) by necessarily non-analytic induction. ∗∗ To prove Fact 7.2 we will proceed as in the proof of Fact 5.3. Conditions (2)–(5) of Definition 4.4 are straightforward. To prove (1) we take any non-standard model M₀ ⊨ T[full] and expand it to an L₇-model M, interpreting acc₇ such that we get M ⊨ T₇ and a non-standard c such that M ⊨ φ₇(c) and M ⊭ φ₇(c+1). ∗∗ ASSUMPTION 7.3. ─ Let M₀ ⊨ T[full] be a non-standard ℒ[full]-model. ─ Let c be a non-standard number in M₀. ∗∗ We will expand M₀ to an L₇-model M ⊨ T₇ such that M ⊨ φ₇(c) and M ⊭ φ₇(c+1). The defining equations for acc₇ (that is, the sentence DEF(acc₇)) fix all its interpretations acc₇ᴹ(a,n) where n is standard. For non-standard n we have quite some leeway. To achieve M ⊨ φ₇(c) and M ⊭ φ₇(c+1) we will put acc₇ᴹ(1,c) := c! and acc₇ᴹ(1,c+1) := 0. These together with the second conjunct of DEF(acc₇) then gives c! = acc₇ᴹ(1,c) = acc₇ᴹ(c,c-1) = acc₇ᴹ(c(c-1),c-2) = acc₇ᴹ(c(c-1)(c-2),c-3) ⋮ respectively 0 = acc₇ᴹ(1,c+1), = acc₇ᴹ(c+1,c), = acc₇ᴹ((c+1)c,c-1), = acc₇ᴹ((c+1)c(c-1),c-2), = acc₇ᴹ((c+1)c(c-1)(c-2),c-3), ⋮ The defining equations impose no further restrictions so we can put acc₇ᴹ(n,m) := 0 for all yet to be defined cases. ∗∗ We will now make the construction in the preceding paragraph precise. ∗∗ DEFINITION 7.4. ─ The set A ⊆ M₀² is defined by A := {(a,n) : n is standard}, ─ The set B ⊆ M₀² is defined inductively by (a,n+1) is in B ─────────────── ──────────────────── (1,c) is in B (a(n+1),n) is in B . ─ The set C ⊆ M₀² is defined by C := M₀²-(A∪B). ∗∗ REMARK. The elements of B are thus (1,c), (c,c-1), (c(c-1),c-2), (c(c-1)(c-2),c-3), ⋮ ∗∗ LEMMA 7.5. A, B and C partitions M₀². PROOF. Clearly: ─ A∪B∪C = M₀². ─ C is disjoint from A and from B. It thus remains to show that A and B are disjoint. If (a,n) is in A then n is standard but if (a,n) is in B then n is non-standard. Thus A and B have no common elements and thus they are disjoint. □ ∗∗ By Lemma 7.5 the following definition is well-formed. ∗∗ DEFINITION 7.6. acc₇ᴹ : M₀² → M₀ is defined by acc₇ᴹ(a,n) := a×n! if n is standard, acc₇ᴹ(a,n) := c! if (a,n) is in B, acc₇ᴹ(a,n) := 0 if (a,n) is in C. ∗∗ LEMMA 7.7. Let X be A, B or C. For all a and n in M₀, (a,n+1) is in X if and only if (a(n+1),n) is. PROOF. It suffices to show this for X = A and X = B (since then it must hold for C, by definition of C). ─ Case X = A: (a,n+1) is in A iff n+1 is standard iff n is standard iff (a(n+1),n) is in A. ─ Case X = B: The 'only if' direction holds by definition. For the 'if' direction, suppose (a(n+1),n) is in B. Case splitting on the inductive definition of B gives the following. ─ Case (a(n+1),n) = (1,c): Then n = c and a(n+1) = 1, so a(c+1) = 1 so a = c+1 = 1, so c = 0. Since c is non-standard this is a contradiction so this case is not possible. ─ Case (a(n+1),n) = (a'(n'+1),n') for some a' and n' in M₀ such that (a',n'+1) is in B: Then a(n+1) = a'(n'+1) and n = n' so a(n+1) = a'(n+1) so a = a' (by the appropriate well-known theorem of T[full]). Thus (a,n+1) = (a',n'+1) and since (a',n'+1) is in B so is (a,n+1). □ ∗∗ LEMMA 7.8. For all a and n in M₀, if (a,n) is in B then n ≤ c. PROOF. Induction on "(a,n) is in B". ─ Case (a,n) = (1,c): Immediate. ─ Case (a,n) = (a'(n+1),n) for some a' in M₀ and with induction hypothesis n+1 ≤ c: Immediate. □ ∗∗ LEMMA 7.9. (1) M ⊨ T₇. (2) M ⊨ φ₇(c). (3) M ⊭ φ₇(c+1). PROOF. (1) We need to show: (a) M ⊨ T[full], (b) M ⊨ ∀a. acc₇(a,0) = a, (c) M ⊨ ∀a∀x. acc₇(a,x+1) = acc₇(a×(x+1),x). (a) holds since M is an M₀-expansion. (b) holds by Definition 7.6. For (c), suppose a and n are in M₀. We need to show (∗) acc₇ᴹ(a,n+1) = acc₇ᴹ(a(n+1),n). By Lemma 7.5 it suffices to consider the following cases. ─ Case (a,n+1) is in A: acc₇ᴹ(a,n+1) = a(n+1)! (by Definition 7.6) = a((n+1)n!) (by Definition 3.1c) = (a(n+1))n! (by associativity) = acc₇ᴹ(a(n+1),n) (by Definition 7.6) ─ Case (a,n+1) is in B: Then, by Lemma 7.7, (a(n+1),n) is in B as well so, by Definition 7.6, both sides of (∗) are c! and thus (∗) holds. ─ Case (a,n+1) is in C: Similar to the previous case. (2) We need to show c! = acc₇ᴹ(1,c). Since (1,c) is in B, this holds by Definition 7.6. (3) We need to show (∗) (c+1)! ≠ acc₇ᴹ(1,c+1). c+1 is non-standard so (1,c+1) is not in A. We have c+1 > c, so by Lemma 7.8, (1,c+1) is not in B. Thus (1,c+1) is in C and thus, by Definition 7.6, we have acc₇ᴹ(1,c+1) = 0. Thus (∗) holds since M ⊨ T[full] and ∀x. x! ≠ 0 is a theorem of T[full]. ∗∗ PROOF OF FACT 7.2. We need to show (1)–(5) of Definition 4.4. (1) follows from Lemmas 4.6 and 7.9. (2)–(5) are easy to verify. □ ∗∗ §8 Facts 3.2a, 3.2b and 3.6 must be proved by non-analytic induction ──────────────────────────────────────────────────────────────────── In this section I present a general result which shows that facts like Facts 3.2a and 3.2b must be proved by non-analytic induction. Since Fact 3.6 is a generalization of Facts 3.2a and 3.2b, this means that Fact 3.6 too must be proved by non-analytic induction. The proof method is basically the same as for Fact 7.2, only a bit more complicated. ∗∗ We now reuse '∙' and '∙∙'. They were used in §3 but those usages does thus not apply anymore. ∗∗ ASSUMPTION 8.1. ─ Let ∙ : ℕ² → ℕ. ─ Let n₀ be a natural number. ─ Let M₀ ⊨ T[full] be non-standard ℒ[full]-model. ─ Let c be a non-standard number in M₀. ∗∗ REMARK. In §3 we had the more general ∙ : A×A → A, with A an arbitrary set. Since the notions introduced in §4 only covers arithmetic we now consider only the case A = ℕ, but I do not think there should be any problems generalizing to a more general setting (once the notions in §4 have been appropriately generalized). ∗∗ DEFINITION 8.2. ∙∙ : ℕ² → ℕ is defined recursively by n∙∙0 := n₀, n∙∙(m+1) := (n∙∙m)∙n. ∗∗ DEFINITION 8.3. ─ The language L₈ of arithmetic is ℒ[full] expanded with the ternary function symbol 'acc₈'. ─ The L₈-sentence DEF(acc₈) is defined by DEF(acc₈) :≡ ∀a∀x. acc₈(a,x,0) = a ∧ ∀a∀x∀y. acc₈(a,x,y+1) = acc₈(a∙x,x,y). ─ The theory T₈ of L₈-arithmetic is defined by T₈ :≡ T[full],DEF(acc₈). ─ The L₈-formula φ₈(y) is defined by φ₈(y) :≡ ∀x. acc₈(n₀,x,y) = x∙∙y. ∗∗ Proceeding similarly to §5 and §7, we will expand M₀ to an L₈-model M ⊨ T₈ such that M ⊨ φ(c-1) and M ⊭ φ(c). To achieve M ⊨ φ(c-1) we will put acc₈ᴹ(n₀,n,c-1) := n∙∙(c-1) for all n in M₀. To achieve M ⊭ φ(c) we will put acc₈ᴹ(n₀,n,c) := (n∙∙c)+1 for some n in M₀. Now whether we can do this while satisfying DEF(acc₈) depends on ∙ and n₀. For example, for ∙ = + and n₀ = 0, we would put acc₈ᴹ(0,n,c-1) := n(c-1). To satisfy the second conjunct of DEF(acc₈) we would then need, for all n in M₀, n(c-1) = acc₈ᴹ(0,n,c-1) = acc₈ᴹ(n,n,c-2) = acc₈ᴹ(2n,n,c-3) = acc₈ᴹ(3n,n,c-4) ⋮ and 0 = 0(c-1) = acc₈ᴹ(0,0,c-1) = acc₈ᴹ(0,0,c) = acc₈ᴹ(0,0,c+1) = acc₈ᴹ(0,0,c+2) ⋮ We will now make the construction precise. ∗∗ DEFINITION 8.4. ─ The set A ⊆ M₀³ is defined by A := {(a,n,m) : m is standard}, ─ The set B ⊆ M₀³ is defined inductively by n is in M₀ (a,n,m+1) is in B (a∙n,n,m) is in B ──────────────────── ─────────────────── ─────────────────── (n₀,n,c-1) is in B (a∙n,n,m) is in B (a,n,m+1) is in B . ─ The set C ⊆ M₀³ is defined by C := M₀³-(A∪B). ∗∗ EXAMPLE 8.5. (a) If ∙ = + and n₀ = 0 then B consists of the triples (0,0,c), (0,0,c+1), (0,0,c+2), ⋮ together with all triples that are on one of the forms (0,n,c-1), (n,n,c-2), (2n,n,c-3), (3n,n,c-4), ⋮ (b) If ∙ = × and n₀ = 1 then B consists of the triples (1,1,c), (1,1,c+1), (1,1,c+2), ⋮ together with all triples that are on one of the forms (1,n,c-1), (n,n,c-2), (n²,n,c-3), (n³,n,c-4), ⋮ ∗∗ LEMMA 8.6. A, B and C partitions M₀³. PROOF. Clearly: ─ A∪B∪C = M₀³. ─ C is disjoint from A and from B. It thus remains to show that A and B are disjoint. If (a,n,m) is in A then m is standard but if (a,n,m) is in B then n is non-standard. Thus A and B have no common elements and thus they are disjoint. □ ∗∗ By Lemma 8.6, the following definition is well-formed. ∗∗ DEFINITION 8.7. acc₈ᴹ : M₀³ → M₀ is defined by acc₈ᴹ(a,n,0) := a, acc₈ᴹ(a,n,m+1) := acc₈ᴹ(a∙n,n,m) if m is standard, acc₈ᴹ(a,n,m) := n∙∙(c-1) if (a,n,m) is in B, acc₈ᴹ(a,n,m) := (n∙∙c)+1 if (a,n,m) is in C. ∗∗ LEMMA 8.8. Let X be A, B or C. For all a, n and m in M₀, (a,n,m+1) is in X if and only if (a∙n,n,m) is. PROOF. It suffices to show this for X = A and X = B (since then it must hold for C, by definition of C). For X = B this holds by definition. For X = A: (a,n,m+1) is in A iff m+1 is standard iff m is standard iff (a∙n,n,m) is in A. □ ∗∗ ASSUMPTION 8.9. There is n in M₀ such that (n₀,n,c) is in C. ∗∗ LEMMA 8.10. (1) M ⊨ T₈. (2) M ⊨ φ₈(c-1). (3) M ⊭ φ₈(c). PROOF. (1) We need to show: (a) M ⊨ T[full], (b) M ⊨ ∀a∀x. acc₈(a,x,0) = a, (c) M ⊨ ∀a∀x∀y. acc₈(a,x,y+1) = acc₈(a∙x,x,y). (a) holds since M is an M₀-expansion. (b) holds by Definition 8.6. For (c), suppose a, n and m are in M₀. We need to show (∗) acc₈ᴹ(a,n,m+1) = acc₈ᴹ(a∙n,n,m). By Lemma 8.6 it suffices to consider the following cases. ─ Case (a,n,m+1) is in A: Then (∗) holds by Definition 8.7. ─ Case (a,n,m+1) is in B: Then, by Lemma 8.8, (a∙n,n,m) is in B as well. Thus, by Definition 8.7, both sides of (∗) are equal. ─ Case (a,n,m+1) is in C: Similar to the previous case. (2) We need to show that acc₈ᴹ(n₀,n,c-1) = n∙∙(c-1) for all n in M₀. Since (n₀,n,c-1) is in B for all n in M₀, this holds by Definition 8.7. (3) We need to exhibit an n in M₀ such that acc₈ᴹ(n₀,n,c) ≠ n∙∙c. By Assumption 8.9 we have an n in M₀ such that (n₀,n,c) is in C, so for this n we have acc₈(n₀,n,c) = (n∙∙c)+1 (by Definition 8.7) ≠ n∙∙c (by well-known theorem of T[full]). □ ∗∗ FACT 8.11. With ∙ = + and n₀ = 0, or with ∙ = × and n₀ = 1, T₈ proves ∀y.φ(y) by necessarily non-analytic induction. PROOF. Both cases are similar. We prove the case ∙ = +. We must exhibit an L₈-formula ψ(y) such that conditions (1)–(5) of Definition 4.4 are satisfied. As the proof of Fact 3.2 shows, ψ(y) :≡ ∀a∀x. acc₈(a,x,y) = a+x×y will work. Conditions (2)–(5) are then straightforward. Condition (1) follows from Lemmas 4.6 and 8.10. It remains to verify that Assumption 8.9 is true when ∙ = + and n₀ = 0, which it is since for example (0,1,c) is in C (see Example 8.5a). □ ∗∗ §9 Discussion and future work ───────────────────────────── What does results like Facts 5.3, 6.5, 7.2 and 8.11 tell us about the necessity of non-analytic induction in mathematical practice? Consider, for example, Fact 5.3 and consider a working mathematician who have just introduced the function f₂ : ℕ → ℕ by Definition 2.1──that is, by the recursive definition f₂(0) := 0, f₂(n+1) := f₂(n)+2n+1. Fact 5.3 tells us that if our working mathematician wants to prove──by the means provided by first-order arithmetic──that f₂(n) is a perfect square for all n, then no matter what facts have been previously established, a non-analytic induction proof is necessary (or put differently: a non-analytic induction axiom is needed). As Fact 5.3 shows, even if our working mathematician would somehow have established all first-order facts of arithmetic in a language without 'f₂', a non-analytic induction axiom would still be needed. Thus results like Fact 5.3 say that some non-analytic induction proofs are necessarily non-analytic in this rather strong sense. ∗∗ PA⁻, in the language ℒ₀, is "the theory of the non-negative parts of discretely ordered commutative rings" (see §A). Hetzl and Wong (2017) consider the problem of finding non-analytic induction proofs from PA⁻. This is motivated by the fact that for any ℒ₀-sentence σ, if PA ⊢ σ then there is a φ(x) such that PA⁻,IND(φ) ⊢ σ. In previous work, we stated and proved Facts 5.3 and 7.2 with PA⁻ instead of T[full] (in the definition of T₅ and T₇, respectively). Naturally, one might wonder whether one could always replace PA⁻ with T[full] in such results. This is not the case for trivial reasons: facts formulated using only ℒ₀ might need non-analytic induction axioms added to PA⁻ to be provable, but these non-analytic induction axioms are of course already in T[full]. Facts 5.3, 6.5, 7.2 and 8.11 concern results formulated in an impure language. Perhaps one could find some general criterion that says that for some class of statements in such languages, if PA⁻,T proves them by necessarily non-analytic induction then so does T[full],T (where T would typically consist of axioms governing the symbols from the impure part of the language). For example one could investigate the following conjecture, which is inspired by Facts 7.2 and 8.11. ∗∗ CONJECTURE 9.1. ─ Let L be ℒ[full] expanded with the (n+m)-ary function symbol 'f'. ─ Let T be an L-theory of arithmetic. ─ Let t₁,...,tₙ be closed ℒ₀-terms. ─ Let t(x₁,...,xₘ) be an ℒ₀-term. ─ Suppose PA⁻,T proves σ :≡ ∀x₁⋅⋅⋅∀xₘ. t(x₁,...,xₘ) = f(t₁,...,tₙ,x₁,...,xₘ). by necessarily non-analytic induction. Then T[full],T proves σ by necessarily non-analytic induction. ∗∗ To more systematically settle whether different facts require non-analytic induction proofs one could attempt to establish more general results──instead of hand-crafting countermodels for each particular case. This might be difficult. As a starting point one could try to develop general methods and results for comparatively simple theories, like fragments of Presburger arithmetic. ∗∗ Another possible future line of work would be to consider other settings than arithmetic. For example, in computer science, many basic facts about functions on inductive structures seem to require non-analytic induction proofs. ∗∗ One might also approach the problem of non-analytic induction proofs from the more proof-theoretical side, for example by studying derivations in natural deduction. Dag Prawitz's (2018) recent work might be useful. ∗∗ §A Some definitions and results ─────────────────────────────── DEFINITION A.1. The ℒ₀-theory PA⁻ is axiomatized by the following. ─ 0 and 1 are distinct: 0 ≠ 1. ─ Associativity of addition and multiplication: (x+y)+z = x+(y+z), (x×y)×z = x×(y×z). ─ Commutativity of addition and multiplication: x+y = y+x, x×y = y×x. ─ Distributivity of addition over multiplication: x×(y+z) = x×y+x×z. ─ 0 is an additive identity and a multiplicative zero: x+0 = x, x×0 = 0. ─ The order is irreflexive: x ≮ x. ─ The order is transitive: x < y ∧ y < z → x < z. ─ The order is total: x < y ∨ x = y ∨ y < x. ─ The order is discrete: x = 0 ∨ x = 1 ∨ 1 < x. ─ Addition and multiplication respect the order: x < y → x+z < y+z, x < y ∧ 0 ≠ z → x×z < y×z. ─ Smaller elements can be subtracted from larger elements: x < y → ∃z. x+z = y. ∗∗ FACT A.2. ─ For all ℒ₀-structures M: M ⊨ PA⁻ if and only if M is the non-negative part of a nontrivial discretely ordered commutative ring. ─ PA⁻ is a theory of ℒ₀-arithmetic. ─ PA ≡ PA⁻+{IND(φ) : φ an ℒ₀-formula in one free variable}. PROOFS. See for example Chapter 2 of Kaye's (1991) book. □ ∗∗ §B Proofs of Lemmas 5.7 and 5.8 ─────────────────────────────── LEMMA B.1. For all natural numbers m and n: βₘ₊₁(n) = βₘ(n)+2. PROOF. Induction on n. ─ Base case: βₘ₊₁(0) = 2(m+1)+1 (by Definition 5.6) = (2m+1)+2 = βₘ(0)+2 (by Definition 5.6). ─ Induction step: βₘ₊₁(n+1) = βₘ₊₁(n)+2n+1 (by Definition 5.6) = βₘ(n)+2+2n+1 (by induction hypothesis) = (βₘ(n)+2n+1)+2 = βₘ(n+1)+2 (by Definition 5.6). □ ∗∗ LEMMA 5.7. For all natural numbers m: βₘ(m) = (m+1)². PROOF. Induction on m. ─ Base case: βₘ(0) = 2×0+1 (by Definition 5.6) = (0+1)². ─ Induction step: βₘ₊₁(m+1) = βₘ(m+1)+2 (by Lemma B.1) = βₘ(m)+2m+1+2 (by Definition 5.6) = βₘ(m)+2m+3 = (m+1)²+2m+3 (by induction hypothesis) = (m+2)² = ((m+1)+1)². □ ∗∗ LEMMA 5.8. For all natural numbers m: βₘ(m+1) is not a perfect square. PROOF. We have βₘ(m+1) = βₘ(m)+2m+1 (by Definition 5.6) = (m+1)²+2m+1 (by Lemma 5.7) = (m+2)²-2. Thus we have (m+1)² < βₘ(m+1) < (m+2)². Thus βₘ(m+1) is not a perfect square. □ ∗∗ §C Proofs of Lemmas 6.10, 6.11 and 6.13 ─────────────────────────────────────── LEMMA C.1. g₂(n) → π²/6 as n → ∞. PROOF. This is Euler's (1740) famous solution to "the Basel problem". □ ∗∗ LEMMA C.2. For each natural number m, ξₘ(n) → 2+(m+1)⁻¹ as n → ∞. PROOF. Immediate from Lemma C.1 and Definition 6.8. □ ∗∗ LEMMA C.3. For each natural number n there is a natural number m such that ξₘ(n) < 2. PROOF. Let n be a natural number. By Lemma C.1 and since g₂ is strictly increasing we have (∗) g₂(n) = π²/6-ε for some ε > 0. Thus for any m we have ξₘ(n) = 2+(m+1)⁻¹+g₂(n)-π²/6 (by Definition 6.8) = 2+(m+1)⁻¹+π²/6-ε-π²/6 (by (∗)) = 2+(m+1)⁻¹-ε. Thus for m large enough, ξₘ(n) < 2. □ ∗∗ LEMMA 6.10. For all natural numbers m: γₘ(n)/h₆(n) = ξₘ(n). PROOF. Induction on n. ─ Base case: γₘ(0)/h₆(0) = (3+(m+1)⁻¹-π²/6)/1 (by Definitions 6.1 and 6.9) = 2+(m+1)⁻¹+1-π²/6 = 2+(m+1)⁻¹+g₂(0)-π²/6 (by Definition 2.3) = ξₘ(0) (by Definition 6.8). ─ Induction step: γₘ(n+1)/h₆(n+1) = ((n+2)²γₘ(n)+h₆(n))/((n+2)²h₆(n)) (by Definitions 6.1 and 6.9) = γₘ(n)/h₆(n)+(n+2)⁻² = ξₘ(n)+(n+2)⁻² (by induction hypothesis) = 2+(m+1)⁻¹+g₂(n)-π²/6+(n+2)⁻² (by Definition 6.8) = 2+(m+1)⁻¹+g₂(n)+(n+2)⁻²-π²/6 = 2+(m+1)⁻¹+g₂(n+1)-π²/6 (by Definition 2.3) = ξₘ(n+1) (by Definition 6.8). □ ∗∗ LEMMA 6.11. For each natural number m there is a unique natural number n such that ξₘ(n) < 2 and ξₘ(n+1) ≮ 2. PROOF. Let m be any natural number. By Lemma C.2 there is a natural number n' such that ξₘ(n') > 2. Since ξₘ(0) < 2 we thus have a natural number n < n' such that ξₘ(n) < 2 and ξₘ(n+1) ≮ 2. Since ξₘ is strictly increasing n must be unique. □ ∗∗ LEMMA 6.13. μ is unbounded. PROOF. We show that for any m there is k such that μ(k) > μ(m). Let m be any natural number. By Lemma C.3 there is a natural number k such that (∗) ξₖ(μ(m)+1) < 2. Thus μ(k) ≥ μ(m)+1 (by Definition 6.12 and (∗) and since ξₖ is increasing) > μ(m). □ ∗∗ References ────────── Euler, Leonhard (1740): "De summis serierum reciprocarum", Commentarii academiae scientiarum Petropolitanae 7, pp. 123-134. Hetzl, Stefan and Tin Lok Wong (2017): "Some observations on the logical foundations of inductive theorem proving", Logical Methods in Computer Science 13(4). Kaye, Richard (1991): "Models of Peano arithmetic". Clarendon Press. Prawitz, Dag (2018): "The concepts of proof and ground", preprint.