DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2024.44

Conservativity of Type Theory over Higher-Order Arithmetic

Authors: Daniël Otten and Benno van den Berg

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract

We investigate how much type theory can prove about the natural numbers. A classical result in this area shows that dependent type theory without any universes is conservative over Heyting Arithmetic (HA). We build on this result by showing that type theories with one level of impredicative universes are conservative over Higher-order Heyting Arithmetic (HAH). This result clearly depends on the specific type theory in question, however, we show that the interpretation of logic also plays a major role. For proof-irrelevant interpretations, we will see that strong versions of type theory prove exactly the same higher-order arithmetical formulas as HAH. Conversely, for proof-relevant interpretations, they prove different second-order arithmetical formulas than HAH, while still proving exactly the same first-order arithmetical formulas. Along the way, we investigate the various interpretations of logic in type theory, and to what extent dependent type theories can be seen as extensions of higher-order logic. We apply our results by proving a De Jongh’s theorem for type theory.

Cite as

Daniël Otten and Benno van den Berg. Conservativity of Type Theory over Higher-Order Arithmetic. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 44:1-44:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{otten_et_al:LIPIcs.CSL.2024.44,
  author =	{Otten, Dani\"{e}l and van den Berg, Benno},
  title =	{{Conservativity of Type Theory over Higher-Order Arithmetic}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{44:1--44:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.44},
  URN =		{urn:nbn:de:0030-drops-196873},
  doi =		{10.4230/LIPIcs.CSL.2024.44},
  annote =	{Keywords: Conservativity, Arithmetic, Realizability, Calculus of Inductive Constructions}
}

Search Results

Documents authored by Otten, Daniël

Conservativity of Type Theory over Higher-Order Arithmetic

Abstract

Cite as

Thanks for your feedback!

Could not send message