An Intuitionistic Set-theoretical Model of the Extended Calculus of Constructions

TL;DR

This paper presents a topological set-theoretical model of the Extended Calculus of Constructions (ECC) that enhances intuitionistic properties of the Prop sort while maintaining simplicity, with proven soundness and practical applications.

Contribution

It introduces a novel interpretation of Prop into a Heyting algebra, improving the intuitionistic nature of Werner's ECC model without losing simplicity.

Findings

The model is sound.

It better captures intuitionistic logic.

Applications demonstrate its usefulness.

Abstract

Werner's set-theoretical model is one of the most intuitive models of ECC. It combines a functional view of predicative universes with a collapsed view of the impredicative sort Prop. However this model of Prop is so coarse that the principle of excluded middle holds. In this paper, we interpret Prop into a topological space (a special case of Heyting algebra) to make it more intuitionistic without sacrificing simplicity. We prove soundness and show some applications of our model.