Direct Proofs regarding Induction

• Simple Induction
CGandC
Summary:: .

When asked to prove by Induction, I'm asked to prove a statement of the form:
Prove that for all natural numbers ##n##, ## P(n) ##
Which means to prove: ## \forall n ( P(n) ) ## ( suppose the universe of discourse is all the natural numbers )

Then, I see people translating the above statement to the following statement:

## P(0) \land \forall n ( P(n) \rightarrow P(n+1) ) \rightarrow \forall n ( P(n) ) ##
And this is what they are proving. And eventually they say " therefore, it was proven that ## \forall n ( P(n) ) ## by induction "

However, I don't really understand this. This is why:

Let's denote the statement ## \forall n ( P(n) ) ## as ## W ##.
To prove ## \forall n ( P(n) ) ## by induction means to prove ## W ## .

Let's denote the statement ## P(0) \land \forall n ( P(n) \rightarrow P(n+1) ) ## as ## Q ##.
To prove ## P(0) \land \forall n ( P(n) \rightarrow P(n+1) ) \rightarrow \forall n ( P(n) ) ## means to prove ## Q \rightarrow W ##

Now's the problem:

If we prove ## Q \rightarrow W ## then we only prove this implication, we are not proving ## W ##.
Meaning, we are only proving ## P(0) \land \forall n ( P(n) \rightarrow P(n+1) ) \rightarrow \forall n ( P(n) ) ## .
And not ## \forall n ( P(n) ) ##

So how can it be that the problem of proving ## \forall n ( P(n) ) ## is translated into the problem ## P(0) \land \forall n ( P(n) \rightarrow P(n+1) ) \rightarrow \forall n P(n) ## ? Because they are both different statements and thus proving these are different proofs.

SSequence
It seems that you are making it more complicated than it is. I think the basic point is that ##Q \rightarrow W## can be seen as "truth" of predicate logic so to speak. When we are doing proof by induction, our reasoning is of this kind:
1-- We have proven ##Q## to be true
2-- ##Q \rightarrow W## is known to be true

3-- Therefore ##W## is true.

=====================

There is one further small point that comes to my mind.

If we are talking about a first-order theory with domain of discourse as ##\mathbb{N}## then we can write the statement of "induction" exactly as you wrote:
## P(0) \land \forall n ( P(n) \rightarrow P(n+1) ) \rightarrow \forall n [ P(n) ] ##

But if we are, say, talking about a first-order theory (say with single-sort) with domain of discourse that is bigger than ##\mathbb{N}##, then we would have to explicitly write [i.e. if we are being more precise]:
## P(0) \land \forall n \in \mathbb{N} \, ( P(n) \rightarrow P(n+1) ) \rightarrow \forall n \in \mathbb{N} \, [ P(n) ] ##

mfb and CGandC
CGandC
It seems that you are making it more complicated than it is. I think the basic point is that ##Q \rightarrow W## can be seen as "truth" of predicate logic so to speak. When we are doing proof by induction, our reasoning is of this kind:
1-- We have proven ##Q## to be true
2-- ##Q \rightarrow W## is known to be true

3-- Therefore ##W## is true.

Now it makes sense, Thanks. I couldn't have thought that the above 3 statements are interwoven one after another so as to use modus ponens.

Gold Member
With induction, you prove both parts of the conjunction in the antecedent. ##P(0)## is the base step that you prove and ##\forall n(P(n)\rightarrow P(n+1))## is the inductive step that you prove. The statement:
$$[P(0)\wedge \forall n(P(n)\rightarrow P(n+1))]\rightarrow \forall nP(n)$$
is an axiom: the axiom of induction (of which there is one for each predicate). When you prove the base step and the inductive step, the axiom of induction let's you conclude ##\forall nP(n)## by modus ponens.

SSequence
The statement:
$$[P(0)\wedge \forall n(P(n)\rightarrow P(n+1))]\rightarrow \forall nP(n)$$
is an axiom: the axiom of induction (of which there is one for each predicate). When you prove the base step and the inductive step, the axiom of induction let's you conclude ##\forall nP(n)## by modus ponens.
Essentially, you are right. We can always add a statement like:
## P(0) \land \forall n \in \mathbb{N} \, ( P(n) \rightarrow P(n+1) ) \rightarrow \forall n \in \mathbb{N} \, [ P(n) ] ##
as an axiom if we want to.

Though in many number of cases (e.g. in set theory) it would be a theorem [that follows from axioms (or axiom schemas I suppose?) and rules of deduction].

But anyway, I don't think this distinction makes a difference in applying it in actual math. The point being that its truth is what matters.