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–Löf 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–Löf type theory.
CITATION STYLE
Rathjen, M. (2017). Proof Theory of Constructive Systems: Inductive Types and Univalence. In Outstanding Contributions to Logic (Vol. 13, pp. 385–419). Springer. https://doi.org/10.1007/978-3-319-63334-3_14
Mendeley helps you to discover research relevant for your work.