Proof-irrelevant model of CC with predicative induction and judgmental equality

TL;DR

This paper introduces a set-theoretic, proof-irrelevant model for the Calculus of Constructions with predicative induction and judgmental equality, using Aczel's trace encoding and extending Dybjer's interpretations.

Contribution

It provides a novel set-theoretic model for CC with predicative induction, incorporating Aczel's trace encoding and concrete interpretations for recursive functions.

Findings

Model demonstrates consistency of type theory.

Supports simultaneous induction and recursive functions.

Framework can serve as a basis for a theorem prover.

Abstract

We present a set-theoretic, proof-irrelevant model for Calculus of Constructions (CC) with predicative induction and judgmental equality in Zermelo-Fraenkel set theory with an axiom for countably many inaccessible cardinals. We use Aczel's trace encoding which is universally defined for any function type, regardless of being impredicative. Direct and concrete interpretations of simultaneous induction and mutually recursive functions are also provided by extending Dybjer's interpretations on the basis of Aczel's rule sets. Our model can be regarded as a higher-order generalization of the truth-table methods. We provide a relatively simple consistency proof of type theory, which can be used as the basis for a theorem prover.