<p>$\mathrm{Prop}$ is <em>impredicative</em>, which create a very expressive proof system. However it is "too" expressive in the following sense:</p>

<p>$$ \mathrm{impredicative\ Prop} + \mathrm{large\ elimination} + \mathrm{excluded\ middle} $$</p>

<p>is inconsistent. Usually you want to keep the possibility to add the excluded middle, so one solution is to keep large elimination and make Prop predicative. The other is to suppress large elimination.</p>

<p>Coq did both! They renamed the predicative Prop to Set, and disabled large elimination in Prop.</p>

<p>The expressiveness gained by impredicativity is "reassuring" in the sense 99% of "reasonable" mathematics can be formalized with it, and it is known to be consistent relative to set theory. This makes it likely they won't weaken it to something like Agda, which only has predicative universes.</p>

CC BY-SA 3.0
2014-04-01T21:31:10.403Z
Oh and I forgot to mention: it is **not** the case that ``Prop : Prop``, that would be inconsistent. Rather *quantifications* over all propositions is again a proposition.
cody
CC BY-SA 3.0
2017-12-21T20:17:08.320Z
Could you point me to any more resources about this?  Everything I can find seems very scattered.
user833970
CC BY-SA 3.0
2017-12-23T09:36:25.990Z
@user833970 any specific things you'd like pointers to? I'm afraid there isn't really an all encompassing reference for meta theory of dependent types. This discussion (which points back here!) might be useful: https://github.com/FStarLang/FStar/issues/360
cody
CC BY-SA 3.0
2017-12-23T22:48:50.817Z
thank, I'm working through the Berardi paradox paper now, I think that will clear up my confusion.
user833970
CC BY-SA 3.0
2014-04-01T21:29:57.507Z
2014-04-01T21:44:49.283Z
2014-04-01T21:44:49.283Z
cody
<p>Even if you are not interested in extracting programs, the fact that <code>Prop</code> is impredicative allows you to build some models which you can't build using a predicative tower of universes. IIRC Thorsten Altenkirch has a model of System F using Coq's impredicativity.</p>

CC BY-SA 3.0
2014-03-31T11:21:37.960Z
2014-03-31T11:21:37.960Z
gallais
<p>The principle of propositions-as-types (or formulas-as-types), also known as the Curry-Howard correspondence, is the key idea for viewing (intuitionistic) type theories as logical systems and to apply type theories (and constructive mathematics in general) to computer science.
Suppose U is the type of all propositions, then U is also the type of all types by the identification. Therefore, type U of all types naturally occurs and, in particular, it is the type of itself.
In Martin-Löf's (predicative) type theory, propositions and types
are still identified, but the type of all types is replaced by an infinite sequence of type universes U0 U 1: U2..... Hence, one can not quantify over all propositions or predicates, although quantification over each universe is allowed.</p>
<p>That's the reason type and prop are separated. Without this separation the resulting system becomes inconsistent.</p>

