🔢 mathematics

Generalized Decidability via Brouwer Trees

Diese Arbeit führt ein Framework in der Homotopietheorie ein, das Entscheidbarkeit unter Verwendung von Brouwer-Ordinalen generalisiert, um eine Hierarchie von $\alpha$ -entscheidbaren Propositionen zu etablieren, deren Abgeschlossenheitseigenschaften unter logischen Operationen und Quantoren charakterisiert, wobei alle Ergebnisse in Cubical Agda formalisiert sind.

Ursprüngliche Autoren: Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh, Fredrik Nordvall Forsberg

Veröffentlicht 2026-07-10

📖 6 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh, Fredrik Nordvall Forsberg

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich vor, Sie sind ein Detektiv, der versucht, ein Rätsel zu lösen. In der Welt der Informatik sortieren wir Rätsel üblicherweise in drei Eimer: entscheidbar (wir können die Antwort schnell finden), semientscheidbar (wir können die Antwort finden, wenn sie „Ja“ lautet, aber wenn sie „Nein“ lautet, warten wir vielleicht ewig) und unentscheidbar (wir können es überhaupt nicht lösen).

Aber was wäre, wenn es Rätsel gibt, die „mehr“ semientscheidbar sind als andere? Was wäre, wenn einige „Ja“-Antworten etwas länger brauchen, um gefunden zu werden, aber dennoch nicht ewig dauern?

Genau das erforschen Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh und Fredrik Nordvall Forsberg in ihrem neuen Paper. Sie schlagen einen Weg vor, um genau zu messen, wie lange es dauert, eine „Ja“-Antwort zu finden, indem sie ein spezielles Zahlensystem namens Brouwer-Baum-Ordinalzahlen verwenden. Denken Sie dabei nicht an normale Zahlen wie 1, 2, 3, sondern an eine magische Leiter von Zeitschritten, die weit über die Unendlichkeit hinausgeht.

Die magische Leiter der Zeit

In ihrem Framework sagen sie nicht einfach nur „es ist lösbar“. Sie sagen: „Es ist $\alpha$ -entscheidbar“, wobei $\alpha$ eine spezifische Sprosse auf ihrer magischen Leiter ist.

Level 1 (Entscheidbar): Wenn ein Problem 1-entscheidbar ist, bedeutet das, dass man die Antwort (oder den Beweis für ihre Unmöglichkeit) in einer endlichen Anzahl von Schritten finden kann. Es ist wie die Prüfung, ob eine Zahl prim ist; man zählt einfach hoch, und schließlich weiß man es sicher.
Level $\omega + 1$ (Semientscheidbar): Wenn ein Problem $(\omega + 1)$ -entscheidbar ist, bedeutet das: Wenn die Antwort „Ja“ lautet, werden Sie sie innerhalb von $\omega$ Schritten finden. Aber $\omega$ ist keine normale Zahl; es repräsentiert das „ewige Zählen“. Das heißt, wenn die Antwort „Ja“ ist, werden Sie sie irgendwann finden, aber wenn die Antwort „Nein“ ist, werden Sie vielleicht ewig weiterzählen, ohne jemals anzuhalten. Dies ist die klassische Definition von „semientscheidbar“.

Die Autoren beweisen, dass dieses neue System perfekt mit dem alten übereinstimmt. Wenn Sie ein Problem haben, das „entscheidbar“ ist, passt es auf Sprosse 1. Wenn es „semientscheidbar“ ist, passt es auf Sprosse $\omega + 1$ . Aber die Magie liegt darin, dass sie nun auch über Sprossen zwischen diesen oder weit darüber hinaus sprechen können.

Das Zwilling Primzahl-Rätsel

Um zu zeigen, wie das funktioniert, nutzen sie ein berühmtes mathematisches Rätsel: die Zwilling Primzahlvermutung. Diese fragt: „Gibt es immer ein Paar von Primzahlen (wie 3 und 5, oder 11 und 13), die nur zwei Zahlen voneinander entfernt sind, egal wie hoch man zählt?“

Zu prüfen, ob ein spezifisches Paar existiert, ist einfach (entscheidbar).
Zu prüfen, ob irgendein Paar existiert, ist semientscheidbar (man sucht einfach weiter; wenn man eines findet, hört man auf).
Aber die große Frage ist, ob dies für jede Zahl wahr ist.

