# λP2, the Calculus of Constructions, and quantifying over propositions

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$$?

• λP2 and COC are different in terms of Lambda Cube. COC has all the three dimension rules while λP2 is missing (binding) type operators rule (type families). Sep 5, 2021 at 23:31
• Yes. I think my question was why adding type operators turn it into a higher-order logic? Was it not already a higher-order logic? Sep 6, 2021 at 1:11
• It gives more powerful type system for CoC compared to λP2. Your propositions (as types) may have different kinds of types, like simple types, algebraic types, termed types, dependent types, and typed types (type families). CoC can abstract over all above kinds of types, while λP2 is missing typed types. Sep 6, 2021 at 1:36
• I understand that. The question is about naming. Why do we call it "higher-order" if we can abstract over all kinds of types? In λP2, couldn't we not already abstract over types, and if so, why do we just call it "second-order"? Why does allowing abstracting over type families turn it into "higher-order"? Sep 6, 2021 at 2:52
• In your example "for all propositions A, A implies A" per Curry–Howard, strictly speaking you can only map proposition to intuitionistic proposition/formula. System F (λ2) adds abstraction over polymorphic types (term dependent on type) which is second order. λP2 is also second order by further adds dependent types. However, CoC is higher order since it allows abstraction over types of types (like ranging over sets of sets in 3rd order logic). Induction is not derivable in λP2 (see here), so it's rarely used Sep 6, 2021 at 4:06

$$λ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.