DROPS

Artifact

Software

Constructive Notions of Ordinals in Homotopy Type Theory

Authors: Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh, Fredrik Nordvall Forsberg, and Chuangjie Xu

Abstract

Cite as

Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh, Fredrik Nordvall Forsberg, Chuangjie Xu. Constructive Notions of Ordinals in Homotopy Type Theory (Software, Repository). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-26786,
   title = {{Constructive Notions of Ordinals in Homotopy Type Theory}}, 
   author = {de Jong, Tom and Kraus, Nicolai and Mohammadzadeh, Aref and Nordvall Forsberg, Fredrik and Xu, Chuangjie},
   note = {Software, Royal Society URF\R1\191055, RF\ERE\210032, RF\ERE\231052, URF\R\241007, UK National Physical Laboratory Measurement Fellowship project "Dependent types for trustworthy tools", Engineering and Physical Sciences Research Council EP/Y000455/1, EP/Z000602/1, swhId: \href{https://archive.softwareheritage.org/swh:1:snp:af7a3d40f000eeb74aa0f06222f84f76e2046841;origin=https://bitbucket.org/nicolaikraus/constructive-ordinals-in-hott.git}{\texttt{swh:1:snp:af7a3d40f000eeb74aa0f06222f84f76e2046841}} (visited on 2026-07-09)},
   url = {https://bitbucket.org/nicolaikraus/constructive-ordinals-in-hott.git},
   doi = {10.4230/artifacts.26786},
}

Document

DOI: 10.4230/LIPIcs.LICS.2026.59

Generalized Decidability via Brouwer Trees

Authors: Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh, and Fredrik Nordvall Forsberg

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract

In the setting of constructive mathematics, we suggest and study a framework for decidability of properties, which allows for finer distinctions than just "decidable, semidecidable, or undecidable". We work in homotopy type theory and use Brouwer tree ordinals to specify the level of decidability of a property. In this framework, we express the property that a proposition is α-decidable, for an ordinal α, and show that it generalizes decidability and semidecidability. Further generalizing known results, we show that α-decidable propositions are closed under binary conjunction, and discuss for which α they are closed under binary disjunction. We prove that if each P(i) is semidecidable, then the countable meet ∀ i ∈ ℕ. P(i) is ω²-decidable, and similar results for countable joins and iterated quantifiers. We also discuss the relationship with countable choice. All our results are formalized in Cubical Agda.

Cite as

Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh, and Fredrik Nordvall Forsberg. Generalized Decidability via Brouwer Trees. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 59:1-59:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{dejong_et_al:LIPIcs.LICS.2026.59,
  author =	{de Jong, Tom and Kraus, Nicolai and Mohammadzadeh, Aref and Nordvall Forsberg, Fredrik},
  title =	{{Generalized Decidability via Brouwer Trees}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{59:1--59:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.59},
  URN =		{urn:nbn:de:0030-drops-268466},
  doi =		{10.4230/LIPIcs.LICS.2026.59},
  annote =	{Keywords: Decidability in constructive mathematics, homotopy type theory, ordinals, Brouwer trees, countable choice}
}

Search Results

Documents authored by Mohammadzadeh, Aref

Constructive Notions of Ordinals in Homotopy Type Theory

Abstract

Cite as

Generalized Decidability via Brouwer Trees

Abstract

Cite as

Thanks for your feedback!

Could not send message