WHEN MUST ONE USE A NON-ANALYTIC INDUCTION HYPOTHESIS?——SUMMARY OF SOME RESULTS ──────────────────────────────────────────────────────────────────────────────── version: 2019-03-15 Eric Johannesson and Anders Lundstedt eric.johannesson@philosophy.su.se anders.lundstedt@philosophy.su.se §1 Introduction ─────────────── In §2 we give two examples of facts that when proved seem to require "a strengthening of the induction hypothesis". The two facts are: (F1) For all natural numbers n: 1+3+5+⋅⋅⋅+(2n-1) = k² for some natural number k. (F2) For all natural numbers n: 1+1/2²+1/3²+⋅⋅⋅+1/(n+1)² < 2. ∗∗ Hetzl and Wong (2017) have made precise sense of the notion of "proof by using a non-analytic induction hypothesis". (What one might call "proof by a strengthening of the induction hypothesis" is a special case of "proof by using a non-analytic induction hypothesis".) In §3 we present a slight generalization of their formalization. ∗∗ In §4 we show that, using the definition given in §3, there is a precise sense in which (F1) must be proved by "using a non-analytic induction hypothesis". ∗∗ In §5 we present some preliminary results towards proving (or disproving) that (F2), in the sense given by the definition in §3, must be proved by "using a non-analytic induction hypothesis". ∗∗ In §6 we present some ideas for future work. ∗∗ §2 Two results proved by "a strengthening of the induction hypothesis" ────────────────────────────────────────────────────────────────────── For our first case, we have that the sum of any initial segment of the odd 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. f₁ : ℕ → ℕ is recursively defined by f₁(0) := 0, f₁(n+1) := f₁(n)+2n+1. ∗∗ FACT 1. For all natural numbers n: f₁(n) = k² for some natural number k. PROOF ATTEMPT. "Straightforward induction": – Base case: f₁(0) = 0 = 0² (by definitions) so f₁(0) = k² for k = 0. – Induction step: f₁(n+1) = f₁(n)+2n+1 (by definition) = 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 1 is a logical consequence. f₁(n) = n² for all natural numbers n. (This fact is not a logical consequence of Fact 1, so it is stronger than Fact 1 in at least that sense.) We prove this fact by induction. – Base case: f₁(0) = 0² ≡ 0 = 0 (by definitions). – Induction step: f₁(n+1) = f₁(n)+2n+1 (by definition) = n²+2n+1 (by induction hypothesis) = (n+1)² (by elementary arithmetic). □ ∗∗ For our second case, we have 1+1/2²+1/3²+⋅⋅⋅+1/(n+1)² < 2 for all natural numbers n, or, avoiding ellipsis notation, the following. ∗∗ DEFINITION. f₂ : ℕ → ℚ is recursively defined by f₂(0) := 1, f₂(n+1) := f₂(n)+1/(n+2)². ∗∗ FACT 2. f₂(n) < 2 for all natural numbers n. PROOF ATTEMPT. "Straightforward" induction: – Base case: f₂(0) < 2 ≡ 1 < 2 (by definition). – Induction step: f₂(n+1) = f₂(n)+1/(n+2)² (by definition) < 2+1/(n+2)² (by induction hypothesis). But 2+1/(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 f₂(n) ≤ 2-1/(n+1) for all natural numbers n. (In what sense is this fact stronger than Fact 2? It is at least stronger in the sense that for arbitrary f : ℕ → ℚ, f(n) ≤ 2-1/(n+1) for all n implies f(n) < 2 for all n while the converse implication need not hold.) We prove this fact by induction. – Base case: f₂(0) ≤ 2-1/(0+1) ≡ 1 ≤ 1 (by definitions). – Induction step: f₂(n+1) = f₂(n)+1/(n+2)² (by definition) ≤ 2-1/(n+1)+1/(n+2)² (by induction hypothesis) = 2-1/(n+2)-1/(n+1)(n+2)² (by lots of elementary arithmetic) ≤ 2-1/(n+2) (by more or less obvious facts). □ ∗∗ §3 Definitions ────────────── What follows in this section is a reformulation and slight generalization of some of the notions introduced by Hetzl and Wong (2017). ∗∗ DEFINITION. The ∗full (first-order) language of arithmetic∗, notation ℒ[full], is the first-order language that for each natural number n has – a constant symbol n, – a function symbol f of arity n+1 for each function f : ℕⁿ⁺¹ → ℕ, – a relation symbol P of arity n for each relation P ⊆ ℕⁿ. ∗∗ DEFINITION. The ∗minimal (first-order) language of arithmetic∗, notation ℒ[min], is the ℒ[full]-reduct with signature ⟨0,1,+,⋅,<⟩. ∗∗ DEFINITION. A first-order language L is a ∗(first-order) language of arithmetic∗ if and only if L is an ℒ[min]-expansion and an ℒ[full]-reduct. ∗∗ Thus a first-order language of arithmetic has as symbols natural numbers and operations on natural numbers and relations on natural numbers. This is just a convenient "trick" which allows us to easily define the standard model. ∗∗ DEFINITION. Let L be a language of arithmetic. – The ∗standard L-model∗ has domain ℕ and each symbol interpreted as itself. – 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∗. ∗∗ DEFINITION. Let L be a language of arithmetic and let φ(x) be an L-formula with at most one free variable x. The ∗induction instance∗ for φ(x) is the L-sentence IND(φ) :≡ φ(0)∧∀x(φ(x)→φ(x+1))→∀x.φ(x). ∗∗ DEFINITION. Let L be a language of arithmetic and let T be an L-theory. Let φ(x) and ψ(x) be L-formulas both with at most one free variable x. Say that ∗ψ witnesses that T proves ∀x.φ(x) with and only with a non-analytic induction hypothesis∗ if and only if (1) T,IND(φ) ⊬ ∀x.φ(x), (2) T ⊢ φ(0), (3) T ⊢ ψ(0), (4) T ⊢ ∀x,ψ(x)→ψ(x+1), (5) T ⊢ ∀x.ψ(x)→∀x.φ(x). ∗∗ DEFINITION. The ℒ[min]-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 = 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: x < y → ∃z. x+z = y. ∗∗ FACT. For all ℒ[min]-structures M: M ⊨ PA⁻ if and only if M is the non-negative part of a nontrivial discretely ordered commutative ring. ∗∗ FACT. PA⁻ is a theory of arithmetic. ∗∗ FACT. PA = PA⁻∪{IND(φ) : φ an ℒ[min]-formula with at most one free variable} ∗∗ §4 Fact 1 must be proved using a non-analytic induction hypothesis ────────────────────────────────────────────────────────────────── DEFINITION. ℤ[X] := ⟨ℤ[X],0,1,+,⋅,<⟩ is the ordered ring of polynomials with coefficients in ℤ. ∗∗ Elements of ℤ[X] are polynomials z₀+z₁X+z₂X²+⋅⋅⋅+zₙXⁿ with z₀,z₁,...,zₙ in ℤ and if n ≠ 0 then zₙ ≠ 0. These can be divided into the ∗constants∗ polynomials z (z in ℤ) and the ∗non-constant∗ polynomials z+pX (p in ℤ[X], z in ℤ). ∗∗ Addition and multiplication in ℤ[X] are as expected. The order is given by z₀+z₁X+z₂X²+⋅⋅⋅+zₙXⁿ > 0 if and only if zₙ > 0, p > q if and only if p-q > 0. ∗∗ DEFINITION. ℤ[X]⁺ = ⟨ℤ[X]⁺,0,1,+,⋅,<⟩ is the non-negative part of ℤ[X], that is, a polynomial p from ℤ[X] is in ℤ[X]⁺ if and only if p ≥ 0. ∗∗ Elements of ℤ[X]⁺ are polynomials z₀+z₁X+z₂X²+⋅⋅⋅+zₙXⁿ with z₀,z₁,...,zₙ in ℤ and zₙ ≥ 0 and if n ≠ 0 then zₙ ≠ 0. The constant polynomials are n (n in ℕ) and the non-constant polynomials are z+pX (p in ℤ[X], z in ℤ, p > 0). ∗∗ FACT. ℤ[X]⁺ ⊨ PA⁻. PROOF. ℤ[X]⁺ is the is the non-negative part of the nontrivial discretely ordered commutative ring ℤ[X]. □ ∗∗ DEFINITION. The language of arithmetic L₁ is ℒ[min] expanded with the function symbol f₁. ∗∗ DEFINITION. The theory of arithmetic T₁ is defined by T₁ := PA⁻, f₁(0) = 0, ∀x. f₁(x+1) = f₁(x)+2x+1. ∗∗ DEFINITION. The L-formulas φ₁(x) and ψ₁(x) are defined by φ₁(x) :≡ ∃y. f₁(x) = y⋅y, ψ₁(x) :≡ f₁(x) = x⋅x. ∗∗ FACT. ψ₁ witnesses that T₁ proves ∀x.φ₁(x) with and only with a non-analytic induction hypothesis. PROOF. We need to verify conditions (1)–(5). (2) Trivial. (3) Trivial. (4) The proof of Fact 1 given earlier can be straightforwardly formalized in PA⁻. (5) Trivial. (1) We exhibit an L₁-model satisfying T₁ and IND(φ₁) but not ∀x.φ₁(x). Let M be the L₁-expansion of ℤ[X]⁺ with f₁ interpreted as follows. f₁ᴹ(0) := 0, f₁ᴹ(n+1) := f₁ᴹ(n)+2n+1, f₁ᴹ(pX-1) := pX² f₁ᴹ(pX-1+(n+1)) := f₁ᴹ(pX-1+n)+2(pX-1+n)+1, f₁ᴹ(pX-1-(n+1)) := f₁ᴹ(pX-1-n)-2(pX-1-n)+1. The right hand side of the last equation does indeed define a polynomial of ℤ[X]⁺ since by construction the degree of f₁ᴹ(z+pX) is greater than the degree of pX for all integers z and all p in ℤ[X]⁺. (We get the last equation by solving f₁(pX-1-n) = f₁(pX-1-(n+1)+1) = f₁(pX-1-(n+1))+2(pX-1-(n+1))+1 for f₁(pX-1-(n+1)).) We then have f₁ᴹ(X-1) = X² which is a perfect square in M and we have f₁ᴹ(X) = f₁ᴹ(X-1)+2(X-1)+1 = X²+2X-1 which is not a perfect square in M. Thus: – M ⊭ ∀x.φ₁(x) since M ⊭ φ₁(X). – M ⊨ IND(φ₁) since M ⊭ ∀x,φ₁(x)→φ₁(x+1) since M ⊨ φ₁(X) but M ⊭ φ₁(X+1). By construction we also have M ⊨ T₁ so we are done. □ ∗∗ §5 Must Fact 2 be proved using a non-analytic induction hypothesis? ─────────────────────────────────────────────────────────────────── Since Fact 2 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. g : ℕ → ℕ and h : ℕ → ℕ are recursively defined by g(0) := 1, g(n+1) := (n+2)²g(n)+h(n), h(0) := 1, h(n+1) := (n+2)²h(n). ∗∗ We have f₂(n) = g(n)/h(n) so the inequality f₂(n) < 2 can be rewritten as g(n) < 2h(n). Similarly the inequality f₂(n) ≤ 2-1/(n+1) becomes (n+1)g(n) ≤ (2n+1)h(n). ∗∗ All in all, we have the following rephrasings of Fact 2 and its proof attempt and proof. ∗∗ LEMMA. 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 2'. g(n) < 2h(n) for all n. PROOF ATTEMPT. Induction on n. – Base case: g(0) < 2h(0) ≡ 1 < 2⋅1 (by definition) ≡ 1 < 2. – Induction step: g(n+1) = (n+2)²g(n)+h(n) (by definition) < (n+2)²⋅2h(n)+h(n) (by induction hypothesis) But for any n we have (n+2)²⋅2h(n)+h(n) ≮ 2h(n). Thus we are "stuck". ACTUAL PROOF. By the lemma, 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) ≤ (2⋅0+1)h(0) (by definition) ≡ 1⋅1 ≤ 1⋅1 ≡ 1 ≤ 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)) = (n+2)³g(n)+(n+2)h(n) and (2n+3)h(n+1) = (2n+3)(n+2)²h(n) = (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 and (IH)) = (2n²+7n+5)h(n). □ ∗∗ DEFINITION. The language of arithmetic L₂ is ℒ[min] expanded with the function symbols g and h. ∗∗ DEFINITION. The L₂-sentences DEF(g) and DEF(h) and the L₂-formulas φ₂(x) and ψ₂(x) are defined by DEF(g) :≡ g(0) = 1 ∧ ∀x. g(x+1) = (x+2)²⋅g(x)+h(x) DEF(h) :≡ h(0) = 1 ∧ ∀x. h(x+1) = (x+2)²⋅h(x), φ₂(x) :≡ g(x) < 2⋅h(x), ψ₂(x) :≡ (x+1)⋅g(x)+h(x) ≤ 2⋅(x+1)⋅h(x). ∗∗ CONJECTURE. There is an L₂-theory of arithmetic T ⊇ PA⁻ such that (1) T ⊢ DEF(g), (2) T ⊢ DEF(h), (3) ψ₂ witnesses that T proves ∀x.φ₂(x) with and only with a non-analytic induction hypothesis. ∗∗ Adapting the proof of the previous section——cleverly interpreting the new function symbols on ℤ[X]⁺——will not work to settle the above conjecture, as the following results shows. ∗∗ LEMMA. Let M be an L₂-expansion of ℤ[X]⁺ such that M ⊨ DEF(h). Let p be a non-zero polynomial and let z be an integer. If hᴹ(pX+z) ≠ 0 then hᴹ(pX+z-1) ≠ 0 and degree(hᴹ(pX+z)) > degree(hᴹ(pX+z-1)). PROOF. We have hᴹ(pX+z) = (pX+z+1)²hᴹ(pX+z-1) since M ⊨ DEF(h) so clearly if hᴹ(pX+z) ≠ 0 then hᴹ(pX+z-1) ≠ 0 and degree(hᴹ(pX+z)) > degree(hᴹ(pX+z-1)). □ ∗∗ FACT. Let M be an L₂-expansion of ℤ[X]⁺. If M ⊨ DEF(h) then h(p) = 0 for all non-constant polynomials p. PROOF. Suppose h(pX+z) ≠ 0 for some non-constant polynomial pX+z. By the above lemma we then have the contradiction that we have an infinite descending chain degree(hᴹ(pX+z)) > degree(hᴹ(pX+z-1)) > degree(hᴹ(pX+z-2)) > degree(hᴹ(pX+z-3)) ⋮ □ ∗∗ Note that the above results should generalize to any polynomial ring R[X]. Perhaps one could settle the conjecture by considering some ring R[X,X⁻¹] of Laurent polynomials. ∗∗ §5 Future work ────────────── One line of future work would of course be to settle the conjecture in §4. ∗∗ In §3 we expanded ℤ[X]⁺ to a L₁-model in order to show that T₁ proves ∀x.φ₁(x) with and only with a non-analytic induction hypothesis. For each sentence σ of true L₁-arithmetic that is false in ℤ[X]⁺ it is natural to ask whether adding σ to T₁ lets us prove ∀x.φ₁(x) without needing a non-analytic induction hypothesis. One simple sentence of true L₁-arithmetic that is not true in ℤ[X]⁺ is "all numbers are odd or even", that is σ₁ :≡ ∀x∃y, x = y+y ∨ x = y+y+1. ∗∗ CONJECTURE. ψ₁ witnesses that T₁∪{σ₁} proves ∀x.φ₁(x) with and only with a non-analytic induction hypothesis. ∗∗ To more systematically settling conjectures like the one above one could attempt to establish more general results——instead of hand-crafting countermodels for each particular case. We hope that the literature on first-order arithmetic already contains lots of applicable results. ∗∗ Veryfing provability in weak fragments of arithmetic is hard. It is easy to rely on something true that is not provable in the fragment one works with. Thus it would be worthwhile to verify the provability statements in §3 with a theorem prover. ∗∗ An interesting future line of work would be to consider other settings than arithmetic. For example, in computer science, basic facts of operations on inductive structures often seem to require a non-analytic induction hypothesis. ∗∗ 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 may be useful. ∗∗ REFERENCES ────────── Hetzl, Stefan and Tin Lok Wong (2017): "Some observations on the logical foundations of inductive theorem proving", Logical Methods in Computer Science 13(4). Prawitz, Dag (2018): "The concepts of proof and ground", preprint.