I'm trying to understand higher order logic deduction, and I sort of understand how after going to third order logic and higher you have a type explosion; predicates and functions can have a large variety of types for the arguments and return different types. Generally I understand that these types match usually match predicate or function variables; A fourth order function could I imagine return a second order function variable and take a third order function and a second order predicate as arguments for example.
Is there some notion of quantifying over higher order types as well as objects? Such as 'for all types tau there exists a type mu such that for all objects of type tau and all objects of type mu something' or:
$\forall$$\tau$$\exists$$\mu$: $\forall$x$^\tau$$\forall$y$^\mu$ : $\psi$(x$^\tau$,y$^\mu$)
And then I imagine reason inductively about statements that can apply across varieties of types.
What this does is inject into higher order logic the notion of type polymorphism. Now apparently, polymorphic types can lead to contradictions in theories like type theory if it's unconstrained for the same reason that concepts like 'the set of all sets' can lead to contradictions, but I'm uncertain if just allowing quantification of types creates an inconsistent system on its own.
If type quantification does work, I imagine it's a further extension of the mapping between set theory and higher order logic, and then we need to come up with rules for quantifier elimination (type Skolemization equivalent to the axiom of choice?) and unification across types.
Does this work or does it break for some reason?
