What logic can express induction on natural numbers?

Question

The induction theorem:

$P(0) \land \forall n \in \mathbb{N}\{ P(n) \Rightarrow P(n+1)\} \Rightarrow \forall n \in \mathbb{N} \{P(n)\}$

My understanding is that nature numbers are constructed from sets, and sets are defined by the axioms, with sets and numbers defined, the induction principle should be proved as a theorem, not a axiom.

But two problems:

1. The induction principle quantifies over propositions.

2. Use of proposition-valued functions.

What formalism is able to express these two things?

Answer 1

There are several different ways to formalize the induction principle depending on which setting you're working in, and you seem to have confused yourself slightly by assuming they are supposed to be the same.

In first-order Peano arithmetic, the induction principle is an axiom schema:

Let $\varphi$ be any well-formed formula in the language of arithmetic (usually containing the variable letter $n$ free). Then

$$ \varphi[n\mapsto 0] \land \forall n\bigl(\varphi\to\varphi[n\mapsto S(n)]\bigr ) \to \forall n\,\varphi $$

(where $\varphi[n\to t]$ denotes textually substituting a different term into $\varphi$ for every free occurrence of $n$), is one of the axioms of Peano Arithmetic.

Here it is important to note that the letter $\varphi$ or the substitution operation is not part of the logic: The actual axioms we get out of this contain no "$\varphi$" symbol. The $\varphi$ is just part of the explanation of how to construct the particular strings of symbols that we declare to be axioms.

If we want to prove that, say, adding $1$ to a number is the same as taking its successor, we would use this concrete instance of the axiom scheme: $$ 0+1=S(0) \land \forall n\bigl(n+1=S(n) \to S(n)+1=S(S(n))\bigr) \to \forall n(n+1=S(n)) $$

The second-order Peano axioms are a higher-order theory, which means that we can quantify over predicates in addition to quantifying over individual elements. In that case the induction principle is a single axiom:

$$ \forall P \Bigl( P(0) \land \forall n\bigl(P(n)\to P(S(n))\bigr) \to \forall n\,P(n)\Bigr) $$

That looks a lot like what you've written in the question. In this case you're right that there are "propositional-valued functions", which is another way to say "predicates" -- but that is not a problem, becuase that's exactly what second-order logic can handle.

Second-order logics will usually have some kind of universal instantiation rule that makes each of the instances of the first-order axiom schema a consequence of the second-order induction axiom.

In a set theory such as ZFC, we can't quantify over predicates, but because our individuals in this case are sets, we can still express induction as a single formula:

$$ \forall A\Bigl( 0\in A \land \forall n\bigl( n\in A \to n^+ \in A \bigr) \to \mathbb N\subseteq A \Bigr) $$

This is not an axiom -- rather, given suitable definitions of $0$, $n^{+}$, and $\mathbb N$, it can be proven as a theorem of ZFC. It rests closely on ZFC's axiom of infinity.

Note, incidentally, that the $\in$ symbol in set theory behaves essentially like a "proposition-valued function" of two arguments, too. In a first-order theory such as ZFC, there are predicates, but you can only mention a fixed selection of them given by the language of the theory, and you cannot quantify over them.