Die Autoren zeigen, dass diese spezifische Frage $\omega^2$ -entscheidbar ist. Stellen Sie sich $\omega$ als eine einzige unendliche Linie von Schritten vor. $\omega^2$ ist wie das Vorhandensein einer unendlichen Anzahl solcher Linien, die übereinander gestapelt sind. Das bedeutet: Wenn ein Gegenbeispiel zur Zwilling Primzahlvermutung existiert, könnten Sie es finden, aber es könnte eine Zeitspanne dauern, die dem Durchwandern eines unendlichen Stapels unendlicher Linien entspricht.

Sie haben auch untersucht, was passiert, wenn man diese Probleme kombiniert:

UND: Wenn Sie zwei Probleme haben, deren „UND“ (beide müssen wahr sein) auch $\alpha$ -entscheidbar ist. Es ist, als würde man zwei Kästchen prüfen; wenn man beide innerhalb desselben Zeitlimits prüfen kann, ist alles in Ordnung.
ODER: Dies ist kniffliger. Wenn Sie zwei Probleme haben, ist ihr „ODER“ (eines von beiden muss wahr sein) nur dann garantiert entscheidbar, wenn das Zeitlimit klein genug ist (speziell, wenn das Level so etwas wie $\omega \cdot k + n$ ist). Wenn das Zeitlimit zu riesig wird, könnte das „ODER“ die Regeln ihres Systems verletzen.

Das „Wahl“-Problem

Hier wird es besonders interessant. Die Autoren fanden heraus, dass man, wenn man eine unendliche Anzahl von „semientscheidbaren“ Problemen kombinieren möchte (wie das Prüfen der Zwilling Primzahlvermutung für jede Startzahl), gegen eine Wand stößt. Oh_ne eine spezielle mathematische Regel namens Zählbare Auswahl (Countable Choice) können Sie nicht beweisen, dass das kombinierte Ergebnis semientscheidbar ist.

Tatsächlich haben sie bewiesen, dass, falls man dies ohne diese Regel beweisen könnte, es andere grundlegende Gesetze der Logik verletzen würde. Daher schlagen sie vor, dass man die Zählbare Auswahl voraussetzen muss, damit die Mathematik für unendliche Kombinationen reibungslos funktioniert.

Sie haben jedoch auch einen Workaround gefunden! Sie untersuchten eine andere Art von „semientscheidbar“, nämlich Sierpiński-semientscheidbar. Dies ist eine etwas schwächere Version, die es tatsächlich erlaubt, unendliche Listen zu kombinieren, ohne die Regel der Zählbaren Auswahl zu benötigen. Es ist wie eine andere Art von Taschenlampe, die zwar nicht ganz so hell leuchtet wie das Original, aber keine Batterie (die Wahl-Regel) benötigt, um einzuschalten.

Was sie nicht gelöst haben

Es ist wichtig zu wissen, was dieses Paper nicht tut. Die Autoren sind sehr deutlich: Sie haben die Zwilling Primzahlvermutung nicht gelöst. Sie haben sie lediglich als Spielzeugbeispiel verwendet, um zu zeigen, wie ihr neuer Messstab funktioniert.

Sie geben auch zu, dass sie die volle Gestalt ihrer Leiter noch nicht kennen. Sie vermuten, dass wenn man ein Problem auf Sprosse $\alpha$ und ein anderes auf $\beta$ hat und $\alpha$ niedriger als $\beta$ ist, das Problem auf $\alpha$ auch auf $\beta$ lösbar sein sollte. Aber sie haben dies noch nicht für jede einzelne Sprosse der Leiter bewiesen. Es ist eine „Vermutung“ (eine starke Annahme), kein Fakt.

Das Faztelement

Dieses Paper schlägt einen neuen Weg vor, um darüber zu sprechen, wie schwierig es ist, eine „Ja“-Antwort in der Mathematik und Informatik zu finden. Anstatt nur zu sagen „wir können es finden“ oder „wir können es nicht“, geben sie uns ein präzises Lineal aus unendlichen Schritten. Sie haben bewiesen, dass dieses Lineal für die Dinge funktioniert, die wir bereits kennen (entscheidbar und semientscheidbar), und sie haben es genutzt, um komplexe Probleme wie die Zwilling Primzahlvermutung zu messen, wobei sie feststellten, dass diese auf einer spezifischen, messbaren Höhe von $\omega^2$ liegen.

Sie haben auch gezeigt, dass dieser Messstab zwar mächtig ist, aber auch Grenzen hat: Das Kombinieren unendlicher Listen von Problemen erfordert die Voraussetzung der Zählbaren Auswahl, es sei denn, man wechselt zu einer etwas anderen Art von Messstab (der Sierpiński-Semientscheidbarkeit).

All dies wurde innerhalb eines Computerprogramms namens Cubical Agda aufgebaut und überprüft, das als superstrenger Schiedsrichter fungiert, um sicherzustellen, dass jeder einzelne Schritt ihrer Logik perfekt ist. Während die Ideen also neu und aufregend sind, ist die Mathematik dahinter absolut solide.

