Mathematical Induction in constructive setting

Question

I'm little confused. As we don't have a proof hence we can't say : let the equation holds till(for) fixed n, and then we are going to show (prove) it holds for n + 1.

From this argument mathematical induction is nearly useless in constructive setting ? Normally we prove nearly 3/4 of stuff using this technique.

The confusion started by diving equality as Extensional Equality and Intentional Equality. where in former case you need a proof and in later case you can just enumerate all possible instances.

Example :

Lets say we are inductively defining Natural Numbers. In extensional equality you have to prove anything about it, so u'll need principle of mathematical induction while in case of Intentional equality u can't use it (Or there is no such principle, {I get to know by Bob Harper's lectures , i might not be presenting facts right}).

My argument are not perfect and might not be completely formal, i'm just a beginner. I have doubts and would love to iteratively understand it. So, stop flagging things as "put on hold". It looks like "Bullying" to me. Stop doing that and just ask or help me to refine my question. Stop showing that you are an elite, its disgusting.

Answer 1

See Richard Dedekind, Stetigkeit und irrationale Zahlen (1872), Engls.translation into:

• Richard Dedekind, Essays on the Theory of Numbers, page 4:

I regard the whole of arithmetic as a necessary, or at least natural, consequence of the simplest arithmetic act, that of counting, and counting itself as nothing else than the successive creation of the infinite series of positive integers in which each individual is defined by the one immediately preceding; the simplest act is the passing from an already-formed individual to the consecutive new one to be formed. The chain of these numbers forms in itself an exceedingly useful instrument for the human mind; it presents an inexhaustible wealth of remarkable laws obtained by the introduction of the four fundamental operations of arithmetic. Addition is the combination of any arbitrary repetitions of the above-mentioned simplest act into a single act; from it in a similar way arises multiplication.

We can see the Axiom of induction as a rule: a sort of "iterated" modus ponens.

For an arithmetical "property" $P$, we start proving the base case:

(1) "$P(0)$ holds";

then we prove the inductive step:

(2) "for $n$ whatever, if $P(n)$ holds, then aso $P(n+1)$ holds".

Having done this, we can "assembly" the two result into an unlmited chain of deductions: first, we have that $P(0)$ holds by (1); then we can "instantiate" (2) to $P(0)→P(1)$ and by modus ponens with $P(0)$ we derive $P(1)$.

Now we use again (2): $P(1)→P(2)$ and by modus ponens again we derive $P(2)$.

And so on. The "and so on" is "built in" into the axiom, and it is the "inner nature" of the progression of natural numbers.