Proof Theory of Martin-Löf Type Theory. An overview

Proof Theory of Martin-Löf Type Theory. An overview

We give an overview over the historic development of proof theory and the main techniques used in ordinal theoretic proof theory. We argue, that in a revised Hilbert’s program, ordinal theoretic proof theory has to be supplemented by a second step, namely the development of strong equiconsistent con...

Ful tanımlama

Kaydedildi:
Detaylı Bibliyografya
Yayımlandı:URI:https://journals.openedition.org/msh,
Yazar: Setzer, Anton
Materyal Türü: Article ou chapitre numérique
Dil:Anglais
Baskı/Yayın Bilgisi: Mathématiques et sciences humaines 2006
Konular:
théorie des ensembles
arbres bien fondés
ordinaux de Kleene
univers de Mahlo
définition inductive-récursive
programmation générique
théorie des types de Martin-Löf
théorie des ensembles de Kripke Platek
set theory
well-founded trees
Kleene's O
Mahlo universe
inductive-recursive definitions
generic programming
Martin-Löf type theory
Kripke Platek set theory
Online Erişim:Accès Université d'Orléans et IFPM
Accès Université d'Orléans et IFPM

Internet

https://ezproxy.univ-orleans.fr/login?url=https://doi.org/10.4000/msh.2959
https://ezproxy.univ-orleans.fr/login?url=https://journals.openedition.org/msh/2959

Benzer Materyaller