💻 computer science

Uniform Realizability Interpretations

Dit werk introduceert een nieuw kader voor uniforme realiserbaarheid dat diverse interpretaties van logica, met name de behandeling van atomaire formules en kwantoren, verenigt en generaliseert door de interpretatie te parametriseren op basis van de behandeling van atomaire formules.

Oorspronkelijke auteurs: Ulrich Berger, Paulo Oliva

Gepubliceerd 2026-03-05

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Ulrich Berger, Paulo Oliva

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

Uniform Realisability: Een Reis door de Wereld van Logica en Bewijzen

Stel je voor dat wiskundige bewijzen niet zomaar abstracte gedachten zijn, maar meer lijken op recepten voor een gerecht of instructies voor een robot. In de wereld van de logica (specifiek "Heyting rekenkunde", een manier om over getallen te redeneren zonder de wetten van de klassieke logica te gebruiken), willen we weten: Hebben we een echt, werkend bewijs, of is het alleen maar een theorie?

Dit artikel, geschreven door Ulrich Berger en Paulo Oliva, introduceert een nieuwe manier om naar deze bewijzen te kijken, genaamd "Uniform Realisability". Laten we dit uitleggen met een paar creatieve metaforen.

1. Het Probleem: De "Getuige" vs. De "Magische Sleutel"

In de traditionele manier om bewijzen te bekijken (zoals bedacht door Kleene in 1945), werkt het als een detectiveverhaal.

Als je zegt: "Er bestaat een getal dat een oplossing is" (een existential bewering), dan moet je bewijs een getuige leveren. Je moet de detective een specifiek getal geven (bijvoorbeeld: "Het is getal 42!") én het bewijs dat 42 werkt.
Als je zegt: "Voor elk getal geldt..." (een universeel bewering), dan moet je bewijs een machine zijn die voor elk willekeurig getal dat je invoert, het juiste antwoord produceert.

Het probleem: Soms is het te veel werk om voor elk bewijs een specifieke "getuige" te vinden. Soms willen we zeggen: "Er is een oplossing, maar ik geef je niet direct het getal, ik geef je een methode die voor iedereen werkt."

2. De Oplossing: De "Uniforme Sleutel"

De auteurs stellen een nieuw systeem voor: Uniform Realisability.

Stel je voor dat je een Sleutelkast hebt.

In het oude systeem moest je voor elke deur (elk bewijs) een unieke, specifieke sleutel vinden die precies in dat slot paste.
In dit nieuwe systeem hebben we één universele sleutel (of een universele methode) die voor alle deuren werkt, zolang we maar weten hoe we de deur moeten benaderen.

De kern van hun idee is dat ze de kern van het bewijs (de "atomen" of basisfeiten) loskoppelen van de structuur van het bewijs (de quantoren zoals "voor elk" en "er bestaat").

De Basis (Atomen): Dit is het "wat". Bijvoorbeeld: "Is dit getal een natuurlijk getal?" of "Zijn deze twee dingen gelijk?". Hier kunnen we kiezen hoe we het bewijzen. Soms geven we een exact getal, soms een schatting, soms een lijstje.
De Structuur (Quantoren): Dit is het "hoe". Hier gebruiken ze altijd dezelfde, uniforme regels. Of je nu over "alle" getallen praat of "er een" zoekt, de logica blijft hetzelfde: je hebt een methode nodig die voor iedereen werkt, zonder dat je eerst het specifieke antwoord hoeft te kennen.

3. Waarom is dit handig? (De "Bakkerij"-Analogie)

Stel je voor dat je een bakkerij runt (de logica).

