QED

Normaal beginnen wiskundigen van een bestaande verzameling axioma’s en bewijzen daarin nieuwe stellingen, maar er bestaat ook een onderzoeksprogramma dat de omgekeerde weg neemt: begin van bestaande stellingen en kijk welke axioma’s je minimaal nodig hebt om de stelling te bewijzen. Dit programma heet reverse mathematics. De wiskundige Harvey Friedman richtte de tak op in zijn artikel “Some systems of second order arithmetic and their use” (1975) en naast hem is ook Stephen Simpson een bekende voorman van reverse mathematics.

Het basisprincipe van reverse mathematics is eenvoudig: we beginnen in een basistheorie, een heel zwak axiomatisch systeem waarin we de meeste interessante stellingen niet kunnen bewijzen. De basistheorie moet echter wel krachtig genoeg zijn om de definities die in de stellingen voorkomen te beschrijven. Om de stelling “Elke begrensde rij van reële getallen heeft een supremum” te analyseren, moeten we in het basissysteem bijvoorbeeld kunnen spreken over reële getallen en over rijen.

Het doel in reverse mathematics is om een axiomatisch systeem S te bepalen dat sterker is dan het basissysteem en tegelijk noodzakelijk om de stelling te bewijzen. Dan weten we dat geen zwakker systeem dan S de stelling kan bewijzen. Zo’n systeem S is te vinden door te bewijzen dat S de stelling én dat de stelling S impliceert. We kunnen dus zeggen dat de stelling equivalent is met de axiomatische theorie S.

Dit onderzoeksprogramma heeft al een groot aantal resultaten behaald waarmee heel wat belangrijke stellingen geclassificeerd zijn als equivalent met bepaalde axiomatische systemen. Eigenlijk is dit een verderzetting van Hilberts programma. Terwijl Gödels onvolledigheidsstellingen het programma van Hilbert om alle klassieke wiskunde te reduceren tot finitistische wiskunde hebben stopgezet, proberen Friedman en Simpson en co nog zoveel mogelijk te redden: hoeveel van de klassieke wiskunde kunnen we reduceren tot finitistische wiskunde? Vrij veel, zo blijkt. Ook verrassend is dat een groot aantal stellingen over het algemeen in een klein aantal equivalentieklassen van axiomatische systemen kunnen geclassificeerd worden (met de “Big Five” RCA₀, WKL₀, ACA₀, ATR₀ en Pi₁¹ - CA₀). Dit onderzoek heeft heel wat interessante vragen in de grondslagen van de wiskunde opgelost, maar kan het dat ook in de filosofie van de wiskunde?