CC BY-SA 4.0
2021-04-08T22:43:54.643Z
2021-04-09T10:48:15.487Z
2021-04-09T10:48:15.487Z
Postmortem
<p><span class="math-container">$\mathtt{Prop}$</span> is very useful for program extraction because it allows us to delete parts of code that are useless. For example, to extract a sorting algorithm we would prove the statement &quot;for every list <span class="math-container">$\ell$</span> there is a list <span class="math-container">$k$</span> such that <span class="math-container">$k$</span> is ordered and <span class="math-container">$k$</span> is a permutatiom of <span class="math-container">$\ell$</span>&quot;. If we write this down in Coq and extract without using <span class="math-container">$\mathtt{Prop}$</span>, we will get:</p>
<ol>
<li>&quot;for all <span class="math-container">$\ell$</span> there is <span class="math-container">$k$</span>&quot; will give us a map <code>sort</code> which takes lists to lists,</li>
<li>&quot;such that <span class="math-container">$k$</span> is ordered&quot; will give a funciton <code>verify</code> which runs through <span class="math-container">$k$</span> and checks that it is sorted, and</li>
<li>&quot;<span class="math-container">$k$</span> is a permutation of <span class="math-container">$\ell$</span>&quot; will give a permutation <code>pi</code> which takes <span class="math-container">$\ell$</span> to <span class="math-container">$k$</span>. Note that <code>pi</code> is not just a mapping, but also the inverse mapping together with programs verifying that the two maps really are inverses.</li>
</ol>
<p>While the extra stuff is not totally useless, in many applications we want to get rid of it and keep just <code>sort</code>. This can be accomplished if we use <span class="math-container">$\mathtt{Prop}$</span> to state &quot;<span class="math-container">$k$</span> is ordered&quot; and &quot;<span class="math-container">$k$</span> is a permutation of <span class="math-container">$\ell$</span>&quot;, but <em>not</em> &quot;for all <span class="math-container">$\ell$</span> there is <span class="math-container">$k$</span>&quot;.</p>
<p>In general, a common way to extract code is to consider a statement of the form <span class="math-container">$\forall x : A \,.\, \exists y : B \,.\, \phi(x, y)$</span> where <span class="math-container">$x$</span> is input, <span class="math-container">$y$</span> is output, and <span class="math-container">$\phi(x,y)$</span> explains what it means for <span class="math-container">$y$</span> to be a correct output. (In the above example <span class="math-container">$A$</span> and <span class="math-container">$B$</span> are the types of lists and <span class="math-container">$\phi(\ell, k)$</span> is &quot;<span class="math-container">$k$</span> is ordered and <span class="math-container">$k$</span> is a permutation of <span class="math-container">$\ell$</span>.&quot;) If <span class="math-container">$\phi$</span> is in <span class="math-container">$\mathtt{Prop}$</span> then extraction gives a map <span class="math-container">$f : A \to B$</span> such that <span class="math-container">$\phi(x, f(x))$</span> holds for all <span class="math-container">$x \in A$</span>. If <span class="math-container">$\phi$</span> is in <span class="math-container">$\mathtt{Set}$</span> then we also get a function <span class="math-container">$g$</span> such that <span class="math-container">$g(x)$</span> is the proof that <span class="math-container">$\phi(x, f(x))$</span> holds, for all <span class="math-container">$x \in A$</span>. Often the proof is computationally useless and we prefer to get rid of it, especially when it is nested deeply inside some other statement. <span class="math-container">$\mathtt{Prop}$</span> gives us the possibility to do so.</p>
<p><strong>Added 2015-07-29:</strong> There is a question whether we could avoid <span class="math-container">$\mathsf{Prop}$</span> altogether by automatically optimizing away &quot;useless extracted code&quot;. To some extent we can do that, for instance all code extracted from the negative fragment of logic (stuff built from the empty type, unit type, products) is useless as it just shuffles around the unit. But there are genuine design decisions one has to make when using <span class="math-container">$\mathsf{Prop}$</span>. Here is a simpe example, where <span class="math-container">$\Sigma$</span> means that we are in <span class="math-container">$\mathsf{Type}$</span> and <span class="math-container">$\exists$</span> means we are in <span class="math-container">$\mathsf{Prop}$</span>. If we extract from
<span class="math-container">$$\Pi_{n : \mathbb{N}} \Sigma_{b : \{0,1\}} \Sigma_{k : \mathbb{N}} \; n = 2 \cdot k + b$$</span>
we will get a program which decomposes <span class="math-container">$n$</span> into its lowest bit <span class="math-container">$b$</span> and the remaining bits <span class="math-container">$k$</span>, i.e., it computes everything. If we extract from
<span class="math-container">$$\Pi_{n : \mathbb{N}} \Sigma_{b : \{0,1\}} \exists_{k : \mathbb{N}} \; n = 2 \cdot k + b$$</span>
then the program will only compute the lowest bit <span class="math-container">$b$</span>. The machine cannot tell which is the correct one, the user has to tell it what they want.</p>