Oude methode: Elke klant (bewijs) komt met een specifiek recept. Als ze een taart willen, moet je eerst de exacte hoeveelheid suiker meten en dan pas beginnen. Als ze een brood willen, moet je eerst het meel wegen. Het is veel werk om voor elke klant apart te beginnen.
Nieuwe methode (Uniform): Je hebt één super-oven (de uniforme interpretatie). Je zegt: "Ik heb een oven die voor elk recept werkt."
- Als de klant vraagt: "Is er een taart?" (Er bestaat een X), dan hoef je niet direct de taart te bakken. Je geeft ze de oven en zegt: "Deze oven kan elke taart bakken die je maar wilt."
- Als de klant vraagt: "Bak voor elke klant een brood" (Voor alle X), dan geeft je ze de oven en zegt: "Deze oven werkt voor elke klant, zonder dat ik eerst weet wie er komt."

Het grote voordeel is dat je flexibel bent. Je kunt kiezen wat de "oven" doet met de basis-ingrediënten (de atomen):

Kleene's manier: De oven geeft je het exacte getal (de exacte hoeveelheid suiker).
Kreisel's manier: De oven geeft je een lijstje met instructies (een type-systeem).
Herbrand's manier: De oven geeft je een lijstje met mogelijke opties (een setje getallen).
Leren Realisability (Aschieri-Berardi): De oven is een lerende robot. Hij begint met een lege kennisbank. Als hij een fout maakt, leert hij van de staat van de wereld en past hij zijn antwoord aan. Hij "leert" het antwoord onderweg.

4. Wat levert dit op?

De auteurs tonen aan dat al deze verschillende manieren om naar logica te kijken (die er heel anders uitzagen) eigenlijk allemaal speciale gevallen zijn van hun nieuwe, grote "Uniforme" systeem.

Het is alsof ze een universele vertaler hebben gebouwd.

Als je een tekst in het "Kleene-landschap" schrijft, vertaalt je systeem het naar hun universele taal.
Als je in het "Lerend-landschap" schrijft, vertaalt het systeem dat ook.

De voordelen voor de lezer (en de wiskunde):

Eén regel voor alles: Je hoeft niet voor elke nieuwe manier van bewijzen een heel nieuw systeem te bouwen. Je past alleen de "basisregels" (de atomen) aan.
Veiligheid: Ze bewijzen dat als je basisregels kloppen, alles wat je afleidt ook klopt. Het is een veilige manier om nieuwe wiskundige ideeën te testen.
Brug tussen werelden: Het maakt het makkelijker om te zien hoe een "klassieke" manier van denken (waar je mag zeggen "het is waar of niet waar" zonder te weten welke) kan worden vertaald naar een "constructieve" manier (waar je een bewijs moet leveren).

Conclusie

In simpele taal: Berger en Oliva hebben een meester-schakelbord ontworpen. In plaats van voor elk type logica een apart stopcontact te bouwen, hebben ze één groot paneel gemaakt. Je kunt de stekker (de basisfeiten) op verschillende plekken steken om verschillende soorten "licht" (bewijzen) te krijgen, maar de bedrading (de logica van de quantoren) blijft altijd hetzelfde en veilig.

Dit helpt wiskundigen om te begrijpen hoe verschillende manieren van redeneren met elkaar verbonden zijn, en hoe we bewijzen kunnen maken die niet alleen zeggen "het is waar", maar ook "hier is hoe je het kunt doen".

Titel: Uniforme Realiseerbaarheidsinterpretaties

Auteurs: Ulrich Berger (Swansea University) en Paulo Oliva (Queen Mary University of London)
Context: Essay opgedragen aan Stefano Berardi (EPTCS 441, 2026)

1. Het Probleem

Sinds Kleene's realisatie-interpretatie van Heyting-aritmetiek (HA) in 1945 zijn er vele varianten ontwikkeld, zoals Kreisel's gemodificeerde realisatie, "klassieke" realisatie, Herbrand-realisatie en "learning" realisatie. Een fundamenteel probleem in de bestaande literatuur is de heterogeniteit in de behandeling van kwantoren en atomaire formules:

