Often we have questions on this site which ask for a proof of some result without induction.1 It seems that when such a question is posted, it is quite well-understood what is meant by proof avoiding induction.2 But can the meaning of this phrase be precise?
- Is it possible to define formally what do "proof without induction" and "proof using induction" mean?
For example, I would suspect that if the claim contains some object defined by induction, then we would expect that the proof uses induction, too. (Perhaps in some non-obvious way.) In the other words, if we want induction-free proof, we should have induction-free formulation of the theorem. (Although I do not claim that this intuition is correct - as you can see from this question, I cannot give even reasonable formalization of this.)
Examples of claims which are typically shown by induction and which involve objects defined by induction could be:3
- $\sum_{k=1}^n k = \frac{n(n+1)}2$ (We have several posts about this sum, for example this one.)
- If $a_1,\dots,a_n$ are elements of a finite abelian group $G=\{a_1,\dots,a_n\}$ (where $|G|=n$, i.e. no element is listed twice), then $(a_1a_2\dots a_n)^2$ see here
Of course, induction can also be used in proofs where inductive (recursive) definitions are not used in the formulation of the result.4
- If we have some formalization of the distinction between proofs with/without induction, is it possible to prove about some results that induction cannot be avoided in the proof?
- What are some examples of results for which it is proven that any proof will need induction. (For some reasonable meaning of the phrase "need induction".)
Perhaps I could imagine something like this when working with Peano axioms. We could simply omit the induction axiom and ask whether there is a proof using the remaining axioms. (Or whether there is a model in which the claim fails.) However, in this way we restrict ourselves to claims about natural numbers. Moreover, if we want to omit induction axioms, we would have problems already with formulating results which use recursive definitions. (The fact that recursive definitions are possible in Peano Arithmetic is proved using this axiom. Some authors calls this result Recursion Theorem.)
The question becomes more complicated if we move beyond natural numbers. For example, if we are working in ZFC, then there is not an easy way out by just saying: "Let us omit the axiom about induction."
1You can find many such questions. Some of the most popular examples (base on the number of views and score) could be Proving the identity $\sum_{k=1}^n {k^3} = \big(\sum_{k=1}^n k\big)^2$ without induction
2I do not remember seeing some lengthy argument about whether some proof involves induction or not. Just compare that with the guess the next number type of questions. Situation is somewhat similar in that we often intuitively can see whether some answer is correct (or at least reasonable) or not; whether it was the solution intended by the creator of the problem. But such questions almost immediately get the response: "Any number can be an answer. Just take Lagrange interpolation."
3Here $S_n=\sum_{k=1}^n k$ is defined inductively by $S_{n+1}=S_n+(n+1)$. Similarly, we have inductive definition for $a_1a_2\dots a_n$. I think that the well-know proofs use induction in some hidden way. For example, the proof based on $2S_n=(1+\dots+n)+(n+\dots+1)=\underset{\text{$n$-times}}{\underbrace{(n+1)+\dots+(n+1)}}$ used commutativity several times. Similarly in the proof that product of all elements of abelian groups we would use commutativity. If by commutativity we mean that the product of $n$ elements gives the same result when reordered in any way, the formal proof of this fact would be based on induction.
4One example I was able to find quickly: Simple Proof by induction: $9$ divides $n^3 + (n+1)^3 + (n+2)^3$ But I cannot at the moment think of an example where it would be difficult to give a proof without induction.