An independence of the MIN principle from the PHP principle

Technische Samenvatting: Onafhankelijkheid van het MIN-principe van het PHP-principe

Probleemstelling
Het artikel behandelt een centraal thema in de propositional bewijscomplexiteit en de begrenste rekenkunde: het begrijpen van de relatieve sterkte van bewijssystemen en het vaststellen van ondergrenzen voor bewijslengte. Specifiek onderzoekt de auteur de logische onafhankelijkheid van het Minimalisatieprincipe (MIN) van het Duivenhokprincipe (PHP) binnen het kader van gerelativeerde begrenste rekenkunde.

Het minimalisatieprincipe, $MIN(\triangleleft)$, stelt dat elke strikte lineaire ordening $\triangleleft$ op een eindig interval $[0, \dots, n)$ een kleinste element bezit. Dit principe is bekend als bewijsbaar in de theorie $T^2_2(\triangleleft)$, maar niet in het zwakkere fragment $T^1_2(\triangleleft)$. Het duivenhokprincipe, $PHP$, stelt dat er geen injectieve afbeelding bestaat van een verzameling van grootte $n+1$ naar een verzameling van grootte $n$. Hoewel $PHP$ onbewijsbaar is, zelfs in sterke theorieën zoals $T_2(\alpha)$, is de status ervan ten opzichte van $MIN$ in zwakkere uitbreidingen minder duidelijk.

De kernvraag is of de theorie $T^1_2(\triangleleft)$, aangevuld met alle instanties van het duivenhokprincipe voor $\Delta^b_1(\triangleleft)$-formules (aangeduid als $PHP(\Delta^b_1(\triangleleft))$), voldoende is om $MIN(\triangleleft)$ te bewijzen. Het artikel beoogt aan te tonen dat deze uitbreiding onvoldoende is, waardoor wordt vastgesteld dat $T^1_2(\triangleleft) + PHP(\Delta^b_1(\triangleleft))$ niet $MIN(\triangleleft)$ bewijst.

Methodologie
Het bewijs maakt gebruik van een modeltheoretische constructie die doet denken aan forcing, gestructureerd als een spel gespeeld tussen drie partijen over een telbaar niet-standaard model $M$ van ware rekenkunde. Het doel is om een expansie te construeren van een substructuur $I \subset M$ door een binaire relatie $\triangleleft$ te definiëren die specifieke eigenschappen voldoet terwijl andere worden geschonden.

1. Het Spelkader:
   De constructie wordt beschouwd als een spel $G_O$ dat gedurende telbaar veel stappen wordt gespeeld tussen drie spelers:

   • $P_{MIN}$: Streeft ernaar een strikte lineaire ordening op $[0, \dots, n)$ te construeren die geen kleinste element heeft, waardoor $MIN(\triangleleft)$ wordt gefalsificeerd.
   • $P_{IND}$: Streeft ernaar dat de resulterende structuur voldoet aan polynoominductie ($\Sigma^b_1(\triangleleft)$-inductie), waardoor de theorie $T^1_2(\triangleleft)$ behouden blijft.
   • $P_{PHP}$: Streeft ernaar dat de structuur voldoet aan alle instanties van het duivenhokprincipe voor $\Delta^b_1(\triangleleft)$-formules.

   Het spel verloopt in rondes waarin spelers een partiële ordeningsvoorwaarde $o \in O$ (een eindige reeks van verschillende getallen) uitbreiden. De uiteindelijke relatie $\triangleleft$ is de vereniging van deze voorwaarden.

2. Winnende Strategieën:

   • Strategie voor $P_{MIN}$: Gebruikt een externe telbare wachtrij om ervoor te zorgen dat elk element uiteindelijk wordt ingevoegd en dat elk element een kleiner voorganger heeft, waardoor een totale ordening zonder minimum wordt gegarandeerd.
   • Strategie voor $P_{IND}$: Leunt op een klassiek resultaat van Paris en Wilkie (uitgebreid door Riis), waarbij wordt gegarandeerd dat voor elke $\Sigma^b_1$-formule, als er een getuige bestaat, een "settling"-voorwaarde kan worden gevonden die het principe van het kleinste getal garandeert.
   • Strategie voor $P_{PHP}$ (De Kernbijdrage): Dit is het technisch veeleisendste deel. De speler moet ervoor zorgen dat voor elke $\Delta^b_1(\triangleleft)$-formule $\phi$, de relatie gedefinieerd door $\phi$ geen injectie is van een grotere verzameling $p$ naar een kleinere verzameling $h$.