Technisches Resümee: Generalisierte Entscheidbarkeit mittels Brouwer-Bäumen

Problemstellung
In der konstruktiven Mathematik und der synthetischen Berechenbarkeitstheorie ist die Standardklassifizierung von Propositionen in „entscheidbar“, „semidecidabel“ oder „unentscheidbar“ oft zu grob gefasst. Beispielsweise ist die Entscheidbarkeit der Primzahlprüfung klar, doch der Status der Zwillingsprimzahlvermutung (ob eine Zwillingsprimzahl-Paarung oberhalb von $n$ existiert) beinhaltet eine Struktur von $\omega$ -vielen semidecidablen Teilproblemen. Klassisch betrachtet könnte dies als ein Limit von Limiten gesehen werden, aber konstruktive Frameworks erfordern eine präzisere Methode, um die „Dauer“ oder Komplexität der Suche nach Evidenz zu messen. Bestehende Konzepte von Ordinalzahlen (z. B. syntaktische Cantor-Normalformen oder semantische wohldefinierte Relationen) bieten keine geeignete Hierarchie: Syntaktische Ansätze machen alle Vergleiche entscheidbar (was die Hierarchie kollabieren lässt), während semantische Ansätze oft daran scheitern, Vergleiche semidecidabel zu machen. Die vorliegende Arbeit adresset das Bedürfnis nach einem Framework, das es ermöglicht, feinere Unterscheidungen in der Entscheidbarkeit vorzunehmen, insbesondere um Propositionen zu charakterisieren, die transfinite Schritte zur Verifizierung erfordern.

Methodik
Die Autoren arbeiten innerhalb der Homotopietheorie (HoTT) und nutzen Brouwer-Baum-Ordinalzahlen ( $\text{Brw}$ ) als Fundament für ihre Hierarchie. Diese Ordinalzahlen werden über einen Quotienten-induktiv-induktiven Typ (QIIT) definiert, der Konstruktoren für Null, Nachfolger und Limiten streng steigender Sequenzen enthält. Entscheidend ist, dass der Limit-Konstruktor nur streng steigende Sequenzen akzeptiert, was sicherstellt, dass Endlichkeit entscheidbar bleibt, während die konstruktive Natur der Theorie gewahrt wird.

Die zentrale Einführung lautet $\alpha$ -Entscheidbarkeit: Eine Proposition $P$ ist $\alpha$ -entscheidbar, wenn es ein Ordinal $y$ gibt, sodass $P \leftrightarrow (\alpha \leq y)$ . Diese Definition generalisiert bestehende Konzepte:

$1$-Entscheidbarkeit (oder $\omega$ -Entscheidbarkeit) entspricht der Standard-Entscheidbarkeit.
$(\omega + 1)$ -Entscheidbarkeit (äquivalent zu $\omega \cdot 2$ -Entscheidbarkeit) entspricht der Semidecidierbarkeit.

Die Autoren formalisieren alle Ergebnisse in Cubical Agda unter Ausnutzung der nativen Unterstützung für QIITs und Univalenz. Sie verwenden spezifische Techniken, um die Komplexität der Definition von Funktionen auf QIITs zu bewältigen, etwa indem sie Relationen auf Punkt-Konstruktoren zuerst definieren und Funktionen erst später extrahieren, um eine kombinatorische Explosion in der Handhabung von Pfad-Konstruktoren zu vermeiden.

Zentrale Beiträge und Ergebnisse

