2
$\begingroup$

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

$\endgroup$
5
  • $\begingroup$ λ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). $\endgroup$
    – mohottnad
    Sep 5 '21 at 23:31
  • $\begingroup$ 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? $\endgroup$
    – cjquines
    Sep 6 '21 at 1:11
  • $\begingroup$ 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. $\endgroup$
    – mohottnad
    Sep 6 '21 at 1:36
  • $\begingroup$ 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"? $\endgroup$
    – cjquines
    Sep 6 '21 at 2:52
  • $\begingroup$ 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 $\endgroup$
    – mohottnad
    Sep 6 '21 at 4:06
1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.