{"id":"arxiv/2602.10844","url":"https://arxiv.org/abs/2602.10844","tags":["cs.LO","math.LO"],"score":0,"title":"Generalized Decidability via Brouwer Trees","domain":"cs.LO","source":"arxiv","authors":["Tom de Jong","Nicolai Kraus","Aref Mohammadzadeh","Fredrik Nordvall Forsberg"],"reviews":0,"subject":"cs.LO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-02-11","reactions":{}}