CC BY-SA 3.0
2015-07-24T07:13:53.417Z
I'm slightly confused. Are you saying that without $\mathtt{Prop}$ it'd be impossible to recognize in the extracted program that $g(x)$ doesn't contribute to the output (i.e. that it merely verifies it)? Are there scenarios where one wouldn't be able to pull out such useless code through the usual means available to code optimizers?
user
CC BY-SA 3.0
2015-07-26T19:11:14.833Z
The extracted code produces higher-order functions. A code optimizer cannot tell whether these will be used in a useful way. So yes, unless there is some mechanism to indicate which parts of code are "useless", you can't tell.
Andrej Bauer
CC BY-SA 3.0
2015-07-27T10:49:49.307Z
I'm sorry, but I'm having trouble coming up with an example that can't be optimized away over multiple passes starting from the desired output and working backwards (albeit with global optimization). Do you have any particular examples?
user
CC BY-SA 3.0
2015-07-28T08:29:46.550Z
Yes, the sorting example presented in my answer. How can you tell that `verify` is useless?
Andrej Bauer
CC BY-SA 3.0
2015-07-29T04:47:55.297Z
From the extracted program one could say, "I want $k$," and backtrack from there. I haven't been able to come up with a scenario so entangled that we couldn't optimize away anything that doesn't directly contribute to determining the permutation without it in fact being necessary for computing said permutation (from a global optimization standpoint, anyway).
user
CC BY-SA 3.0
2015-07-29T09:46:37.410Z
You do not have the information "I want $k$". That is an extra assumption, and obviously once they tell you which particular result they want, you can just optimize away dead code. Actually, I thought of a better answer: it is a *design* question which things to put in $\mathsf{Prop}$. You need to know what the user wants, and he tells you what he wants by using $\mathsf{Prop}$. It is easy to come up with examples where there are several options. I will add one to my answer.
Andrej Bauer
CC BY-SA 3.0
2015-07-29T13:53:29.390Z
perhaps this is slightly off topic, but in HoTT Prop is replaced by -1-types, so it's not a simple markup anymore. Is it possible (or efficiently implementable) to do the same thing if we were to extract code into say ocaml?
SorcererofDM
CC BY-SA 3.0
2015-07-29T14:24:51.413Z
As far as I know nobody can really tell how to extract anything from $(-1)$-types. It's clear that they contain *some* computational content, but not what this might be.
Andrej Bauer
CC BY-SA 3.0
2015-07-29T18:12:45.833Z
Ah, okay. Using $\mathtt{Prop}$ as a way of specifying design decisions makes a lot more sense to me than as a way of deleting useless code.
user
CC BY-SA 4.0
2018-06-10T14:58:50.733Z
There are 3 dimensions: proof relevance vs irrelevance (which as I understand effects in non-extracted code), different type constructions $\Sigma$ vs $\exists$, strength of the theory: predicative vs impredicativive quantification. These dimensions are tied in a one particular way in Coq. Is it a pragmatic choice or a fundamental one?
Łukasz Lew
CC BY-SA 4.0
2021-11-27T06:47:14.840Z
@ŁukaszLew That's probably a separate large question, but impredicative sigmas enable variants of Girard's paradox. Very intuitively (this is no proof), you can't squeeze types inside values (in simple models, that is even because types are predicates on values so they're more). Large existentials get around that by erasing the witness type altogether, they just make up an arbitrary suitable one on elimination. This story just hints at a possible model, the actual paradox is much more technical.
Blaisorblade
CC BY-SA 4.0
2014-03-31T05:07:13.747Z
2022-12-09T12:51:21.457Z
2022-12-09T12:51:21.457Z
Andrej Bauer
<p>Coq has a type Prop of proof irrelevant propositions which are discarded during extraction. What are the reason for having this if we use Coq only for proofs. Prop is impredicative, <s>so Prop : Prop,</s> however, Coq automatically infers universe indexes and we can use Type(i) instead everywhere. It seems Prop complicates everything a lot.</p>

<p>I read that there're philosophical reasons for separating Set and Prop in Luo's book, however, I didn't find them in the book. What are they?</p>

CC BY-SA 3.0
2014-03-31T14:48:52.240Z
“if we use Coq only for proofs”: I think you've identified a key point here. Coq isn't used only for proofs.
Gilles 'SO- stop being evil'
<coq><dependent-type>
Why does Coq have Prop?
Konstantin Solomatov
# Why does Coq have Prop?

(Asked by: username_0 on 2014-03-31)

Coq has a type Prop of proof irrelevant propositions which are discarded during extraction. What are the reason for having this if we use Coq only for proofs. Prop is impredicative, ~~so Prop : Prop,~~ however, Coq automatically infers universe indexes and we can use Type(i) instead everywhere. It seems Prop complicates everything a lot.

I read that there're philosophical reasons for separating Set and Prop in Luo's book, however, I didn't find them in the book. What are they?

