Non-Derivability Results in Polymorphic Dependent Type Theory
In the pure Calculus of Constructions (CC) one can define data types and function over these, and there is a powerful higher order logic to reason over these functions and data types. This is due to the combination of impredicativity and dependent types, and most of these features can already be observed in polymorphic (second order) dependent type theory $λ$P2. The impredicative encoding of data types (in $λ$P2 or CC) is powerful but not fully satisfactory: for example, the induction principle is not provable. As a matter of fact, it can be shown that induction is not provable for whatever…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2603.04014
curl -X POST /api/v1/records/arxiv/2603.04014/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2603.04014/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'