Skip to main content
37 votes
Accepted

What is predicativity?

Impredicativity is one of those soft concepts that appears in many related forms, but it is difficult to explain what precisely they share. Let me try anyhow. Impredicativity allows us to single out, ...
Andrej Bauer's user avatar
  • 9,553
27 votes

Proof-theoretic comparison table?

Here are a few comparisons of dependent type theories with fragments of Peano arithmetic and set theories that I know of: Predicative systems (the MLTT family) Predicative systems are comparable with ...
Loïc Pujet's user avatar
  • 1,479
24 votes
Accepted

Why not have `Prop : Set` in Coq?

As it often happens with Coq, the answer is historical reasons. In the original version dating back from 1984, Coq was based on the Calculus of Constructions, a barebone dependent type theory. In ...
Pierre-Marie Pédrot's user avatar
18 votes

What are the advantages to impredicativity?

All impredicativity means is that propositions form a complete lattice! This is a basic principle of mathematics. So if you want to be able to use the architecture of mathematics developed in the last ...
Neel Krishnaswami's user avatar
15 votes
Accepted

What is the role of impredicativity in program extraction?

I have occasionally thought about this question. My inconclusive conclusion is that impredicativity hinders program extraction. Let me try to give an argument in the context of realizability. I am ...
Andrej Bauer's user avatar
  • 9,553
12 votes
Accepted

Why are impredicative constructions used less in type theory than in material set theory?

Regarding natural numbers, and inductive types (ie. initial algebras of some form) in general, impredicative encodings are inconvenient, as they only specify weakly initial algebras, rather than ...
Meven Lennon-Bertrand's user avatar
10 votes

What is predicativity?

System F allows for function types like $T=\Pi X. X \to X$, where $X$ ranges through all the types. In particular, $T$ is one of them! This means that the usual set-theoretic interpretation of $\Pi (a:...
Trebor's user avatar
  • 4,015
10 votes

What is predicativity?

As I understand it, impredicativity in type theory is unrelated (at least in a formal way) from impredicativity in set theory. The single rule in a type system which makes it impredicative is the ...
Couchy's user avatar
  • 2,241
8 votes
Accepted

What are the advantages to impredicativity?

There are some tricks that only work when you have access to an impredicative universe. They tend to construct "the smallest object" of some kind, without an explicit construction, i.e. a ...
Pierre-Marie Pédrot's user avatar
8 votes
Accepted

What is the trade-off to accepting impredicative propositions?

I think this is mainly not a question about usability, but rather a form of discomfort so as to the foundational status of theories incorporating impredicativity. Indeed, as you mentioned, ...
Meven Lennon-Bertrand's user avatar
7 votes
Accepted

Can we completely erase propositions in the type checker?

The ability to have this kind of "erasure" for propositions is indeed one of the major arguments in favour of having a proper sort of strict propositions (see e.g. Section 9.3 of this ...
Meven Lennon-Bertrand's user avatar
6 votes

What is the trade-off to accepting impredicative propositions?

There's a general principle to keep in mind: Weaker theories have more models Martin Escardo, Paul Taylor or Andrej Bauer will probably be able to supply some cool geometric examples of this, but ...
Neel Krishnaswami's user avatar
6 votes

Why are impredicative constructions used less in type theory than in material set theory?

Induction over impredicative encodings requires internalizing a small amount of parametricity. See https://cedille.github.io/ for an example of a language that does this. Otherwise working around the ...
Ms. Molly Stewart-Gallus's user avatar
6 votes
Accepted

Why can termination checker affect strict Prop in Agda?

After some research I have found a counterexample by Jesper Cockx: ...
ice1000's user avatar
  • 6,256
5 votes

Why are impredicative constructions used less in type theory than in material set theory?

This is not directly an answer to the question, but since two other answers have claimed that impredicative encodings can't satisfy induction principles, I thought someone ought to set the record ...
Mike Shulman's user avatar
  • 3,180
5 votes
Accepted

Understanding the complete lattice definition of impredicativity

You must be careful to distinguish internal and external completeness. First, I think you might be looking for the Lindenbaum-Tarski algebra of monadic first-order logic, and you are asking whether it ...
Andrej Bauer's user avatar
  • 9,553

Only top scored, non community-wiki answers of a minimum length are eligible