Lack of atomic propositions in the Calculus of Constructions from ATTAPL textbook

Question

I am working through the Dependent Types chapter from Advanced Topics in Types and Programming Languages (ATTAPL) by Benjamin Pierce et al. I am confused with the calculus presented Fig 2-7 (Calculus of Constructions) that extends $\lambda LF$ to support Prop type. I have multiple questions.

1. Can a Prop term be $\beta$-reduced at all? The rule (BETA-ALL) on the next page suggests that only the body of a Prop can be reduced. That is, in the term forall x:T.t, only t is reduced.

2. There are no atomic propositions like True, False. So how can one build a term of type Prop (and Prf p). Any simple example suffices.

3. I am not sure I understand the type equivalence rule QT-ALL in Fig 2-7.

4. The encoding of nat (and zero later on) is confusing. For the sake of readability I am writing it down here.

   nat = all a:Prop.all z:Prf a.all s:Prf a ->Prf a. a

   What is the meaning? Specifically, what is a - any Prop? Why are proofs of z (zero) and s (succ) required?

I think these are lot of questions. I would appreciate answers to any of these questions.

EDIT: I was suggested to move this to cs.stackexchange.com. However, the question is about the meta-theory of Coq and I thought cstheory is an appropriate forum. But if multiple users suggest moving this, I can do that.

Answer 1

I have no thoughts on whether this is on-topic for TCS and if need be I can repost my answer elsewhere. But I think the question is a good opportunity to demonstrate how to think about the CoC pending some consensus to move it.

1. The rule BETA-ALL, which says we can beta-reduce terms underneath the all binder (but not the type of the argument), is not part of the typing or equivalence rules of $\mathsf{CC}$. Pierce is extending his definition of $\beta$-reduction first seen in Section 2.3 (section "Strong Normalization"), which itself is defined "As an auxiliary device for the soundness and completeness of algorithmic typechecking." Specifically the fact that this reduction is strongly normalizing can be used to show that typechecking halts.

2. Pierce mentions on page 51 that "We may use type and term variables declared in a fixed initial context to simulate the built-in types and operators of a programming language."

   Also see Figure 2-1 (First-order dependent types), in which one of the context formation rules (labelled "term variable binding") is that if $\Gamma$ is a well-formed context and $T$ is a well-formed type, we can pick a variable name $x$ and and then $\Gamma, x :: T$ is a well-formed context. (It seems to be implicit that $x$ should be a fresh name, i.e. does not conflict with the rest of $\Gamma$, and that $T$ is well-formed in context $\Gamma$.).

   Now combine this with rule of Figure 2-7 which states that $T ::= \ldots \mathsf{Prop}\ldots$, meaning $\mathsf{Prop}$ is a type. Therefore we can add $\mathsf{True} :: \mathsf{Prop}$ to the context. Likewise with $\mathsf{False}$.

   To add a proof of $\mathsf{True}$, use rule K-App to deduce that $\mathsf{Prf} \:\mathsf{True}$ has kind $\ast$, i.e. is a type, and apply term variable binding again to add some proof $\mathsf{Unit} :: \mathsf{Prf} \,\mathsf{True}$ to the context.

3. When introducing $\mathsf{Prop}$, we also introduce this new binder called forall, which seems reasonable. Now we have to give this a semantics---how do we prove some forall x, P? The rule merely states that a proof of forall x, P is the same thing as offering "a proof of $P$ for every $x$" where the latter is defined as a dependent product (something our system already had). In a sense, the rules just say "by using the operator $\mathsf{Prf}$, $\mathsf{Prop}$ acts like $\ast$."

   Perhaps you're wondering why this is interesting. We know that a proposition $p:\mathsf{Prop}$ can be coerced to a type $\mathsf{Prf} p : \ast$, and the equivalence says the binder forall acts like a dependent product, so what is gained?. But notice that by using T-ALL and QT-ALL, $\mathsf{Prop}$ can effectively play the role of $T$ when forming the dependent product, so we can quantify over $\mathsf{Prop}$ and still have a $\mathsf{Prop}$. This is the "impredicativity" Pierce refers to, and it makes the system drastically more expressive. If we tried to get rid of the coercion just take $\mathsf{Prop} \equiv \ast$, we would have $\ast : \ast$, which is known to be inconsistent by a theorem of Girard.

4. To exhibit a natural number per Pierce's definition, you must be able to satisfy this criterion: If I give you any type $a$, term $z : a$, and successor function $s : a \to a$, you must be able to offer me some term of type $a$. Since you don't know the type $a$ in advance, the only thing you can do is apply $s$ to $z$ some number of times, and that is effectively the same thing as having a natural number. Pierce is showing that $\mathsf{CC}$ is expressive enough to type Church's encoding of the natural numbers , which is good because that encoding becomes impossible when you move from untyped lambda calculus to STLC. See these course notes. See also the Wikipedia page on System F for more information---System F is less expressive than $\mathsf{CC}$ but still good enough to play this game.