How can know if a proof technique can actually prove something? Specifically, induction

Induction is an incredible tool to prove some propositions. Although it seems that these propositions require some level of simplicity for us to be able prove them using only induction. If we wanted, for example, to prove Fermat's last theorem using induction on the exponential, I think we would have a hard time.

Regardless of that, if $\phi$ (n) is the statement:$n > 2$ $\land$ $x^n + y^n = z^n$ has no natural solutions. Since Fermat's last theorem is now proved the statement: $\phi (0)$ $ \land $ $\forall x(\phi(x) \implies \phi(x+1))$ is trivially true. (trivially in the sense that it follows directly from Wile's proof of Fermat's last theorem). Then, using in the Induction Scheme, we can conclude that $\forall x \phi (x)$

So, the induction scheme over our statement is provable. But i doubt that anyone would ever be capable of proving Fermat's last theorem using only induction.

Is there a formalization of the concept of "proof technique"? Are there current theories which could, theoretically, prove that if a computer is programmed to only search for proofs using induction, it would never be capable of proving Fermat's last theorem?

I apologize if this question is too vague. If a moderator believes this question is not meant for this website, please delete this.

Edit: In my research I found some paper called "natural proofs", in which it shows that any proof using certain technique, directly related to a combinatorial property, would not be enough to prove that P != NP. But it seems to me, at least in my ignorance, that the proof is too connected with Complexity Theory, and I wouldn't know if we can generalize this for other methods of mathematics. Has this been done before?

Solution 1:

Your question can be made precise in a variety of different ways, but you first need to know logic and Peano Arithmetic (PA). (You can skip these links if you understand the rest of this post.) $\def\nn{\mathbb{N}}$ $\def\t#1{\text{#1}}$ $\def\place#1{\,\boxed{#1}\,}$ $\def\code#1{\underline{#1}}$

Meta-Reasoning

We must always work in some meta-system when talking about proofs. We always choose our meta-system to have the collection of natural numbers, which we call $\nn$, and arithmetic constants $0,1 \in \nn$, and arithmetic operations $+,\times$, such that $(\nn,0,1,+,\times)$ is a model of (first-order) PA (a world satisfying the axioms of PA) and every member of $\nn$ is of the form "$1+1+\cdots+1$". All the mathematics in the rest of this post will be done within the meta-system, where we will talk about other formal systems and what they can or cannot prove.

Induction in general

Induction in the most general sense is the following inference rule:

Given any $1$-parameter sentence $P$ with one natural number parameter:

  If you can deduce both of the following:

    $P(0)$.  

    $\forall n \in \nn\ ( P(n) \to P(n+1) )$.

  Then you can deduce:

    $\forall n \in \nn\ ( P(n) )$.

Here, a $1$-parameter sentence is an expression with blanks, such that filling in the blanks with the same parameter (of the correct type) results in a sentence. Here $P$ requires a parameter that is a natural number, namely a member of $\nn$. We write "$P(t)$" to denote the sentence formed by filling in the blanks in $P$ with the term "$t$". Note that the induction rule is about deduction, not about truth (in the mathematical sense).

For example "$\exists m \in \nn\ \left( \place{1} = 2m \lor \place{1} = 2m+1 \right)$" is a $1$-parameter sentence where all the occurrences of "$\place{1}$" denote the blanks to be filled in, and the result will be a sentence if they are filled in with a natural number. Induction applied to this would say that:

If you can deduce both of the following:

  $\exists m \in \nn\ ( 0 = 2m \lor 0 = 2m+1 )$.

  $\forall n \in \nn\ ( \exists m \in \nn\ ( n = 2m \lor n = 2m+1 ) \to \exists m \in \nn\ ( n+1 = 2m \lor n+1 = 2m+1 ) )$.

Then you can deduce:

  $\forall n \in \nn\ ( \exists m \in \nn\ ( n = 2m \lor n = 2m+1 ) )$.

Indeed we can deduce the two sentences that induction requires in this case (try it!), and hence we can deduce the sentence given by induction, which is in fact a special case of the division-remainder theorem.

Now Fermat's last theorem corresponds to the statement:

$\forall n \in \nn\ ( \t{FLT}(n) )$

  where "$\t{FLT}(n)$" denotes "$n > 2 \to \neg \exists x,y,z \in \nn\ ( x > 0 \land y > 0 \land x^n+y^n=z^n )$".

Indeed since it has been proven (in some powerful formal system), the following can be deduced (in that system) trivially (as you noted):

$\t{FLT}(0)$.

$\forall n \in \nn\ ( \t{FLT}(n) \to \t{FLT}(n+1) )$.

