natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
basic constructions:
strong axioms
further
This is a stub collecting information on the proof theoretic strength of univalent type theory with higher inductive types.
Setzer computes the strength of MLTT+W. Voevodsky reduces Coq’s inductive types to W-types. Coquand et al reduces univalence and some HITs to an unspecified constructive framework, which can be taken to be CZF+REA with a sequence of universes. It follows from this work that univalent type theory and these HITs has the same proof theoretic strength as MLTT with inductive definitions and a sequence of universes.
There is an MO-question on the proof theoretic strength of pCIC. Avigad provide a general overview of the proof theory of predicative constructive systems.
This section collects some references that establish the strength various type theories, roughly in increasing order of strength.
Let $\mathrm{ML}_n$ denote MLTT without inductive types and $n$ universes closed under $\Pi$ and $\Sigma$. This has the strength of the first-order system of $n$ iterated fixed points (whether with intuitionistic or classical logic), and thus by Feferman 1982 has proof-theoretic ordinal $\xi_n$, where $\xi_0=\varepsilon_0$ and $\xi_{n+1} = \varphi(\xi_n,0)$.
Jeremy Avigad, Proof Theory, 2014 PDF
Thierry Coquand et al, Variation on Cubical sets, 2014 PDF.
Solomon Feferman, Iterated inductive fixed-point theories: application to Hancock’s conjecture, Stud. Logic Foundations Math., 109, 1982.
Anton Setzer, Proof theoretical strength of Martin-Lof Type Theory with W-type and one universe PDF.
Anton Setzer, Proof theory of Martin-Löf type theory. An overview PDF
Vladimir Voevodsky, Notes on type systems 2011 PDF.
Last revised on August 5, 2023 at 14:29:05. See the history of this page for a list of all contributions to it.