Questions tagged [predicativity]

Use this tag for questions about the logical concept of predicativism, which is the rejection of self-referential definitions, or impredicativity. This may be used to refer to the implementation of polymorphism or induction/recursion in some systems.

Filter by
Sorted by
Tagged with
14 votes
1 answer

Why not have `Prop : Set` in Coq?

My understanding of Coq is that Prop : Type_1, Set : Type_1, and then Type_1 : Type_2, ...
10 votes
0 answers

Unintentionally proven false theorem with type-in-type outside logic and foundations?

We are all familiar with Russell's paradox, and it is known that Per Martin-Löf proved that type-in-type is normalizing and consistent (which is false), by accidentally using an assumption in his meta-...
  • 427
10 votes
1 answer

What is the role of impredicativity in program extraction?

Is impredicativity useful for program extraction in Coq? For example is there some kind of realizability argument that depends on impredicativity? Of course it doesn't seem to be necessary for program ...
  • 1,868
18 votes
1 answer

Proof-theoretic comparison table?

I read this CSTheory SE post, which suggests that it is often not clear what variant of MLTT or CIC is being referred to. But I would like to know the proof-theoretic strengths of the various ...
  • 427
5 votes
1 answer

Understanding the complete lattice definition of impredicativity

This is a nice definition of (one notion of?) impredicativity and is mentioned directly here and in one of the sections of the answer here (although I'm probably misinterpreting Andrej Bauer's answer)....
  • 2,593
15 votes
2 answers

What are the advantages to impredicativity?

Mostly when I read about impredicativity I see people bemoaning its downsides. But it's not clear to me why I would want impredicativity in the first place. Impredicativity is useful for analyzing ...
17 votes
2 answers

What is the trade-off to accepting impredicative propositions?

Impredicativity greatly increases the logical strength of a formal system, and impredicative propositions are also a consequence of various axioms including LEM and Zorn's Lemma. An impredicative sort ...
35 votes
3 answers

What is predicativity?

Type systems, and the proof assistants based on them, are frequently divided into predicative and impredicative. What exactly does this mean? I've heard the slogan "impredicativity means you can'...
  • 2,593