🔢 mathematics

Generalized Decidability via Brouwer Trees

Dit artikel introduceert een raamwerk in homotopietheorie dat beslisbaarheid generaliseert met behulp van Brouwer-ordinalen om een hiërarchie van $\alpha$ -beslisbare proposities vast te stellen, waarbij hun afsluitingseigenschappen onder logische operaties en kwantoren worden gekarakteriseerd, waarbij alle resultaten geformaliseerd zijn in Cubical Agda.

Oorspronkelijke auteurs: Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh, Fredrik Nordvall Forsberg

Gepubliceerd 2026-07-10

📖 6 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh, Fredrik Nordvall Forsberg

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je een detective bent die een mysterie probeert op te lossen. In de wereld van de informatica verdelen we mysteries meestal in drie categorieën: Beslisbaar (we kunnen het antwoord snel vinden), Semibeslisbaar (we kunnen het antwoord vinden als het "ja" is, maar als het "nee" is, wachten we misschien eeuwig) en Onbeslisbaar (we kunnen het helemaal niet oplossen).

Maar wat als er mysteries zijn die "meer" semibeslisbaar zijn dan andere? Wat als sommige "ja"-antwoorden iets langer duren om te vinden, maar nog steeds niet eeuwig duren?

Dat is precies waar Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh en Fredrik Nordvall Forsberg onderzoek naar doen in hun nieuwe paper. Ze stellen een manier voor om exact te meten hoe lang het duurt om een "ja"-antwoord te vinden, met behulp van een speciaal getallensysteem genaamd Brouwer-boom-ordinaal. Denk hierbij niet aan gewone getallen zoals 1, 2, 3, maar aan een magische ladder van tijdstappen die veel verder gaat dan oneindigheid.

De Magische Ladder van de Tijd

In hun raamwerk zeggen ze niet alleen "het is oplosbaar." Ze zeggen: "Het is $\alpha$ -beslisbaar," waarbij $\alpha$ een specifieke sport is op hun magische ladder.

Niveau 1 (Beslisbaar): Als een probleem 1-beslisbaar is, betekent dit dat je het antwoord (of het bewijs dat het onmogelijk is) kunt vinden in een eindig aantal stappen. Het is als controleren of een getal priem is; je telt gewoon op, en uiteindelijk weet je het zeker.
Niveau $\omega + 1$ (Semibeslisbaar): Als een probleem $(\omega + 1)$ -beslisbaar is, betekent dit dat als het antwoord "ja" is, je het binnen $\omega$ stappen zult vinden. Maar $\omega$ is geen normaal getal; het vertegenwoordigt "voor eeuwig tellen". Dus, als het antwoord "ja" is, zul je het uiteindelijk vinden, maar als het "nee" is, blijf je misschien eeuwig door tellen zonder ooit te stoppen. Dit is de klassieke definitie van "semibeslisbaar".

De auteurs bewijzen dat dit nieuwe systeem perfect aansluit bij het oude systeem. Als je een probleem hebt dat "beslisbaar" is, past het op sport 1. Als het "semibeslisbaar" is, past het op $\omega + 1$ . Maar de magie is dat ze nu ook kunnen praten over sporten tussen deze niveaus, of ver daarboven.

Het Tweelingpriem Mysterie

Om te laten zien hoe dit werkt, gebruiken ze een beroemd wiskundig raadsel: de Tweelingpriemvermoeden. Dit vraagt: "Is er altijd een paar priemgetallen (zoals 3 en 5, of 11 en 13) die slechts twee getallen van elkaar verwijderd zijn, ongeacht hoe hoog je telt?"

Controleren of er één specifiek paar bestaat, is makkelijk (beslisbaar).
Controleren of er enig paar bestaat boven een bepaald getal, is semibeslisbaar (je blijft zoeken; als je er een vindt, stop je).
Maar de grote vraag is of dit waar is voor elk getal.

De auteurs laten zien dat deze specifieke vraag $\omega^2$ -beslisbaar is. Stel je voor dat $\omega$ een enkele oneindige lijn van stappen is. $\omega^2$ is als het hebben van een oneindig aantal van die lijnen op elkaar gestapeld. Het betekent dat als er een tegenvoorbeeld voor het Tweelingpriemvermoeden bestaat, je dat zou kunnen vinden, maar het kan een tijdsspanne kosten die gelijk staat aan het doorlopen van een oneindige stapel oneindige lijnen.

