I'm trying to understand the Curry-Howard correspondence. I am comfortable with it for propositional logic, but get confused when $\forall, \exists$ quantifiers come in the picture.
The axiom schema of induction (in second-order logic) is $\forall P. \left[(P(0) \implies \forall k\in \mathbb N. (P(k)\implies P(k+1)))\implies \forall n\in \mathbb N. P(n)\right]$.
To my understanding, via Curry-Howard every statement gets translated to a type. Proving a statement means showing that the type is inhabited. For example, +, = are dependent types taking two parameters of type nat; every $\forall k\in A$ gets translated into a dependent product $\prod_{k::A}$. So the axiom schema should become something like $ \left[\prod_{P::?} \left((P\, 0) \rightarrow \left(\prod_{k::\mathbb N} (P \, k)\rightarrow P \, (+\, k\, 1) \right)\right)\right]\rightarrow \prod_{n::\mathbb N}(P \,n) $
A difficulty arises when translating $\forall P$: what is the type of $P$? The problem is that, in order for the above to make sense, $(P\, k)$ is supposed to be a type for all $k::\mathbb N$ (so we are allowed to say $(P\, 0) \rightarrow \cdots$, for instance). So $P$ seems to me like a (dependent) type constructor taking a nat as parameter. But then we are taking a product over $P$, so we must be able to treat $P$ as an element of a type! The problem seems to boil down to, are type constructors themselves of some type? Can we write this statement without having to refer to such a type? Perhaps higher-order logic translates to higher-order type theory, but I do not know the latter. References would also be appreciated.