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
10 votes
0 answers
149 views

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-...
user avatar
  • 421
10 votes
1 answer
484 views

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 ...
user avatar
  • 1,662
18 votes
1 answer
817 views

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 ...
user avatar
  • 421
5 votes
1 answer
136 views

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)....
user avatar
  • 2,477
14 votes
2 answers
202 views

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 ...
user avatar
17 votes
2 answers
326 views

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 ...
user avatar
32 votes
3 answers
437 views

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'...
user avatar
  • 2,477