3. Combinatorische Analyse (De "Array"-methode):
   Om te bewijzen dat $P_{PHP}$ een winnende strategie heeft, introduceert de auteur het concept van $(o, p, h)$-PHP-arrays. Dit zijn definieerbare families van voorwaarden die de mogelijke uitkomsten van orakelberekeningen voor $\Delta^b_1$-formules vertegenwoordigen.

   • Het bewijs stelt een ondergrens vast voor de grootte van dergelijke arrays door ze uit te breiden tot uniforme bomen (analoog aan beslissingsbomen voor orakelqueries).
   • Het stelt een bovengrens vast voor de grootte van elke verzameling van paarsgewijs incompatibele voorwaarden in het forcing-positie.
   • Door deze grenzen te vergelijken, leidt de auteur een contradictie af als $p > h$: het bestaan van een geldige array impliceert $p \le h$. Bijgevolg kan, als $p > h$, de speler $P_{PHP}$ altijd een schending van injectiviteit afdwingen (door ofwel een botsing of een ontbrekende waarde te vinden), waardoor het PHP-principe geldt.

Belangrijkste Bijdragen en Resultaten

• Hoofdstelling: Het artikel bewijst dat $T^1_2(\triangleleft) + PHP(\Delta^b_1(\triangleleft)) \nvdash \forall n MIN(\triangleleft)_n$.
  • Dit resultaat scheidt de sterkte van $T^2_2(\triangleleft)$ (dat $MIN$ bewijst) van de uitbreiding van $T^1_2$ door het duivenhokprincipe.
  • Het impliceert dat in de gerelativeerde setting de theorie $T^1_2(\triangleleft) + PHP(\Delta^b_1(\triangleleft))$ en $T^2_2(\triangleleft)$ onvergelijkbaar zijn in sterkte: de eerste bewijst geen $MIN$, terwijl de tweede geen gewone PHP bewijst.
• Combinatorische Techniek: Het artikel ontwikkelt een verfijnde combinatorische methode die PHP-arrays en MIN-bomen omvat. Deze techniek maakt nauwkeurige telling van voorwaardegroottes in de forcing-constructie mogelijk, wat een verbetering is ten opzichte van eerdere ondergrensargumenten om exacte grootte-schattingen te bieden.
• Aanvullende Scheidingen: De methodologie wordt toegepast om verdere onafhankelijkheidsresultaten aan te tonen:
  • Modellen van $T^1_2(\alpha) + PHP(\Delta^b_1(\alpha))$ kunnen worden geconstrueerd die het Dual Weak Pigeonhole Principle (dWPHP) falen.
  • Modellen kunnen worden geconstrueerd die het Tournament Principle (TOUR) falen.
  • De constructie kan worden gemodificeerd om modellen te produceren waarin de ordening $\triangleleft$ een dichte lineaire ordening is op specifieke deelverzamelingen.

Beteekenis en Claims
Het artikel claimt een nieuwe route te bieden naar het begrijpen van open problemen in de begrenste rekenkunde, zoals de scheiding van aangrenzende theorieën $T^i_2$ en $T^{i+1}_2$, en het $R(\log)$-probleem. Door aan te tonen dat het toevoegen van het duivenhokprincipe aan $T^1_2$ niet leidt tot het minimalisatieprincipe, benadrukt het werk de beperkingen van combinatorische principes bij het versterken van zwakke rekenkundige theorieën.

De auteur merkt op dat hoewel het zwakke duivenhokprincipe (WPHP) bekend staat als onvoldoende om sterke principes zoals MIN te bewijzen (via resultaten in [12]), dit artikel dat begrip uitbreidt tot het sterke duivenhokprincipe beperkt tot $\Delta^b_1$-formules. De betekenis ligt in het aantonen dat zelfs het sterke PHP, wanneer beperkt tot in polynomiale tijd berekenbare grafen, de kloof niet overbrugt naar de sterkte van $T^2_2$ met betrekking tot minimalisatie.

Het artikel sluit af met het formuleren van een open probleem: of dezelfde combinatorische methoden $T^1_2(\triangleleft) + PHP'(\Delta^b_1(\triangleleft))$ (een variant die multifuncties toestaat) kunnen scheiden van $MIN(\triangleleft)$. De auteur uit onzekerheid, waarbij hij de moeilijkheid benadrukt om ondergrenzen vast te stellen voor arrays waarbij rijelementen niet noodzakelijk incompatibel zijn.