Correctness of proof by induction
Short answer: Proof by induction is correct because we define the natural integers as the set for which proof by induction works.

On your interpretations and examples

Your understanding seems broadly correct, though there are a few places where your statements are not fully rigorous. Given that we're talking about logic, getting things precisely right is important.


You should mention that you're working in the domain of integers (naturals, to be precise, which are the nonnegative integers). Induction doesn't work on many larger domains such as real numbers.
When proving a property of the form $\forall n \gt 0, \ldots$, the case $n=0$ does not come up. The basic induction principle applies to all natural numbers: if $P(0)$ and $\forall n \in \mathbb{N}, (P(n) \to P(n+1))$ then $\forall n \in \mathbb{N}, P(n)$. Other statements such as “if $P(1)$ and $\forall n \in \mathbb{N}, (n \ge 1 \to (P(n) \to P(n+1)))$ then $\forall n \in \mathbb{N}, (n \ge 1 \to P(n))$” are also true (and easy to derive from one another).
“$P(n)$ is valid for $n:=n+1$” is not a rigorous statement since the last occurrence of $n$ is not covered by any quantifier. The proper way to write this is “for any natural $n$, if $P(n)$ holds then $P(n+1)$ holds”.
Regarding your second question, it isn't clear what you mean by “and, in fact, …”. It is not the case, for example, that $P(0) \wedge (\forall n \in \mathbb{N}, P(n) \to P(n+2))$ implies $\forall n, P(n)$ — these hypotheses only prove that the property holds on even integers.
Finally, this isn't a matter of rigor, but your choice of example is odd, as $n^2$ is normally defined as $n*n$ — so after expanding the definition, the property to prove becomes $\forall n \gt 0, n * n = n * n$, which doesn't need induction. A better elementary example would be $\forall n \in \mathbb{N}, n + 1 = 1 + n$.


The Peano axioms

Now, to turn to why proof by induction works. It is impossible to answer this question rigorously without explicitly stating how the natural numbers are defined, or what properties of the natural numbers we define. Many definitions exist.

One definition of the natural numbers is the Peano axioms. There are many minor variants of the Peano axioms; one (which assumes equality as a preexisting notion) is:


$0$ is a natural.
For every natural $n$, $S(n)$ is a natural.
For every natural $n$, $0 \ne S(n)$.
For every natural $n$ and $m$, if $S(m) = S(n)$ then $m = n$.
Let $P$ be any unary predicate over the naturals. Suppose that $P(0)$ is true and that for every natural $n$, if $P(n)$ is true then $P(S(n))$ is true. Then for every natural $n$, $P(n)$ is true.


The first two axioms describe ways to build naturals. The next two axioms state that naturals built in different ways are distinct. (Exercise: find a model where all the axioms hold except for #3. Maybe a bit harder: find a model where all the axioms hold except for #4.)

As you can see, with this axiomatisation of the naturals, the induction principle is an axiom.

If you try to define the naturals as a subset of the reals, you'll run into foundational trouble: where do the reals comes from, and how do you prove properties of them? For example, it's difficult to reason about sequences of reals (or anything else) without induction.

The most common foundation of mathematics is set theory, specifically, ZF (Zermelo-Fraenkel). From ZF, a common way to define naturals is as Von Neumann ordinals:


$0$ is the empty set: $0 := \varnothing$
the successor of an ordinal is the union of that ordinal with the singleton containing it: $S(n) := n \cup \{n\}$.


The existence of the empty set is guaranteed by any set theory that proves the existence of at least one set and even a weak version of the axiom of comprehension. The existence of a successor is guaranteed by pairing to prove the existence of $\{n\}$ (which is an abbreviated notation for the pair $\{n,n\}$), and one to prove and union to deduce the existence of $n \cup \{n\}$. This suffices to prove the existence of all the natural numbers.

In order to prove that all the natural numbers form a set, an additional axiom is needed. It can be stated as “the natural numbers form a set”. Usually, the axiom is formulated as “the exists an inifinite set”. This more general formulation does not guarantee that the natural numbers obtained by this construction form a set — there are models of ZF where the smallest infinite set contains more than just zero and its successors, called non-standard models. I won't dwell on these models; doing logic in these models tends to be somewhat non-intuitive, but they are nice in that they allow rigorous reasoning about “infinitesimally large” integers, and from there about infinitesimally small numbers such as the $\mathrm{d}x$ in $\dfrac{\mathrm{d}x}{\mathrm{d}t}$ beloved of physicists.

Let's call a set $x$ supernatural (this is not standard terminology) if it contains $0$ and if for any $y \in x$, $S(y) \in x$. A supernatural set contains all the naturals, and perhaps more. A common formulation of the axiom of infinity is that there exists a supernatural set; we'll assume that. Let $\mathbb{O}$ be a supernatural set.

Now let $\mathbb{N}$ be the intersection of all the supernatural subsets of $\mathbb{O}$. Since all the supernatural sets contain $0$ and there is at least one element in the family ($\mathbb{O}$ itself), $0 \in \mathbb{N}$. For any $n \in \mathbb{N}$, $n$ is a member of each supernatural subset of $\mathbb{O}$, therefore (by definition of supernatural sets) so is $S(n)$. Thus $\mathbb{N}$ itself is supernatural. We'll call this set the set of naturals. Intuitively speaking, $\mathbb{N}$ is the smallest set containing the naturals (though without further axioms it is not necessarily unique, e.g. in nonstandard models).

$\mathbb{N}$ satisfies the induction principle. To see this, consider a predicate $P$ over the naturals, such that $P(0)$ is true and for all $n \in \mathbb{N}$, $P(n)$ implies $P(n+1)$. Let $\mathbb{N}_P$ be the set of naturals that satisfy $P$, i.e. $\mathbb{N}_P = \{n \in \mathbb{N} \mid P(n)\}$. Then $\mathbb{N}_P$ is a supernatural set, so $\mathbb{N} \subseteq \mathbb{N}_P$ by definition of $\mathbb{N}$.

Other foundations of mathematics

There are foundations of mathematics that are not based on set theory. What you consider the foundations vs derived theorems is not important: as long as you prove that your foundations are equally consistent with one of the commonly accepted ones, you're doing the same mathematics as everyone else. The definition of $\mathbb{N}$ as a set of ordinals is merely one way to construct it. The Peano axioms (or any equivalent formulation) are the specification of the naturals, and it is this specification that defines $\mathbb{N}$, rather than any particular construction.

In particular, constructive foundations of mathematics tend to treat the naturals as the most fundamental notion, and the induction principle on naturals, or on some more general structures, as a foundational axiom. For example, in homotopy type theory, the Peano axioms are a consequence of the rules for constructing functions by recursion. In intuitionistic type theory with inductive types (e.g. in the calculus of inductive constructions, which is the foundation of the Coq proof assistant), the induction principle on naturals is an instance of the more general induction principle that holds on any constructed type.