A NOTE ON NECESSARILY NON-ANALYTIC INDUCTION PROOFS ─────────────────────────────────────────────────── Anders Lundstedt (anders.lundstedt@philosophy.su.se) 2019–06–12 §0 Preliminaries ──────────────── DEFINITIONS. – L₀ is the first-order language with signature ⟨0,1,+⟩. – Any first-order language that is an expansion of L₀ is a ∗(first-order) language of arithmetic∗. – L₁ is the ∗(first-order) language of ordered rings∗──signature ⟨0,1,+,⋅,<⟩. – The ∗standard model of arithmetic∗ is the L₁-model with domain ℕ and the expected interpretation of each symbol. – An L₁-model is ∗non-standard∗ if and only if it is not isomorphic to the standard model. – Let L be a language of arithmetic and let M be an L-model. – The ∗standard natural numbers∗ of M are the denotations of all terms of the form 0+1+⋅⋅⋅+1 (0 or more 1's). – An element of M is a ∗non-standard natural number∗ if and only if it is not a standard natural number. – The L₁-theory ∗true L₁-arithmetic∗, notation T₁, is the theory of the standard model of arithmetic. – 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). – 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. ∗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∗. ∗∗ §1 Introduction ─────────────── The purpose of this note is to show that the following two facts must be proved by non-analytic induction in a rather strong sense. ∗∗ FACT 1.1. Define f : ℕ → ℕ recursively by f(0) := 0, f(n+1) := f(n)+2n+1. Then f(n) is a perfect square for all natural numbers n. ∗∗ FACT 1.2. Define f : ℕ → ℕ recursively by f(0) := 1, f(n+1) := (n+1)f(n+1). Define g : ℕ×ℕ → ℕ recursively by g(0,m) := m, g(n+1,m) := g(n,(n+1)m). Then f(n) = g(n,1) for all natural numbers n. ∗∗ Even if we assume all of T₁ (that is, true arithmetic in the language ⟨0,1,+,⋅,<⟩), both these facts——if formulated by suitably expanding L₁ with function symbols——must be proved by non-analytic induction. This might seem counterintuitive: The involved functions are definable in T₁ and formulated using defining formulas, both facts are indeed theorems of T₁. But if we expand the language and add the defining equations for each function, then T₁ cannot prove that equations using the new function symbols are equivalent to their corresponding formulations using their defining formulas, since T₁ does not contain any induction axioms containing the new function symbols. ∗∗ The results can in fact be strengthened a bit further: Take any language L extending L₁ and consider the L-theory T of true arithmetic (suitably defined for that language). Then as long as we formulate the facts using fresh (that is, not in L) function symbols then T proves both facts by necessarily non-analytic induction. To avoid having to deal with how to define "true arithmetic" for arbitrary languages I will not prove these strengthenings. ∗∗ §2 The sum of any initial segment of the odd natural numbers is a perfect square ──────────────────────────────────────────────────────────────────────────────── DEFINITIONS. – The first-order language L₂ is L₁ expanded with the unary function symbol 'f₂'. – φ₂(x) :≡ ∃y: f₂(x) = y². – ψ₂(x) :≡ f₂(x) = x². – The first-order theory T₂ is the L₂-theory consisting of T₁ together with the ∗the defining equations for f₂∗ f₂(0) = 0, ∀x: f₂(x+1) = f₂(x)+2⋅x+1. ∗∗ FACT 2.1. ψ₂(x) witnesses that T₂ proves ∀x.φ₂(x) by necessarily non-analytic induction. PROOF. We need to show (1)–(5) of the definition. (2)–(5) are easy. To show (1), that is T₂,IND(φ₂) ⊭ ∀x.φ₂(x), we will exhibit an L₂-model M ⊨ T₂ with an element a such that M ⊨ φ₂(a) and M ⊭ φ₂(a+1). The following construction is due to Matt Kaufmann. Let M₀ ⊨ T₁ be a non-standard model and let a be any non-standard natural number in M₀. We expand M₀ to an L₂-model M by defining the interpretation f₂ᴹ : M₀ → M₀ as follows. f₂ᴹ(n) := n²-9a² if n = 5a+z for some integer z, f₂ᴹ(n) := n² otherwise. We need to verify that this definition is well-formed; that is, that n²-9a² is never negative when n = 5a+z for some integer z. We have f₂ᴹ(5a+z) = (5a+z)²-9a² = 25a²+10za+z²-9a² = 16a²+10za+z² = a(16a+10z)+z² which is positive since a > 0 (since a is non-standard), 16a+10z > 0 (since a is non-standard and z is not), z² ≥ 0 (since z² is a square). With f₂ᴹ so defined it is easy to verify that M ⊨ T₂. We have M ⊨ φ₂(5a) since φ₂(5a) = (5a)²-16a² = 25a²-16a² = 9a² = (3a)². It remains to show M ⊭ φ₂(5a+1). We have φ₂(5a+1) = (5a+1)²-16a² = 25a²+10a+1-16a² = 9a²+10a+1. This is not a perfect square in M since ∀x∀y: x > 0 → 9x²+10x+1 ≠ y² is a theorem of T₁. Thus we have M ⊭ φ₂(5a+1). □ ∗∗ §3 A tail-recursive factorial is equivalent to the standard factorial ───────────────────────────────────────────────────────────────────── DEFINITIONS. – The first-order language L₃ is L₁ expanded with the unary function symbols 'f₃' and 'g₃'. – φ₃(x) :≡ f₃(x) = g₃(x,1). – ψ₃(x) :≡ ∀y: y⋅f₃(x) = g₃(x,y). – The first-order theory T₃ is the L₃-theory consisting of T₁ together with the ∗the defining equations for f₃∗ f₃(0) = 1, ∀x: f₃(x+1) = (x+1)⋅f₃(x) and ∗the defining equations for g₃∗ ∀y: g₃(0,y) = y, ∀x∀y: g₃(x+1,y) = g₃(x,(x+1)⋅y). ∗∗ FACT 3.1. ψ₃(x) witnesses that T₃ proves ∀x.φ₃(x) by necessarily non-analytic induction. ∗∗ To prove Fact 3.1 we will proceed as in the previous section. Conditions (2)–(5) of the definition are straightforward. To prove (1) we take any non-standard model M₀ ⊨ T₁ and expand it to an L₃-model M, interpreting f₃ and g₃ such that we get M ⊨ T₃ and a non-standard a such that M ⊨ φ₃(a) and M ⊭ φ₃(a+1). ∗∗ ASSUMPTIONS. – Let M₀ ⊨ T₁ be a non-standard model. – Let a be a non-standard number in M₀. ∗∗ We will expand M₀ to an L₃-model M ⊨ T₃ such that M ⊨ φ₃(a-1) and M ⊭ φ₃(a). The defining equations for f₃ fix its interpretation on the standard natural numbers. For non-standard numbers c we will simply put f₃ᴹ(c) := 0 (which does satisfy the defining equations). The defining equations for g₃ fix all its interpretations g₃ᴹ(n,m) where n is standard. For non-standard n we have quite some leeway. To achieve M ⊨ φ₃(a-1) and M ⊭ φ₃(a) we will put g₃ᴹ(a-1,1) := 0 and g₃ᴹ(a,1) := 1. These together with the second defining equation for g₃ gives 0 = g₃ᴹ(a-1,1) = g₃ᴹ(a-2,a-1) = g₃ᴹ(a-3,(a-1)(a-2)) = g₃ᴹ(a-4,(a-1)(a-2)(a-3)) ⋮ respectively 1 = g₃ᴹ(a,1) = g₃ᴹ(a-1,a) = g₃ᴹ(a-2,a(a-1)), = g₃ᴹ(a-3,a(a-1)(a-2)) ⋮ The defining equations impose no further restrictions so we can put g₃ᴹ(c,d) := 0 for all yet to be defined cases. ∗∗ I will now make the construction in the preceding paragraph more precise. ∗∗ DEFINITION. f₃ᴹ : M₀ → M₀ is defined by f₃ᴹ(0) := 1, f₃ᴹ(n+1) := (n+1)f₃ᴹ(n) if n is standard, f₃(c) := 0 if c is non-standard. ∗∗ DEFINITIONS. – The set A ⊆ M₀×M₀ is defined by A := {(n,m) : n,m∈M and n is standard}, – The set B ⊆ M₀×M₀ is defined inductively by (n+1,m) is in B ─────────────── ──────────────────── (a,1) is in B (n,(n+1)m) is in B . – The set C ⊆ M₀×M₀ is defined by C := M₀×M₀ - (A∪B). ∗∗ REMARK. The elements of B are thus (a,1), (a-1,a), (a-2,a(a-1)), (a-3,a(a-1)(a-2)), ⋮ ∗∗ LEMMA 3.2. A, B and C partitions M₀×M₀. PROOF. Clearly: – A∪B∪C = M₀×M₀. – C is disjoint from A and from B. It thus remains to show that A and B are disjoint. If (n,m) is in A then n is standard but if (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 3.2 the following definition is well-formed. ∗∗ DEFINITION. g₃ᴹ : M₀×M₀ → M₀ is defined by g₃ᴹ(0,c) := c, g₃ᴹ(n+1,c) := g₃ᴹ(n,(n+1)c) if n is standard, g₃ᴹ(b,c) := 1 if (b,c) is in B, g₃ᴹ(b,c) := 0 if (b,c) is in C. ∗∗ LEMMA 3.3. Let X be A, B or C. For all n and m in X, (n+1,m) is in X if and only if (n,(n+1)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). – Case X = A: (n+1,m) is in A iff n+1 is standard iff n is standard iff (n,(n+1)m) is in A. – Case X = B: The 'only if' direction holds by definition. For the 'if' direction, suppose (n,(n+1)m) is in B. Case splitting on the inductive definition of B gives the following. – Case (n,(n+1)m) = (a,1): Then n = a and (n+1)m = 1, so (a+1)m = 1 so a+1 = m = 1, so a = 0. Since a is non-standard this is a contradiction so this case is not possible. – Case (n,(n+1)m) = (n',(n'+1)m') for some n' and m' in M₀ such that (n'+1,m') is in B: Trivial. □ ∗∗ LEMMA 3.4. (1) M ⊨ T₃. (2) M ⊨ φ₃(a-1). (3) M ⊭ φ₃(a). PROOF. (1) We need to show: (a) M ⊨ T₁, (b) M ⊨ f₃(0) = 1, (c) M ⊨ ∀x: f₃(x+1) = (x+1)⋅f₃(x) (d) M ⊨ ∀y: g₃(0,y) = y, (e) M ⊨ ∀x∀y: g₃(x+1,y) = g₃(x,(x+1)⋅y). (a) holds since M is an M₀-expansion. (b) and (d) holds by definition of f₃ᴹ and g₃ᴹ, respectively. It remains to show (c) and (e). (c) Suppose n is in M. We want to show f₃ᴹ(n+1) = (n+1)f₃ᴹ(n). If n is standard then this holds by definition. If n is non-standard then, by definition, both sides of the equation are 0 and thus equal. (e) Suppose n and m is in M₀. We need to show (∗) g₃ᴹ(n+1,m) = g₃ᴹ(n,(n+1)m). By Lemma 3.2 it suffices to consider the following cases. – Case (n+1,m) is in A: (∗) holds by definition of g₃ᴹ. – Case (n+1,m) is in B: Then, by Lemma 3.3, (n,(n+1)m) is in B as well so, by definition of g₃ᴹ, both sides of (∗) are 1 and thus (∗) holds. – Case (n+1,m) is in C: Similar to the previous case. (2) We need to show (∗) f₃ᴹ(a-1) = g₃ᴹ(a-1,1). We have f₃ᴹ(a-1) = 0 by definition. We have that (a-1,1) is in C, so g₃ᴹ(a-1) = 0 by definition. Thus (∗) holds. (3) We need to show (∗) f₃ᴹ(a) ≠ g₃ᴹ(a,1). Again, we have f₃ᴹ(a) = 0 by definition. We have that (a,1) is in B, so g₃ᴹ(a,1) = 1 by definition. Thus (∗) holds. □ ∗∗ PROOF OF FACT 3.1. We need to show (1)–(5) of the definition. (1) follows from Lemma 3.4. (2)–(5) are easy to verify. □ ∗∗ §4 Conclusion ───────────── These results are improvements of previous results, where in Facts 2.1 and 3.1 we had PA⁻ instead of T₁ (PA⁻ is "the theory of the non-negative parts of nontrivial discretely ordered commutative rings"). Naturally, one might wonder if it is always the case that such results can be strengthened by replacing PA⁻ with T₁. This is not the case for trivial reasons: If we formulate Facts 1.1 and 1.2 in L₁——that is, using defining formulas and not fresh function symbols——then both formulations are of course theorems of T₁. Requiring use of an expanded language would of course not suffice either, since we could just add some validity in the expanded language to our formulas. But perhaps there is some criterion for when it is indeed the case that PA⁻ can be replaced with T₁. That would be a really interesting result and is something I think is worth looking into.