**Tags:** coq, dependent-type
> **Comments:**
> **username_1**: “if we use Coq only for proofs”: I think you've identified a key point here. Coq isn't used only for proofs.  

---

## 4 answers

### Answer by username_6 on 2014-03-31. Score: 43 | Accepted answer

$\mathtt{Prop}$ is very useful for program extraction because it allows us to delete parts of code that are useless. For example, to extract a sorting algorithm we would prove the statement "for every list $\ell$ there is a list $k$ such that $k$ is ordered and $k$ is a permutatiom of $\ell$". If we write this down in Coq and extract without using $\mathtt{Prop}$, we will get:

1. "for all $\ell$ there is $k$" will give us a map `sort` which takes lists to lists,
2. "such that $k$ is ordered" will give a funciton `verify` which runs through $k$ and checks that it is sorted, and
3. "$k$ is a permutation of $\ell$" will give a permutation `pi` which takes $\ell$ to $k$. Note that `pi` is not just a mapping, but also the inverse mapping together with programs verifying that the two maps really are inverses.

While the extra stuff is not totally useless, in many applications we want to get rid of it and keep just `sort`. This can be accomplished if we use $\mathtt{Prop}$ to state "$k$ is ordered" and "$k$ is a permutation of $\ell$", but *not* "for all $\ell$ there is $k$".

In general, a common way to extract code is to consider a statement of the form $\forall x : A \,.\, \exists y : B \,.\, \phi(x, y)$ where $x$ is input, $y$ is output, and $\phi(x,y)$ explains what it means for $y$ to be a correct output. (In the above example $A$ and $B$ are the types of lists and $\phi(\ell, k)$ is "$k$ is ordered and $k$ is a permutation of $\ell$.") If $\phi$ is in $\mathtt{Prop}$ then extraction gives a map $f : A \to B$ such that $\phi(x, f(x))$ holds for all $x \in A$. If $\phi$ is in $\mathtt{Set}$ then we also get a function $g$ such that $g(x)$ is the proof that $\phi(x, f(x))$ holds, for all $x \in A$. Often the proof is computationally useless and we prefer to get rid of it, especially when it is nested deeply inside some other statement. $\mathtt{Prop}$ gives us the possibility to do so.

**Added 2015-07-29:** There is a question whether we could avoid $\mathsf{Prop}$ altogether by automatically optimizing away "useless extracted code". To some extent we can do that, for instance all code extracted from the negative fragment of logic (stuff built from the empty type, unit type, products) is useless as it just shuffles around the unit. But there are genuine design decisions one has to make when using $\mathsf{Prop}$. Here is a simpe example, where $\Sigma$ means that we are in $\mathsf{Type}$ and $\exists$ means we are in $\mathsf{Prop}$. If we extract from
$$\Pi\_{n : \mathbb{N}} \Sigma\_{b : \{0,1\}} \Sigma\_{k : \mathbb{N}} \; n = 2 \cdot k + b$$
we will get a program which decomposes $n$ into its lowest bit $b$ and the remaining bits $k$, i.e., it computes everything. If we extract from
$$\Pi\_{n : \mathbb{N}} \Sigma\_{b : \{0,1\}} \exists\_{k : \mathbb{N}} \; n = 2 \cdot k + b$$
then the program will only compute the lowest bit $b$. The machine cannot tell which is the correct one, the user has to tell it what they want.