Traditionele aanpak (bijv. Kleene): Realizers voor existentiële kwantoren ( $\exists n A(n)$ ) moeten expliciete getuigen (witnesses) bevatten (bijv. een getal $k_0$ dat $n$ is, en een realizer voor $A(k_0)$ ). Universele kwantoren vereisen een functie die voor elke invoer een realizer produceert.
Uniforme aanpak (bijv. Herbrand, Uniform HA): In sommige moderne interpretaties worden kwantoren "uniform" behandeld. Een realizer voor $\exists n A(n)$ hoeft $n$ niet expliciet te bevatten; het is voldoende dat er een $n$ bestaat waarvoor de realizer werkt. Een realizer voor $\forall n A(n)$ moet uniform voor alle $n$ werken.
De uitdaging: Er ontbreekt een unificerend raamwerk dat deze verschillende benaderingen (waarbij sommige kwantoren expliciete witnesses vereisen en andere niet) onder één theoretische noemer kan brengen. Het is moeilijk om de overeenkomsten en verschillen tussen deze interpretaties formeel te isoleren.

2. Methodologie

De auteurs introduceren een parametrisch raamwerk voor uniforme realiseerbaarheid. De kern van de methode is het scheiden van de interpretatie van atomaire predikaten van de interpretatie van logische connectieven en kwantoren.

Base Interpretation (Basisinterpretatie):
Voor een brontheorie $S$ (bijv. HA) en een doeltheorie $T$ , wordt een basisinterpretatie gedefinieerd die elk $n$ -plaatsig predikaat $P$ van $S$ koppelt aan een $(n+m)$ -plaatsige relatie $x \triangleright_P a$ in $T$ . Hierbij is $x$ het argument en $a$ de "realizer" of "witness" voor $P(x)$ .
Uniforme Realiseerbaarheid (Definitie 2.2):
De interpretatie van complexe formules wordt uniform gedefinieerd, ongeacht de specifieke keuze van de basisinterpretatie:
- Conjunctie: $a, b \text{ ur } A \land B \iff (a \text{ ur } A) \land (b \text{ ur } B)$
- Implicatie: $f \text{ ur } A \to B \iff \forall a ((a \text{ ur } A) \to (f(a)\downarrow \land f(a) \text{ ur } B))$
- Existentiële kwantor (Uniform): $a \text{ ur } \exists x A(x) \iff \exists x (a \text{ ur } A(x))$
  Let op: De realizer $a$ verandert niet; de existentie wordt in de doeltheorie $T$ uitgesproken.
- Universele kwantor (Uniform): $a \text{ ur } \forall x A(x) \iff \forall x (a \text{ ur } A(x))$
  Let op: Dezelfde realizer $a$ moet voor alle $x$ werken.
Behandeling van Kwalificatie:
De auteurs onderscheiden tussen ongekwalificeerde kwantoren ( $\forall x A(x)$ ) en gekwalificeerde kwantoren ( $\forall_N x A(x)$ ). Gekwalificeerde kwantoren worden gereduceerd tot ongekwalificeerde kwantoren gecombineerd met de interpretatie van het predikaat $N(x)$ . Dit stelt hen in staat om de variatie in interpretaties (bijv. of $N(n)$ een exact getal is of een bovengrens) te parametriseren via de basisinterpretatie van $N$ .

3. Belangrijkste Bijdragen

