Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Are Dependent Types in Set Theory Feasible?

Yunsong Yang, Simon Guilloud, Viktor Kunčak

Abstract

Following the types-as-sets paradigm, we present a mechanized embedding of dependent function types with a hierarchy of universes into schematic first-order logic with equality, with axiom schemas of Tarski-Grothendieck set theory. We carry this embedding in the Lisa proof assistant. On top of this foundation, we implement a proof-producing bidirectional type-checking tactic to compute proofs for typing judgements, with partial support for subtyping. We present examples showing how our approach enables automated reasoning for dependent types that is fully verified from set-theoretic axioms and deduction rules for schematic first-order logic with equality. Because types are merely sets, the resulting formalism supports equality that applies to all types and values and permits the usual substitution rules.

Are Dependent Types in Set Theory Feasible?

Abstract

Following the types-as-sets paradigm, we present a mechanized embedding of dependent function types with a hierarchy of universes into schematic first-order logic with equality, with axiom schemas of Tarski-Grothendieck set theory. We carry this embedding in the Lisa proof assistant. On top of this foundation, we implement a proof-producing bidirectional type-checking tactic to compute proofs for typing judgements, with partial support for subtyping. We present examples showing how our approach enables automated reasoning for dependent types that is fully verified from set-theoretic axioms and deduction rules for schematic first-order logic with equality. Because types are merely sets, the resulting formalism supports equality that applies to all types and values and permits the usual substitution rules.
Paper Structure (4 sections, 7 theorems, 5 equations)

This paper contains 4 sections, 7 theorems, 5 equations.

Table of Contents

  1. Introduction
  2. Embedding of Dependent Product
  3. Universe Management
  4. Proof Generation

Key Result

Theorem 2

If $t \in T$ then $\mathop{\mathrm{app}}\nolimits(\mathop{\mathrm{abs}}\nolimits(T)(L))(t) = L(t)$.

Theorems & Definitions (11)

  • Definition 1
  • Theorem 2: $\beta$-reduction
  • Theorem 3: $T_{abs}$
  • Theorem 4: $T_{app}$
  • Definition 5: Grothendieck Universe
  • Definition 6: Tarski's axiom
  • Definition 7: isUniverse predicate
  • Lemma 8: From Grothendieck universes to isUniverse
  • Lemma 9: Universe closure under dependent products
  • Theorem 10: $T_{\mathrm{sort}}$
  • ...and 1 more