Skip to content

Abstracts.2020.Impredicativity

Jump to bottom
Warrick Macmillan edited this page Oct 12, 2021 · 3 revisions

Some Remarks about Impredicativity

by Thierry Coquand

Abstract

I will try to present the calculus that I designed in 1984–85, inspired by the works of de Bruijn, Girard and Martin-Löf, and what were the main problems at the time. I will compare it to the system of Frege, and explain how it provides a uniform notation for terms and proofs in higher-order logic (∀t : (t ⟶ ο) ⟶ ο with t ::= ι extended by not just t ::= ... | ο | ι → t but by t ::= ... | ο | t1 → t2) and proofs of parametricity. I will also explain how it was possible to represent inductive definitions. Next, I will connect it with the work about paradoxes in type theory and how this suggested the extension with universes. If time allows, I will explain what were the problems with an encoding of inductive data types, and why this was extended with primitive inductive definitions.

Resources

Bibliography

  1. Thierry Coquand: Some remarks on dependent type theory
  2. Wikipedia: Frege's Begriffsschrift
  3. Steven Fortune, Daniel Leivant, Michael O'Donnell: The Expressiveness of Simple and Second-Order Type Structures (1983)
  4. N.G. de Bruijn: AUTOMATH, A Language for Mathematics (1973)
  5. Thierry Coquand: Type Theory in The Stanford Encyclopedia of Philosophy (2006, 2018)
  6. Thierry Coquand: An Analysis of Girard's Paradox (1986)
  7. Thierry Coquand: Metamathematical Analysis of a Calculus of Constructions
  8. Alexandre Miquel: Le Calcul des Constructions implicite — Syntaxe et Sémantique (2001)
  9. Frank Pfenning, Christine Paulin-Mohring: Inductively Defined Types in the Calculus of Constructions (1989)
  10. Jean-Philippe Bernardy, Patrik Jansson, Ross Paterson: Parametricity and Dependent Types (2010)
Clone this wiki locally