Ze keken ook naar wat er gebeurt als je deze problemen combineert:

EN: Als je twee problemen hebt die $\alpha$ -beslisbaar zijn, dan is hun "EN" (beide moeten waar zijn) ook $\alpha$ -beslisbaar. Het is als het controleren van twee vakjes; als je beide binnen hetzelfde tijdsbestek kunt controleren, zit je goed.
OF: Dit is lastiger. Als je twee problemen hebt, is hun "OF" (ofwel de een, ofwel de ander is waar) alleen gegarandeerd beslisbaar als de tijdslimiet klein genoeg is (specifiek, als het niveau iets is als $\omega \cdot k + n$ ). Als de tijdslimiet te groot wordt, kan de "OF" de regels van hun systeem breken.

Het "Keuze"-probleem

Hier wordt het echt interessant. De auteurs ontdekten dat als je een oneindig aantal "semibeslisbare" problemen wilt combineren (zoals het controleren van het Tweelingpriemvermoeden voor elk startgetal), je tegen een muur aanloopt. Zonder een speciale wiskundige regel genaamd Aftelbare Keuze (Countable Choice), kun je niet bewijzen dat het gecombineerde resultaat semibeslisbaar is.

Sterker nog, ze bewezen dat als je dat zonder die regel zou kunnen bewijzen, het andere fundamentele wetten van de logica zou schenden. Daarom suggereren ze dat je, om de wiskunde soepel te laten verlopen voor oneindige combinaties, de aanname van Aftelbare Keuze nodig hebt.

Ze hebben echter ook een workaround gevonden! Ze keken naar een ander type "semibeslisbaar", namelijk Sierpiński-semibeslisbaar. Dit is een iets zwakkere versie die wél toestaat om oneindige lijsten te combineren zonder de regel van Aftelbare Keuze nodig te hebben. Het is als het hebben van een ander soort zaklamp die misschien niet zo fel schijnt als de originele, maar die geen batterij (de Keuze-regel) nodig heeft om aan te gaan.

Wat ze niet hebben opgelost

Het is belangrijk om te weten wat dit paper niet doet. De auteurs zijn zeer duidelijk: ze hebben het Tweelingpriemvermoeden niet opgelost. Ze hebben het slechts gebruikt als een voorbeeld om te laten zien hoe hun nieuwe meetlat werkt.

Ze geven ook toe dat ze de volledige vorm van hun ladder nog niet kennen. Ze vermoeden dat als je een probleem hebt op sport $\alpha$ en een ander op $\beta$ , en $\alpha$ lager is dan $\beta$ , dan het probleem op $\alpha$ ook oplosbaar zou moeten zijn op $\beta$ . Maar ze hebben dit nog niet voor elke sport op de ladder bewezen. Het is een "conjectuur" (een sterke gok), geen feit.

De Kern van het Verhaal

Dit paper suggereert een nieuwe manier om te praten over hoe moeilijk het is om een "ja"-antwoord te vinden in de wiskunde en de informatica. In plaats van alleen te zeggen "we kunnen het vinden" of "dat kunnen we niet", geven ze ons een precieze liniaal gemaakt van oneindige stappen. Ze hebben bewezen dat deze liniaal werkt voor de zaken die we al kennen (beslisbaar en semibeslisbaar), en ze hebben het gebruikt om complexe problemen zoals het Tweelingpriemvermoeden te meten, waarbij ze vonden dat deze op een specifieke, meetbare hoogte van $\omega^2$ liggen.

Ze hebben ook aangetoond dat hoewel deze liniaal krachtig is, deze ook grenzen heeft: het combineren van oneindige lijsten van problemen vereist een specifieke aanname (Aftelbare Keuze), tenzij je overstapt op een iets ander soort liniaal (Sierpiński-semibeslisbaarheid).

