Open Research Index

Generalized Decidability via Brouwer Trees

Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh, Fredrik Nordvall Forsberg

arXivarxiv/2602.10844Feb 11, 2026cs.LOscore 0

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 ordinals to specify the level of decidability of a property. In this framework, we express the property that a proposition is $α$-decidable, for a Brouwer ordinal $α$, and show that it generalizes decidability and semidecidability. Further generalizing known results, we show that $α$-decidable propositions are closed under binary conjunction, and…

SourceJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/arxiv/2602.10844
curl -X POST /api/v1/records/arxiv/2602.10844/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2602.10844/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'