**Problem Detail:**

I'm looking at the Calculus of Constructions and its place in the Lambda Cube.

If I understand correctly, each axis of the cube can be thought of as adding another operation involving types to the simply-typed calculus, $\lambda_\to$. The first axis adds type-to-term operators, the second type-to-type operators, and the third dependent typing, or term-to-type operators. The CoC has all three.

However, the CoC introduces a term $Prop$, and states that $Prop : Type$ by the inference rules, but is otherwise not used. I understand that it is for the eponymous propositions, but the logical propositions are not defined in terms of it.

Could you explain to me what $Prop$ is for, where/when it appears, and explain it in terms of the cube's axes (if indeed it is possible to do so)?

###### Asked By : Michael Rawson

#### Answered By : Andrej Bauer

In traditional Martin-Löf type theory there is no distinction between types and propositions. This goes under the slogan "propositions as types". But there are sometimes reasons for distinguishing them. CoC does precisely that.

There are many variants of CoC, but most would have $$\mathsf{Prop} : \mathsf{Type}$$ but *not* $\mathsf{Type} : \mathsf{Prop}$. Another difference shows up when we have infinitely many type universes and make $\mathsf{Prop}$ impredicative (this is what Coq does). Concretely, consider a variant of CoC where we have $\mathsf{Prop}$ and infinitely many type universes $\mathsf{Type}_1$, $\mathsf{Type}_2$, $\mathsf{Type}_3$ with \begin{align*} \mathsf{Prop} &: \mathsf{Type}_1 \\ \mathsf{Type}_1 &: \mathsf{Type}_2 \\ \mathsf{Type}_2 &: \mathsf{Type}_3 \\ &\vdots \end{align*} The formation rule for $\prod$ has to explain how to form $\prod_{x : A} B(x)$ when $A$ is either a proposition or a type, and $B(x)$ is either a proposition or a type. There are four combinations:

- $$\frac{A : \mathsf{Prop} \qquad x : A \vdash B(x) : \mathsf{Prop}} {\prod_{x : A} B(x) : \mathsf{Prop}}$$
- $$\frac{A : \mathsf{Type}_i \qquad x : A \vdash B(x) : \mathsf{Prop}} {\prod_{x : A} B(x) : \mathsf{Prop}}$$
- $$\frac{A : \mathsf{Prop} \qquad x : A \vdash B(x) : \mathsf{Type}_i} {\prod_{x : A} B(x) : \mathsf{Type}_i}$$
- $$\frac{A : \mathsf{Type}_i \qquad x : A \vdash B(x) : \mathsf{Type}_j} {\prod_{x : A} B(x) : \mathsf{Type}_{\max(i,j)}}$$

The most interesting is the difference between the second and the fourth case. The fourth rules says that if $A$ is in the $i$-th universe and $B(x)$ is in the $j$-th universe, then the product is in the $\max(i,j)$-th universe. But the second rule is telling us that $\mathsf{Prop}$ is *not* just "one more universe at the bottom", because $\prod_{x : A} B(x)$ lands in $\mathsf{Prop}$ as soon as $B(x)$ does, no matter how big $A$ is. This is *impredicative* because it allows us to define elements of $\mathsf{Prop}$ by quantifying over $\mathsf{Prop}$ itself.

A concrete example would be $$\prod_{A : \mathsf{Type}_1} A \to A$$ versus $$\prod_{A : \mathsf{Prop}} A \to A$$ The first product lives in $\mathsf{Type}_2$, but the second one is in $\mathsf{Prop}$ (and not in $\mathsf{Type}_1$, even though we are quantifying over an element of $\mathsf{Type}_1$). In particular, this means that one of the possible values for $A$ is $\prod_{A : \mathsf{Prop}} A \to A$ itself.

###### Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/28695

**3.2K people like this**

## 0 comments:

## Post a Comment

Let us know your responses and feedback