> **Comments:**
> **username_7**: I'm slightly confused. Are you saying that without $\mathtt{Prop}$ it'd be impossible to recognize in the extracted program that $g(x)$ doesn't contribute to the output (i.e. that it merely verifies it)? Are there scenarios where one wouldn't be able to pull out such useless code through the usual means available to code optimizers?  
> **username_6**: The extracted code produces higher-order functions. A code optimizer cannot tell whether these will be used in a useful way. So yes, unless there is some mechanism to indicate which parts of code are "useless", you can't tell.  
> **username_7**: I'm sorry, but I'm having trouble coming up with an example that can't be optimized away over multiple passes starting from the desired output and working backwards (albeit with global optimization). Do you have any particular examples?  
> **username_6**: Yes, the sorting example presented in my answer. How can you tell that `verify` is useless?  
> **username_7**: From the extracted program one could say, "I want $k$," and backtrack from there. I haven't been able to come up with a scenario so entangled that we couldn't optimize away anything that doesn't directly contribute to determining the permutation without it in fact being necessary for computing said permutation (from a global optimization standpoint, anyway).  
> **username_6**: You do not have the information "I want $k$". That is an extra assumption, and obviously once they tell you which particular result they want, you can just optimize away dead code. Actually, I thought of a better answer: it is a *design* question which things to put in $\mathsf{Prop}$. You need to know what the user wants, and he tells you what he wants by using $\mathsf{Prop}$. It is easy to come up with examples where there are several options. I will add one to my answer.  
> **username_8**: perhaps this is slightly off topic, but in HoTT Prop is replaced by -1-types, so it's not a simple markup anymore. Is it possible (or efficiently implementable) to do the same thing if we were to extract code into say ocaml?  
> **username_6**: As far as I know nobody can really tell how to extract anything from $(-1)$-types. It's clear that they contain *some* computational content, but not what this might be.  
> **username_7**: Ah, okay. Using $\mathtt{Prop}$ as a way of specifying design decisions makes a lot more sense to me than as a way of deleting useless code.  
> **username_9**: There are 3 dimensions: proof relevance vs irrelevance (which as I understand effects in non-extracted code), different type constructions $\Sigma$ vs $\exists$, strength of the theory: predicative vs impredicativive quantification. These dimensions are tied in a one particular way in Coq. Is it a pragmatic choice or a fundamental one?  
> **username_10**: @ŁukaszLew That's probably a separate large question, but impredicative sigmas enable variants of Girard's paradox. Very intuitively (this is no proof), you can't squeeze types inside values (in simple models, that is even because types are predicates on values so they're more). Large existentials get around that by erasing the witness type altogether, they just make up an arbitrary suitable one on elimination. This story just hints at a possible model, the actual paradox is much more technical.  

---

### Answer by username_2 on 2014-04-01. Score: 27

$\mathrm{Prop}$ is *impredicative*, which create a very expressive proof system. However it is "too" expressive in the following sense:

$$ \mathrm{impredicative\ Prop} + \mathrm{large\ elimination} + \mathrm{excluded\ middle} $$

is inconsistent. Usually you want to keep the possibility to add the excluded middle, so one solution is to keep large elimination and make Prop predicative. The other is to suppress large elimination.

Coq did both! They renamed the predicative Prop to Set, and disabled large elimination in Prop.

The expressiveness gained by impredicativity is "reassuring" in the sense 99% of "reasonable" mathematics can be formalized with it, and it is known to be consistent relative to set theory. This makes it likely they won't weaken it to something like Agda, which only has predicative universes.

> **Comments:**
> **username_2**: Oh and I forgot to mention: it is **not** the case that ``Prop : Prop``, that would be inconsistent. Rather *quantifications* over all propositions is again a proposition.  
> **username_3**: Could you point me to any more resources about this?  Everything I can find seems very scattered.  
> **username_2**: @user833970 any specific things you'd like pointers to? I'm afraid there isn't really an all encompassing reference for meta theory of dependent types. This discussion (which points back here!) might be useful: https://github.com/FStarLang/FStar/issues/360  
> **username_3**: thank, I'm working through the Berardi paradox paper now, I think that will clear up my confusion.  

---

### Answer by username_4 on 2014-03-31. Score: 14

Even if you are not interested in extracting programs, the fact that `Prop` is impredicative allows you to build some models which you can't build using a predicative tower of universes. IIRC Thorsten Altenkirch has a model of System F using Coq's impredicativity.


---

### Answer by username_5 on 2021-04-08. Score: 2

The principle of propositions-as-types (or formulas-as-types), also known as the Curry-Howard correspondence, is the key idea for viewing (intuitionistic) type theories as logical systems and to apply type theories (and constructive mathematics in general) to computer science.
Suppose U is the type of all propositions, then U is also the type of all types by the identification. Therefore, type U of all types naturally occurs and, in particular, it is the type of itself.
In Martin-Löf's (predicative) type theory, propositions and types
are still identified, but the type of all types is replaced by an infinite sequence of type universes U0 U 1: U2..... Hence, one can not quantify over all propositions or predicates, although quantification over each universe is allowed.

That's the reason type and prop are separated. Without this separation the resulting system becomes inconsistent.


---

