Finitary type theories with and without contexts

TL;DR

This paper defines a broad class of finitary type theories, proves key meta-theorems, and introduces a context-free formulation with explicit variable annotations, demonstrating their equivalence and implementing it in a proof assistant.

Contribution

It introduces a unified framework for finitary type theories with and without contexts, along with translations and implementation in a proof assistant.

Findings

Finitary type theories encompass many dependent type theories.

Meta-theorems like weakening and substitution are established.

Context-free formulation is shown to be equivalent to traditional context-based theories.

Abstract

We give a definition of finitary type theories that subsumes many examples of dependent type theories, such as variants of Martin-L\"of type theory, simple type theories, first-order and higher-order logics, and homotopy type theory. We prove several general meta-theorems about finitary type theories: weakening, admissibility of substitution and instantiation of metavariables, derivability of presuppositions, uniqueness of typing, and inversion principles. We then give a second formulation of finitary type theories in which there are no explicit contexts. Instead, free variables are explicitly annotated with their types. We provide translations between finitary type theories with and without contexts, thereby showing that they have the same expressive power. The context-free type theory is implemented in the nucleus of the Andromeda 2 proof assistant.