On the Strength of Proof-Irrelevant Type Theories

Benjamin Werner explore a type theory that, among other things, might be a first step towards making a proof assistant that's also a more traditional programming environment in On the Strength of Proof-Irrelevant Type Theories, Logical Methods In Computing 2008.

Abstract. We present a type theory with some proof-irrelevance built into the conversion rule. We argue that this feature is useful when type theory is used as the logical formalism underlying a theorem prover. We also show a close relation with the subset types of the theory of PVS. We show that in these theories, because of the additional extentionality, the axiom of choice implies the decidability of equality, that is, almost classical logic. Finally we describe a simple set-theoretic semantics.

A suggested application lies a few paragraphs in.

In order to identify more terms it thus is tempting to [integrate] program extraction into the formalism so that the conversion rule does not require the computationally irrelevant parts of terms to be convertible.

In what follows, we present and argue in favor of a type-theory along this line. More precisely, we claim that such a feature is useful in at least two respects. For one, it gives a more comfortable type theory, especially in the way it handles equality. Furthermore it is a good starting point to build a platform for programming with dependent types, that is to use the theorem prover also as a programming environment. ...

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Is my reasoning correct?

This is a very nice idea and proof irrelevance (implemented one way or another) seems essential to me for the adoption of type theory as a programming language, but I worry about this particular method not being applicable in practice.
If a constructed proof is indistinguishable from a hypothesised proof (for example, of a false statement) then surely the type theory has become inconsistent and undecidable. So I can believe it would work for CoC + eq, but for CIC it seems impossible, is it?

Prop vs Type

A basic question: Why do proof systems separate Prop and Type? In other words, which types aren't propositions?

A few reasons

Prop and Type are separated in Coq using the sorting system, while Epigram for example separate it by embedding a new, closed prop datatype into Type so all prop's begins with a particular constructor. With Coq's way it is easy to separate logical and computational terms, which forms the basis of extraction: you just need to erase things whose sort is Prop. It is also possible this way to have particular typing rules for handling props and selectively make the Prop universe impredicative for example [(∀ P : Prop, P \/ ~ P) : Prop].
The formation rules for Prop and Type are roughly the same otherwise so you can have a copy of nat, tree or whatever in one or the other. However, things in Prop intuitively obey the proof-irrelevance principle which says that in your copy of bool in Prop you will have true_prop = false_prop.

Impredicative Sigma quantification

In fact, not all type systems/logical frameworks do separate them: the original version of Martin-Loef's intensional type theory did not, although many systems based on it do add the distinction, typically, as Mathieu said, to get the right notion of proof equivalence.

There's a strong technical reason to separate them in impredicative type theory, which is that several desirable type formers, most importantly impredicative Sigma quantification, cannot be added to the theory without inconsistency. This is, of course, catastrophic in Prop, but may be tolerated in Type, so such type formers can be used in Type, but forbidden in Prop, recovering consistency in the parts that matter.

I have the idea that this is in Coquand's "Metamathematical Investigations of a Calculus of Constructions", but I have lost my copy. It's discussed in Zhaohui Luo's "Computation & Reasoning".