Models and termination of proof reduction in the $\lambda$$\Pi$-calculus modulo theory

TL;DR

This paper introduces a model for the λΠ-calculus modulo theory, proving proof reduction termination for super-consistent theories, including simple type theory and the calculus of constructions.

Contribution

It defines a new notion of model and super-consistency, establishing proof reduction termination in the λΠ-calculus modulo theory.

Findings

Proof reduction terminates in super-consistent theories

Models for λΠ-calculus modulo theory are established

Termination proven for simple type theory and calculus of constructions

Abstract

We define a notion of model for the $\lambda$$\Pi$-calculus modulo theory and prove a soundness theorem. We then define a notion of super-consistency and prove that proof reduction terminates in the $\lambda$$\Pi$-calculus modulo any super-consistent theory. We prove this way the termination of proof reduction in several theories including Simple type theory and the Calculus of constructions .