Unificerend Raamwerk: Het paper biedt een algemene definitie die diverse bestaande realisatie-interpretaties als specifieke instanties kan bevatten. Het isoleert de variatie in de behandeling van atomaire formules (zoals gelijkheid, onwaarheid, en natuurlijke getallen) van de uniforme behandeling van de logische structuur.
Algemene Geluidheid (Soundness): Het paper bewijst een algemene geluidheidstelling (Theorema 2.7). Als de niet-logische axioma's van de brontheorie realiseerbaar zijn onder een specifieke basisinterpretatie, dan zijn alle theorema's van die theorie realiseerbaar. Dit elimineert de noodzaak om voor elke nieuwe variant van realisatie een volledig nieuw bewijs te leveren; men hoeft alleen de axioma's te controleren.
Parametrisatie van Atomaire Predikaten: De auteurs analyseren drie manieren om het predikaat voor natuurlijke getallen $N(n)$ $N (n)$ te interpreteren:
- Uniform: $n \triangleright_N \langle \rangle \equiv \text{true}$ (geen extra informatie nodig).
- Benaderend: $n \triangleright_N a \equiv n \in a$ (waarbij $a$ een eindige verzameling is) of $n \leq a$ (bovengrens).
- Precies: $n \triangleright_N a \equiv n = a$ (de realizer is het getal zelf).
Behandeling van Onwaarheid ( $\bot$ ): Het raamwerk toont aan hoe verschillende behandelingen van $\bot$ (van volledig triviaal tot computationeel betekenisvol via Friedman-Dragalin vertaling) kunnen worden geïntegreerd.

4. Resultaten en Geïmplementeerde Instanties

De auteurs demonstreren dat hun raamwerk vijf bekende interpretaties dekt:

Kleene's Getalrealisatie: Wordt herwonnen door $N(n)$ exact te interpreteren ( $n=m$ ) en $\bot$ triviaal. De realizers zijn natuurlijke getallen die paren coderen.
Kreisel's Gemodificeerde Realisatie: Wordt herwonnen door totale functies te gebruiken (systeem T) en $N(n)$ exact te interpreteren. Hierdoor vallen definieerbaarheidsvoorwaarden weg.
Herbrand Realisatie (Niet-standaard aritmetiek): Hierbij wordt $N(n)$ uniform geïnterpreteerd ( $\text{true}$ ), terwijl een nieuw predikaat $st(n)$ (standaard getallen) benaderend wordt geïnterpreteerd ( $n \in S$ met $S$ een eindige verzameling). Dit verklaart de uniforme behandeling van interne kwantoren.
Klassieke Realisatie: Door $\bot$ te interpreteren via een predikaat $P(a)$ , kunnen negaties computationele inhoud krijgen. Dit combineert gemodificeerde realisatie met de A-vertaling.
Aschieri-Berardi "Learning" Realisatie: Hierbij wordt de staat van kennis ( $s$ ) als parameter gebruikt. Realizers zijn state transformers. De interpretatie van gelijkheid en onwaarheid hangt af van of de staat een vast punt is van de transformer. Dit maakt het mogelijk om de wet van uitgesloten midden voor $\Sigma^0_1$ -formules te interpreteren.

5. Significantie

Theoretische Unificatie: Het paper lost de versnippering in het veld van realisatie-interpretaties op door te tonen dat veel verschillen slechts variaties zijn in de interpretatie van atomaire predikaten, terwijl de logische structuur uniform blijft.
Flexibiliteit: Het raamwerk maakt het mogelijk om nieuwe interpretaties te ontwerpen door simpelweg de basisinterpretatie van predikaten aan te passen, zonder de complexe logica opnieuw te definiëren.
Extensie naar Klassieke Logica: Het raamwerk ondersteunt de integratie van klassiek geldige formules (zoals dubbele negatie-eliminatie voor uniforme formules) als axioma's, zolang deze alleen uniforme predikaten bevatten.
Toekomstperspectief: De auteurs merken op dat hoewel het raamwerk momenteel voor eerste-orde theorieën is, het eenvoudig naar eindige typen kan worden uitgebreid. Een belangrijke open vraag blijft de conservativiteit: of de uitgebreide theorie (met gekwalificeerde en ongekwalificeerde kwantoren) conservatief is over de oorspronkelijke theorie.

Kortom, dit paper biedt een fundamentele theoretische basis die de diversiteit van moderne realisatie-interpretaties verenigt en een robuust mechanisme biedt voor het bewijzen van geluidheid voor nieuwe varianten.