Dit alles is gebouwd en gecontroleerd binnen een computerprogramma genaamd Cubical Agda, dat fungeert als een superstrenge scheidsrechter om er zeker van te zijn dat elke stap van hun logica perfect is. Dus hoewel de ideeën nieuw en opwindend zijn, is de wiskunde erachter ijzersterk.

Technische Samenvatting: Gegeneraliseerde Beslisbaarheid via Brouwer-bomen

Probleemstelling
In de constructieve wiskunde en synthetische berekenbaarheidstheorie is de standaardclassificatie van proposities als "beslisbaar", "semibeslisbaar" of "onbeslisbaar" vaak te grofmazig. Zo is de beslisbaarheid van priemgetalidentificatie duidelijk, maar de status van de Tweelingpriemgetalconjectuur (of er een tweelingpriempaar bestaat boven elke $n$ ) betreft een structuur van $\omega$ -veel semibeslisbare subproblemen. Klassiek gezien kan dit worden beschouwd als een limiet van limieten, maar constructieve kaders vereisen een preciezere manier om de "duur" of complexiteit van de zoektocht naar bewijs te meten. Bestaande concepten van ordinaalgetallen (bijv. syntactische Cantor-normaalvormen of semantische welgefundeerde relaties) bieden geen geschikt hiërarchisch systeem: syntactische benaderingen maken alle vergelijkingen beslisbaar (waardoor de hiërarchie instort), terwijl semantische benaderingen vaak er niet in slagen om vergelijkingen semibeslisbaar te maken. Het artikel adresseert de behoefte aan een kader dat een fijnere onderscheiding in beslisbaarheid mogelijk maakt, specifiek om proposities te karakteriseren die transfiniete stappen vereisen voor verificatie.

Methodologie
De auteurs werken binnen de Homotopietheorie (HoTT) en gebruiken Brouwer-boomordinaalgetallen ( $\text{Brw}$ ) als de fundering voor hun hiërarchie. Deze ordinaalgetallen worden gedefinieerd via een quotient inductive-inductive type (QIIT) die constructoren bevat voor nul, successoren en limieten van strikt toenemende sequenties. Cruciaal is dat de limietconstructor alleen strikt toenemende sequenties accepteert, wat ervoor zorgt dat eindigheid beslisbaar is terwijl het constructieve karakter van de theorie behouden blijft.

De kerndefinitie die wordt geïntroduceerd is $\alpha$ -beslisbaarheid: Een propositie $P$ is $\alpha$ -beslisbaar als er een ordinaal $y$ bestaat zodanig dat $P \leftrightarrow (\alpha \leq y)$ . Deze definitie generaliseert bestaande concepten:

$1$-beslisbaarheid (of $\omega$ -beslisbaarheid) komt overeen met standaard beslisbaarheid.
$(\omega + 1)$ -beslisbaarheid (equivalent aan $\omega \cdot 2$ -beslisbaarheid) komt overeen met semibeslisbaarheid.

De auteurs formaliseren alle resultaten in Cubical Agda, waarbij gebruik wordt gemaakt van de natuurlijke ondersteuning voor QIITs en univalente principes. Zij hanteren specifieke technieken om de complexiteit van het definiëren van functies op QIITs te beheersen, zoals het eerst definiëren van relaties op puntconstructoren en het later extraheren van functies om een combinatorische explosie in padconstructoren te vermijden.

Belangrijkste Bijdragen en Resultaten