So we could use the induction rule to deduce Fermat's last theorem. But for what? We already have deduced it, so it is pointless to append a few lines consisting of the above deduction just to deduce it again! Instead, what you want to ask is not about induction alone but about the formal system as a whole, specifically what formal systems can deduce the theorem.

One natural candidate that comes to mind is first-order PA, but there are some caveats that I will talk about later. First let us see what induction means for PA.

Induction in first-order PA

Since the language of PA only has $0,1,+,\times$, we can apply induction to only sentences involving these and nothing else. This also means that all the quantifiers are unrestricted, since PA is unable to state anything about $\nn$ or other collections. Specifically, induction in PA is a schema, namely an infinite collection of axioms that form a part of the axioms of PA. This schema includes for every $1$-parameter sentence over PA the following axiom:

$P(0) \land \forall n\ ( P(n) \to P(n+1) ) \to \forall n\ ( P(n) )$.

Note that general induction as described earlier uses restricted quantifiers, and hence is only valid in a system that is able to express statements about the collection $\nn$.

However, you can check that the axioms of PA$^-$ (PA without the induction schema) are sufficient to prove:

$\exists m\ ( 0 = 2m \lor 0 = 2m+1 )$.

$\forall n\ ( \exists m\ ( n = 2m \lor n = 2m+1 ) \to \exists m\ ( n+1 = 2m \lor n+1 = 2m+1 ) )$.

Therefore PA can, by using one of the axioms in the induction schema, deduce:

$\forall n\ ( \exists m\ ( n = 2m \lor n = 2m+1 ) )$.

It turns out that this theorem of PA cannot be proven without using induction, because there is a model of PA$^-$ that does not satisfy this sentence, and so PA$^-$ cannot prove the sentence.

This technique of constructing a model of a formal system $S$ (in this case PA$^-$) that does not satisfy some sentence $A$ (in this case "$\neg \forall n\ ( \exists m\ ( n = 2m \lor n = 2m+1 ) )$") to show that $S$ does not prove $A$ is a very useful technique, though there is no systematic way to construct the model needed.

Fermat's last theorem in weak arithmetic theories

The model-construction technique was used to prove that Fermat's last theorem in various forms cannot be proven in various formal systems. This recent paper states (roughly) the following (page 2):

PA$^-$ plus quantifier-free induction cannot prove "$\t{FLT}(3)$".

  where "$t^3$" is read as "$t \times t \times t$" [the language of PA cannot express exponentiation!].

$\t{Th}(\nn) + \t{Exp}$ cannot prove "$\forall n\ ( \t{FLT}_e(n) )$"

  where $\t{Th}(\nn)$ (the theory of $\nn$) is the collection of all sentences satisfied by $\nn$

  and $e$ is a binary function symbol and $\t{Exp}$ consists of the familiar laws of exponentiation

  and $\t{FLT}_e(n)$ is the same as $\t{FLT}(n)$ except that "$t^n$" is read as "$e(t,n)$".

The problem here that the language of PA cannot talk about exponentiation is an important one. Godel showed as part of the proof of his incompleteness theorems that there is a way to encode finite sequences of natural numbers as single natural numbers such that the encodings can be manipulated by first-order formulae over PA. It implies that there is a $3$-parameter sentence $\t{exp}$ over PA such that for every $a,b,c \in \nn$ we have that $\nn$ satisfies "$\t{exp}(a,b,c)$" iff $a^b = c$. So PA can sort of talk about exponentiation using $\t{exp}$.

The paper asserts (page 1) that it is widely believe that PA can prove Fermat's last theorem. This claim is that:

? PA proves "$\forall n\ ( n > 2 \to \neg \exists x,y,z,p,q,r \in \nn\ ( x > 0 \land y > 0$

$\ \land \t{exp}(x,n,p) \land \t{exp}(y,n,q) \land \t{exp}(z,n,r) \land p+q=r ) )$".

The catch is that there is no way to see that the formulae used in manipulating sequence encodings faithfully represent the manipulation of the sequences themselves, without already having an understanding of sequences! So if (hypothetically) one rejects the meta-system's notions of $\nn$ and sequences from $\nn$, then one might consider $\t{exp}$ to be a meaningless sentence. Similarly, unless one already accepts the existence of the exponential function on $\nn$, the above claim loses its meaning.

This is in my opinion why it is interesting to consider those extensions of PA that explicitly have the exponential function. Exponential function arithmetic (EFA) is one. And if Friedman's conjecture turns out to be true, EFA would prove Fermat's last theorem in its original form (i.e. no encoding needed).