2016/10/07 by Michael Rathjen, Rathjen, Michael
Mathematics · #03C62 #03F30 #03F50 #FOS: Mathematics #Logic (math.LO) #math.LO #msc:03C62 #msc:03F30 #msc:03F50
paper · pdf · doi:10.48550/arxiv.1610.02191
28 pages
arxiv created 2018/01/05 · arxiv updated 2018/01/08
In Feferman's work, explicit mathematics and theories of generalized inductive definitions play a central role. One objective of this article is to describe the connections with Martin-Lof type theory and constructive Zermelo-Fraenkel set theory. Proof theory has contributed to a deeper grasp of the relationship between different frameworks for constructive mathematics. Some of the reductions are known only through ordinal-theoretic characterizations. The paper also addresses the strength of Voevodsky's univalence axiom. A further goal is to investigate the strength of intuitionistic theories of generalized inductive definitions in the framework of intuitionistic explicit mathematics that lie beyond the reach of Martin-Lof type theory.