Hiërarchie van Beslisbaarheid:
- Het artikel stelt vast dat $\alpha$ -beslisbaarheid beslisbaarheid en semibeslisbaarheid generaliseert.
- Er wordt aangetoond dat voor elk ordinaal $\alpha$ , $(\alpha+1)$ -beslisbaarheid equivalent is aan $(\alpha+\omega)$ -beslisbaarheid. Bijgevolg kan de hiërarchie effectief worden geïndexeerd door limiet-ordinaalgetallen (niet-successor ordinaalgetallen).
- De auteurs bewijzen dat als $P$ $\alpha$ -beslisbaar is en $Q$ $\alpha$ -beslisbaar is, dan $P \land Q$ ook $\alpha$ -beslisbaar is. Dit berust op de constructie van een binaire minimum functie voor niet-successor ordinaalgetallen, wat over het algemeen niet mogelijk is voor willekeurige ordinaalgetallen zonder de Limited Principle of Omniscience (LPO) te impliceren.
Disjunctie en Maxima:
- Hoewel conjunctie gesloten is op hetzelfde niveau, is binaire disjunctie niet gesloten voor willekeurige $\alpha$ . De auteurs bewijzen echter dat $(\omega \cdot k + n)$ -beslisbare proposities gesloten zijn onder binaire disjunctie. Dit vereist de constructie van een binaire maximum functie relatief aan ordinaalgetallen van de vorm $\omega \cdot k$ .
- Het bestaan van globale binaire maxima voor niet-successoren impliceert de aanwezigheid van LPO, een constructieve taboe.
Telbare Kwantoren en Families:
- Telbare Gemiddelden (Meets): Voor een familie van semibeslisbare proposities $P: \mathbb{N} \to \text{Prop}$ wordt bewezen dat de telbare meet $\forall i. P(i)$ $\omega^2$ -beslisbaar is. Dit resultaat wordt toegepast op de Tweelingpriemgetalconjectuur, waarbij deze als $\omega^2$ -beslisbaar wordt gekarakteriseerd.
- Telbare Joins: De telbare join $\exists i. P(i)$ van semibeslisbare proposities is getoond te $(\omega \cdot 3)$ -beslisbaar te zijn.
- Kwantor-alternaties: Het artikel analyseert formules met alternerende kwantoren. Voor een familie $P(n, m)$ waar $P(n, m) \to P(n, m+1)$ , wordt aangetoond dat de propositie $\exists m. \forall n. P(n, m)$ $(\omega^2 + \omega)$ -beslisbaar is. Dit levert een precieze ordinaal grens voor de zoektocht naar tegenvoorbeelden van de Tweelingpriemgetalconjectuur.
Relatie met Keuze-principes:
- De auteurs onderzoeken de impact van Telbare Keuze (AC). Onder aanname van AC wordt de telbare join van semibeslisbare proposities semibelsbaar (d.w.z. $(\omega \cdot 3)$ -beslisbaarheid convergeert naar $(\omega \cdot 2)$ -beslisbaarheid).
- Echter, zelfs met AC vervallen $\omega^2$ -beslisbare proposities niet naar semibelsbaar, tenzij Markov's Principe LPO impliceert.
- Het artikel introduceert Sierpiński-semibelsbaarheid (gebaseerd op de Sierpiński-type, de vrije $\omega$ -complete partiële orde) als een alternatieve notie van semibelsbaarheid die gesloten is onder telbare joins zonder Telbare Keuze aan te nemen. Er wordt getoond dat Sierpiński-semibelsbaarheid zwakker is dan standaard semibelsbaarheid.

Betekenis en Claims
De auteurs positioneren dit werk als de eerste stap naar een theorie van gegeneraliseerde beslisbaarheid. Zij claimen een kader te bieden waarin de "duur" van algoritmen (in een constructieve, abstracte zin) precies gespecificeerd en bewezen kan worden met behulp van ordinaal-rekenkunde.

Het artikel merkt bescheiden op dat het geen open problemen zoals de Tweelingpriemgetalconjectuur zelf oplost; het biedt eerder een formele taal om de complexiteit van dergelijke problemen te beschrijven. Het benadrukt dat de hiërarchie van beslisbaarheid nog niet volledig begrepen is, waarbij specifiek wordt opgemerkt dat het een open vraag blijft of $\alpha$ -beslisbaarheid $\beta$ -beslisbaarheid impliceert voor alle $\alpha \leq \beta$ (hoewel er gedeeltelijke resultaten zijn geleverd). Het werk laat ook de vraag open of Brouwer-boomordinaalgetallen de optimale notie voor deze theorie zijn, of dat alternatieve ordinaalconstructies potentieel andere, mogelijk rijkere hiërarchieën zouden opleveren.

Alle resultaten zijn rigoureus geformaliseerd in Cubical Agda, wat garandeert dat het constructieve karakter van de bewijzen behouden blijft en dat de definities van ordinaalgetallen en hun eigenschappen computationeel correct zijn binnen de type-theorie.