Hierarchie der Entscheidbarkeit:
- Das Paper etabliert, dass $\alpha$ -Entscheidbarkeit die Entscheidbarkeit und Semidecidierbarkeit generalisiert.
- Es wird gezeigt, dass für jedes Ordinal $\alpha$ die $(\alpha+1)$ -Entscheidbarkeit äquivalent zur $(\alpha+\omega)$ -Entscheidbarkeit ist. Folglich kann die Hierarchie effektiv durch Limit-Ordinale (Nicht-Nachfolger-Ordinale) indiziert werden.
- Die Autoren beweisen, dass wenn $P$ $\alpha$ -entscheidbar und $Q$ $\alpha$ -entscheidbar ist, dann auch $P \land Q$ $\alpha$ -entscheidbar ist. Dies beruht auf der Konstruktion einer binären Minimum-Funktion für Nicht-Nachfolger-Ordinale, was für beliebige Ordinale ohne die Implikation des Limited Principle of Omniscience (LPO) nicht allgemein möglich ist.
Disjunktion und Maxima:
- Während die Konjunktion auf demselben Niveau abgeschlossen ist, ist die binäre Disjunktion für beliebige $\alpha$ nicht abgeschlossen. Die Autoren beweisen jedoch, dass $(\omega \cdot k + n)$ -entscheidbare Propositionen unter binärer Disjunktion abgeschlossen sind. Dies erfordert die Konstruktion einer binären Maximum-Funktion relativ zu Ordinalen der Form $\omega \cdot k$ .
- Die Existenz globaler binärer Maxima für Nicht-Nachfolger wird gezeigt, impliziert jedoch LPO, ein konstruktives Tabu.
Zählbare Quantoren und Familien:
- Zählbare Schnitte (Meets): Für eine Familie semidecidabler Propositionen $P: \mathbb{N} \to \text{Prop}$ wird bewiesen, dass der zählbare Schnitt $\forall i. P(i)$ $\omega^2$ -entscheidbar ist. Dieses Resultat wird auf die Zwillingsprimzahlvermutung angewendet, indem diese als $\omega^2$ -entscheidbar charakterisiert wird.
- Zählbare Vereinigungen (Joins): Die zählbare Vereinigung $\exists i. P(i)$ von semidecidablen Propositionen ist gezeigt zu $(\omega \cdot 3)$ -entscheidbar.
- Quantor-Alternationen: Das Paper analysiert Formeln mit alternierenden Quantoren. Für eine Familie $P(n, m)$ , bei der $P(n, m) \to P(n, m+1)$ gilt, wird gezeigt, dass die Proposition $\exists m. \forall n. P(n, m)$ $(\omega^2 + \omega)$ -entscheidbar ist. Dies liefert eine präzise Ordinal-Schranke für die Suche nach Gegenbeispielen zur Zwillingsprimzahlvermutung.
Beziehung zu Auswahlprinzipien:
- Die Autoren untersuchen den Einfluss der Zählbaren Auswahl (AC). Unter Annahme von AC wird die zählbare Vereinigung semidecidabler Propositionen semidecidabel (d. h. $(\omega \cdot 3)$ -entscheidbar kollabiert zu $(\omega \cdot 2)$ -entscheidbar).
- Selbst mit AC kollabieren $\omega^2$ -entscheidbare Propositionen nicht zu semidecidablen, sofern Markovs Prinzip nicht LPO impliziert.
- Das Paper führt die Sierpiński-Semidecidierbarkeit (basierend auf dem Sierpiński-Typ, dem freien $\omega$ -vollständigen partiellen Ordnungsverband) als alternatives Konzept der Semidecidierbarkeit ein, welches unter der Annahme von Zählbarer Auswahl unter der zählbaren Vereinigung abgeschlossen ist. Es wird gezeigt, dass die Sierpiński-Semidecidierbarkeit schwächer ist als die Standard-Semidecidierbarkeit.

Signifikanz und Behauptungen
Die Autoren positionieren diese Arbeit als den ersten Schritt hin zu einer Theorie der generalisierten Entscheidbarkeit. Sie behaupten, ein Framework bereitgestellt zu haben, in dem die „Dauer“ von Algorithmen (in einem konstruktiven, abstrakten Sinne) präzise spezifiziert und unter Verwendung von Ordinalarithmetik bewiesen werden kann.

Das Paper merkt bescheiden an, dass es keine offenen Probleme wie die Zwillingsprimzahlvermutung selbst löst; vielmehr bietet es eine formale Sprache, um die Komplexität solcher Probleme zu beschreiben. Es hebt hervor, dass die Hierarchie der Entscheidbarkeit noch nicht vollständig verstanden ist, insbesondere da es eine offene Frage bleibt, ob $\alpha$ -Entscheidbarkeit $\beta$ -Entscheidbarkeit für alle $\alpha \leq \beta$ impliziert (obwohl partielle Ergebnisse geliefert werden). Die Arbeit lässt zudem offen, ob Brouwer-Baum-Ordinale die optimale Vorstellung für diese Theorie sind oder ob alternative Ordinalkonstruktionen zu anderen, potenziell reicheren Hierarchien führen könnten.

Alle Ergebnisse sind rigoros in Cubical Agda formalisiert, wodurch sichergestellt wird, dass die konstruktive Natur der Beweise gewahrt bleibt und die Definitionen der Ordinale sowie deren Eigenschaften rechentechnisch innerhalb der Typentheorie fundiert sind.

Die magische Leiter der Zeit

Das Zwilling Primzahl-Rätsel

Das „Wahl“-Problem

Was sie nicht gelöst haben

Das Faztelement

Mehr davon