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.
12
questions
5
votes
0
answers
185
views
Proof-theoretic strength of HOL compared to predicative dependent types
By HOL I mean something like inference rules of HOL Light with the 3 axioms of infinity, extensionality and choice ($\varepsilon$ operator).
By predicative dependent types, I am thinking of MLTT + W-...
- 497
5
votes
1
answer
160
views
Why can termination checker affect strict Prop in Agda?
In https://dl.acm.org/doi/10.1145/3290316 section 4 (which I believe is a standard reference), the authors claimed that Voevodsky's propositional resizing rule justifies the consistency of an ...
- 5,424
12
votes
3
answers
318
views
Why are impredicative constructions used less in type theory than in material set theory?
Many infinitary objects in (say) ZFC are constructed with impredicative principles. The natural numbers are formed by intersecting every inductive set (whose existence is given by the axiom of ...
- 3,261
6
votes
1
answer
190
views
Can we completely erase propositions in the type checker?
Related question on semantic side: How much of trouble is Lean's failure of normalization, given that logical consistency is not obviously broken?
Suppose we have an impredicative universe of ...
- 5,424
16
votes
1
answer
879
views
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, ...
- 163
13
votes
0
answers
305
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-...
- 455
11
votes
1
answer
553
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 ...
- 2,051
18
votes
1
answer
954
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 ...
- 455
6
votes
1
answer
154
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)....
- 2,651
17
votes
2
answers
375
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 ...
- 2,628
17
votes
2
answers
409
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 ...
- 983
35
votes
3
answers
754
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'...
- 2,651