In $\lambda P2$, we can write polymorphic functions like $\Lambda A. \lambda x. x: \Pi A. A \to A$. By Curry–Howard, this corresponds to the proposition "for all propositions $A$, $A$ implies $A$". From my understanding, the quantification here is predicative, i.e. "for all propositions" includes the proposition "for all propositions $A$, $A$ implies $A$" itself. Hence, $\lambda P2$ allows quantifying over arbitrary propositions.
If so, then I'm wondering about the difference between $\lambda P2$ and COC. From my understanding, the logical difference between $\lambda P2$ and COC is that COC allows predicates over propositions. Supposedly, $\lambda P2$ logically corresponds to second-order predicate calculus, while COC is higher-order predicate calculus.
But why is $\lambda P2$ only second-order? Isn't a statement like "for all propositions $A$, $A$ implies $A$" already a higher-order statement, because it not only quantifies first-order statements, but also second-order statements, etc.? If not, how does adding predicates over propositions make COC higher-order? What's an example of a higher-order proposition we can make in COC that we can't in $\lambda P2$?
Best Answer
The reason is that quantifying over propositions isn't considered higher-order merely because propositions can contain second-order quantifiers.
In logic, 'order' is measuring to what extent subsets or relations are realized as objects within the logic. In first order logic, only individuals of the domain of discourse are objects. In second order logic, relations on/subsets (of products) of the domain of discourse are objects. Third order logic allows subsets of subsets. And higher order logic is like the limit of this, where any finite iteration of subsets/relations are available as objects.
The propositions in second order logic are allowed to have second order quantifiers. So, in general, the relations/subsets being quantified over may in principle be defined in terms of the collection of 'all' relations. This doesn't make the logic higher order. You could restrict the semantics of the logic more, but it would be a restriction (it would be related to "predicativity"). It's not really different than a first order theory that allows you to specify individuals via formulae that contain first order quantifiers. Such a theory isn't considered higher order because of that.
$λP2$ is second order in this sense because you can quantify over relations via types like $ℕ → ℕ → *$. However, the type of predicates-on-relations would be $(ℕ → ℕ → *) →*$, which is disallowed. But, the calculus of constructions allows this, and further finite iterations, which is the sense in which it matches higher order logic. Quantifying over propositions/$*$ is like quantifying over a 0 arity relation in this sense.