On the strength of proof-irrelevant type theories

TL;DR

This paper introduces a proof-irrelevant type theory useful for theorem proving, explores its relation to subset types, and demonstrates how it leads to classical logic features like decidability of equality.

Contribution

It presents a novel proof-irrelevant type theory with a set-theoretic semantics and analyzes its logical properties and relation to existing systems.

Findings

Proof-irrelevance integrated into conversion rule enhances theorem proving.

In these theories, the axiom of choice implies decidability of equality.

The set-theoretic semantics provides a foundational understanding of the theory.

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.