已收录 273176 条政策
 政策提纲
  • 暂无提纲
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 constructive theories. Then we show, how, as part of such a programe, the proof theoretic analysis of Martin-Löf type theory with W-type and one microscopic universe containing only two finite sets is carried out. Then we look at the analysis Martin-Löf type theory with W-type and a universe closed under the W-type, and consider the extension of type theory by one Mahlo universe and its proof-theoretic analysis. Finally, we repeat the concept of inductive-recursive definitions, which extends the notion of inductive definitions substantially. We introduce a closed formalization, which can be used in generic programming, and explain, what is known about its strength.
[发布日期]  [发布机构] 
[效力级别]  [学科分类] 数学(综合)
[关键词] set theory;well-founded trees;Kleene's O;Mahlo universe;inductive-recursive definitions;generic programming;Martin-Löf type theory;Kripke Platek set theory [时效性] 
   浏览次数:11      统一登录查看全文      激活码登录查看全文