Wat betekent ‘is gelijk aan’? Voor wiskundigen heeft deze eenvoudige vraag meer dan één antwoord. Dat levert problemen op wanneer we computers inzetten om bewijzen te controleren. Misschien moeten wiskundigen daarom terug naar de tekentafel om de grondslagen van hun vakgebied te herdefiniëren.
Als je ‘2 + 2 = 4’ ziet, wat betekent ‘=’ dan? Het blijkt een ingewikkelde vraag te zijn. Wiskundigen zijn het niet eens over de definitie van wanneer twee dingen gelijk zijn. Hoewel deze =-discussie al tientallen jaren woedt, heeft een recente ontwikkeling om wiskundige bewijzen te laten controleren door computerprogramma’s, formalisering genoemd, er nieuwe urgentie aan gegeven.
‘Wiskundigen bedoelen twee verschillende dingen met ‘is gelijk aan’. Ik vond dat prima’, zegt wiskundige Kevin Buzzard van het Imperial College in Londen. ‘Tot ik begon wiskunde te doen op een computer.’
‘Het ITER-uitstel is minder dramatisch dan het lijkt’
‘ITER tien jaar vertraagd’, kopten de media. Maar de momenten waar het bij deze kernfusiereactor écht om gaat worden veel minder uitgesteld.
Zodra hij computers aan bewijzen liet werken, realiseerde Buzzard zich dat wiskundigen een knoop moeten doorhakken over wat hij een ‘tot voor kort nuttige dubbelzinnigheid’ noemt. Dat zou ertoe kunnen leiden dat wiskundigen de grondslagen van hun vakgebied opnieuw moeten definiëren.
Twee definities
De eerste definitie van gelijkheid is bij veel mensen bekend. De meeste wiskundigen nemen aan dat ‘=’ betekent dat aan beide zijden van een vergelijking hetzelfde wiskundige object staat. Dat kan bewezen worden door een reeks logische transformaties uit te voeren op datgene wat aan de linkerzijde staat, waardoor de rechterzijde verschijnt. Hoewel het gelijkheidsteken, de ‘=’, pas in de 16e eeuw is opgeschreven, gaat dit concept van gelijkheid terug tot de oudheid.
Aan het eind van de 19e eeuw kwam de verzamelingenleer op, die de logische basis vormt van de meeste moderne wiskunde. De verzamelingenleer behandelt verzamelingen van wiskundige objecten en introduceert een andere definitie van gelijkheid: als twee sets dezelfde elementen bevatten, dan zijn ze gelijk. De verzamelingen {1, 2, 3} en {3, 2, 1} zijn bijvoorbeeld gelijk, omdat de volgorde van de elementen in een verzameling er niet toe doet.
Isomorfismen
Naarmate de verzamelingenleer zich ontwikkelde, besloten wiskundigen dat twee verzamelingen al aan elkaar gelijk zijn als er een voor de hand liggende manier is om ze met elkaar in verband te brengen. Dat geldt zelfs als ze niet precies dezelfde elementen bevatten, zegt Buzzard.
Neem de verzamelingen {1, 2, 3} en {a, b, c}. Het is duidelijk dat de elementen van elke set verschillend zijn, dus de sets zijn niet gelijk. Maar er zijn manieren om de twee verzamelingen aan elkaar te koppelen, door elke letter met een getal te identificeren. Wiskundigen noemen dit een isomorfisme.
In dit geval zijn er meerdere isomorfismen, omdat je kunt kiezen welk getal je aan elke letter toekent. Maar in veel gevallen is er maar één duidelijke keuze, het zogenaamde ‘canonieke isomorfisme’.
Omdat een canoniek isomorfisme van twee verzamelingen de enige mogelijke manier is om ze aan elkaar te koppelen, gaan veel wiskundigen er nu van uit dat dit betekent dat die verzamelingen gelijk zijn, ook al is het technisch gezien niet hetzelfde concept van gelijkheid als waar de meesten van ons aan gewend zijn. ‘Deze verzamelingen komen op een volledig natuurlijke manier met elkaar overeen en wiskundigen realiseerden zich dat het erg handig zou zijn als we deze ook gewoon ‘gelijk’ zouden noemen’, zegt Buzzard.
Beetje slordig
Twee definities voor gelijkheid geven geen problemen wanneer wiskundigen onderzoekartikelen schrijven of lezingen geven, omdat de betekenis van de ‘=’ dan altijd duidelijk volgt uit de context. Het levert wél problemen op voor computerprogramma’s die strikte, precieze instructies nodig hebben, zegt wiskundige Chris Birkbeck van de Universiteit van East Anglia in het Verenigd Koninkrijk. ‘We komen erachter dat we al die tijd een beetje slordig zijn geweest en dat we misschien een paar dingen moeten rechtzetten.’
Om dit probleem aan te pakken, heeft Buzzard onderzoek gedaan naar de manier waarop sommige wiskundigen canoniek isomorfisme op grote schaal gebruiken als gelijkheid en de problemen die dit kan veroorzaken met formele computerbewijssystemen. Hij publiceerde zijn vondsten in een artikel op de website arxiv.org.
Met name het werk van Alexander Grothendieck, een van de belangrijkste wiskundigen van de 20e eeuw, is momenteel extreem moeilijk te formaliseren. ‘Geen van de systemen die tot nu toe bestaan, bevatten de manier waarop wiskundigen zoals Grothendieck het gelijkheidssymbool gebruiken’, zegt Buzzard.
Hoe werkt je keuken?
De kern van het probleem zit in de manier waarop wiskundigen bewijzen samenstellen. Om iets te kunnen bewijzen, moet je eerst aannames doen, die axioma’s worden genoemd. Die worden zonder bewijs voor waar aangenomen.
In het begin van de 20e eeuw hebben wiskundigen een verzameling axioma’s binnen de verzamelingenleer vastgesteld, die een stevige basis vormen. Dit betekent dat ze axioma’s over het algemeen niet direct hoeven te gebruiken in hun dagelijkse werk, omdat ze ervan uit kunnen gaan dat het gewone hulpmiddelen zijn die correct werken, op dezelfde manier dat jij je geen zorgen maakt over hoe je keuken werkt voordat je aan een recept begint.
‘Als wiskundige weet je op de een of andere manier goed genoeg wat je doet, zodat je je er niet al te veel zorgen over maakt’, zegt Birkbeck. Maar die vlieger gaat niet op zodra computers erbij betrokken raken. Die voeren de wiskunde uit op een manier die vergelijkbaar is met het vanaf nul opbouwen van een keuken voor elke maaltijd. ‘Zodra je een computer hebt die alles wat je zegt controleert, kun je niet meer vaag zijn. Je moet echt heel precies zijn’, zegt Birkbeck.
Gelijkheid in gelijkheid
Om het probleem op te lossen, stellen sommige wiskundigen dat we de grondslagen van de wiskunde moeten herdefiniëren, zodat canonieke isomorfismen en gelijkheid één en hetzelfde zijn. Dan kunnen we computerprogramma’s daar omheen laten werken. ‘Isomorfisme is gelijkheid’, zegt computerwetenschapper Thorsten Altenkirch van de Universiteit van Nottingham in het Verenigd Koninkrijk. ‘Ik bedoel, wat zou het anders kunnen zijn? Als je twee isomorfe objecten niet kunt onderscheiden, wat zou het dan anders zijn? Hoe zou je deze relatie anders noemen?’
Er zijn al pogingen gedaan om dit te doen in het wiskundige vakgebied ‘homotopie-typetheorie’, waarin traditionele gelijkheid en canoniek isomorfisme identiek gedefinieerd zijn. In plaats van te proberen om bestaande computersoftware zo aan te passen dat het past bij het canoniek isomorfisme, zegt Altenkirch, zouden wiskundigen de typetheorie moeten overnemen, en alternatieve software moeten gebruiken die daar direct mee werkt.
Wiskundigen veranderen
Buzzard is geen fan van deze suggestie. Hij heeft al veel moeite gedaan om met de huidige software wiskundige bewijzen te formaliseren die nodig zijn om geavanceerder werk te controleren, zoals een bewijs van de laatste stelling van Fermat.
De axioma’s van de wiskunde moeten blijven zoals ze zijn, in plaats van de typetheorie over te nemen. In plaats daarvan moeten bestaande systemen worden aangepast, zegt hij. ‘Waarschijnlijk is de oplossing om wiskundigen te laten zoals ze zijn’, zegt Buzzard. ‘Het is erg moeilijk om wiskundigen te veranderen. Je moet de computersystemen beter maken.’
