Portal de Periódicos da CAPES

Proof Theory of Constructive Systems: Inductive Types and Univalence

2017; Springer International Publishing; Linguagem: Inglês

10.1007/978-3-319-63334-3_14

2211-2766

Michael Rathjen,

Logic, Reasoning, and Knowledge

In Feferman’sFeferman, Solomon work, explicit mathematicsExplicit 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 typeMartin–Löf, Per theory and constructive Zermelo–FraenkelZermelo, Ernst set theoryConstructive 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’sVoevodsky, Vladimir univalence axiomUnivalence axiom. A further goal is to investigate the strength of intuitionistic theories of generalized inductive definitionsInductive definition in the framework of intuitionistic explicit mathematicsExplicit mathematics that lie beyond the reach of Martin–Löf type theory.