photo: John Stell, courtesy http://www.cs.kun.nl/fnds/
TYPES2002/martin-lof.html

Leids eredoctoraat voor filosoof Per Martin-Löf

Bouwwerk van betekenis

Leids Eredoctor Per Martin-Löf begon als vogelaar, maar werd beroemd door de wiskunde van een solide basis te voorzien. Intussen wist hij ook nog aan de KGB te ontsnappen.

Bruno van Wayenburg

Per Martin-Löf is een filosoof zoals je je een filosoof voorstelt: grote grijze baard en in het bezit van bruin ribfluwelen jasje. Voeg daarbij vriendelijk priemende ogen en een bedaarde, precieze manier van spreken, en je hebt bij uitstek iemand aan wie in Leiden een eredoctoraat wordt verleend voor verdiensten in de wijsbegeerte.
Dat laatste gebeurde dan ook, afgelopen maandag, ter gelegenheid van de 429de dies natalis. Leids hoogleraar wijsbegeerte prof.dr. Göran Sundholm fungeerde als Löfs erepromotor.
Toch heeft prof. dr. Martin-Löf (1942), in vakkringen geëerd en bewonderd om zijn ‘constructive type theory’, ook zijn onverwachte kanten. Zo vaak komt het niet voor dat het werk van een filosoof toepasbaar is in wiskunde, taalkunde en zelfs de vliegtuigbouw. Ook zullen er ook weinig andere filosofen zijn aan wie een nummer van een beroemd sovjet-zanger is gewijd.
Dat laatste is een lang verhaal, vertelt Martin-Löf in een suite van hotel De Doelen. In 1964 kreeg hij als student statistiek de kans om een jaar te studeren in Moskou. ‘Dat was toen de Russische wiskunde echt op haar hoogtepunt stond.’ Dat gold ook voor de koude oorlog, maar van hinderlijke volgende geheim agenten merkte de enige westerling in de studentenflat weinig. ‘Politiek kwam ook vrijwel nooit ter sprake. Het ging puur om wiskunde.’
‘Het was een beslissend jaar’, zegt de filosoof nu. Als Zweedse scholier was hij al geïnteresseerd geraakt in statistiek als vogelenthousiast. ‘We vingen en ringden vogels, maar ik vond het interessant om ook andere metingen te doen: vleugellengtes, de lengte van de staart.’ Al gauw besefte de vogelaar dat met de resulterende cijferbrij weinig zinnigs te doen was zonder kennis van de statistiek.

In Moskou maakte hij een tweede sprong in het diepe: hij begon zich bezig te houden net grondslagenwiskunde. ‘Mijn begeleider, de beroemde wiskundige Kolmogorov, had me een probleem opgegeven, maar dat had ik al snel opgelost.’ Intussen hadden medestudenten de Zweed verteld dat Kolmogorov ook ooit twee belangrijke artikelen had geschreven over de ‘grondslagen van de wiskunde.’ Daarmee wordt de onderbouwing van de wiskunde bedoeld. Hoewel dat voor buitenstaanders vaak pietepeuterig precies lijkt, vinden vaklui anders.
‘Je wilt eigenlijk een methode die heel nauwkeurig en mechanisch alle stappen in een wiskundige redenering beschrijft’, omschrijft Martin-Löf de heilige graal.
Een speurtocht dus naar een systeem waarin ieder wiskundig idee vertaald wordt in eenvoudigere begrippen, tot je uitkomt op een minimaal aantal elementaire ideeën, en een paar basisstellingen of axioma’s. ‘De allereenvoudigste concepten zijn dan meestal wiskundige verzamelingen en logica.’
Pogingen tot zo’n rigide onderbouwing begonnen al in de negentiende eeuw, maar het bleek allemaal niet zo eenvoudig.
Zo schoot de Britse filosoof Bertrand Russell een gat in één van de eerste systemen door de Duitser Gottlob Frege. Russell definieerde een paradoxale ‘verzameling van alle verzamelingen die geen deel uitmaken van zichzelf.’ Als die verzameling leeg is, hoort hij in die verzameling. Maar in dat laatste geval hoort hij er juist weer niet in. Deze paradox was een bom onder Frege’s systeem.
Rond diezelfde tijd, in het begin van de twintigste eeuw, bespeurde de Nederlandse wiskundige Luitzen Brouwer nog meer problemen. Brouwer vond dat je in de wiskunde eigenlijk geen gebruik mocht maken van de aanname dat iedere uitspraak óf waar, óf onwaar is.
Wiskundigen doen dat standaard in zogenaamde ‘bewijzen uit het ongerijmde.’ Daarbij begin je met de aanname dat de te bewijzen stelling niet waar is. Vervolgens laat je zien dat die aanname tot een logische tegenspraak leidt. Dus, is de conclusie, moet de stelling wel waar zijn. Brouwer vond dat te gemakkelijk, en maakte school met dit wiskundig zindelijke ‘intuïtionisme.’
Martin-Löf stortte zich op een combinatie: een formele onderbouwing van Brouwers zogeheten ‘constructieve’ wiskunde. ‘Aan de verzamelingenleer moest nog heel wat gebeuren’, herinnert hij zich. Na een eerste publicatie van zijn ‘constructieve typetheorie’ overkwam hem bovendien hetzelfde als Frege. Een collega vond een gat dat gerepareerd moest worden. ‘Heel jammer’, vindt de logicus dat nog altijd.
Hij besefte dat je wel kon werken aan een logische machinerie, maar dat je ook ideeën moet hebben over de betekenis en de functie van de onderdelen, om meer bedrijfsongevallen te voorkomen. ‘Als je het eerste vergelijkt met een machine, dan is het tweede een soort handleiding van alle onderdelen, met beschrijvingen waar ze voor zijn, en wat ze doen.’
Dus werkte de filosoof tegelijkertijd aan een bijpassende ‘betekenistheorie’, een bezigheid die hem in het vaarwater van pure filosofen bracht. ‘Betekenis’ is immers een oud filosofisch probleem: een woord of symbool, heeft een relatie met iets anders, het ‘betekende’. Maar hoe die relatie precies in elkaar steekt, daar vallen nog wel wat haren over te kloven.

Martin-Löf’s handleiding bleek een ideaal vehikel voor filosofische verkenningen van het begrip ‘betekenis.’ Er konden zelfs praktische betekenisproblemen mee aangepakt kunnen worden, zoals computervertaling.
‘Finse onderzoekers werken aan een vertalingssysteem op basis van de theorie’, vertelt Martin-Löf, ‘er zijn zelfs besprekingen over het vertalen van mechanische procedurebeschrijvingen voor vliegtuigbouwers.’ Dat is saai maar secuur vertaalwerk, dat cruciaal is voor de veiligheid van reparaties en onderhoud.
Computerwetenschappers weten Martin-Löfs werken ook te vinden, en wiskundigen werken op basis daarvan aan software die automatisch wiskundige bewijzen kan controleren.
‘Maar onder taal- en andere filosofen zou de theorie nog wel wat bekender kunnen zijn’, vindt Martin-Löf, die zich aan het eind van zijn loopbaan op dit zendingswerk heeft gestort. Vandaar dat deze erkenning, uit het land van Brouwer nog wel, meer dan welkom is. Martin-Löf: ‘Het systeem zelf is wel min of meer af, vermoed ik. Ik zal wel geen radicale veranderingen meer verzinnen. Ik ben al ouder dan zestig.’
Dat is dezelfde leeftijd die Kolmogorov had toen hij zijn pupil op het pad zette waarvoor hij zelf geen tijd had gehad. Later bleek ook een ander, toen ingeslagen pad onverwacht nog resultaten op te leveren.
‘Destijds had hij me uitgenodigd op een reis naar de Kaukasus, maar de toestemming van de autoriteiten kwam maar niet rond. Toen zijn wel maar zonder papieren gegaan, overigens zonder problemen.’ Begin jaren negentig ontdekte Martin-Löf dat hij toen waarschijnlijk ontsnapt was aan de toch ook weer niet zó passieve sovjet-autoriteiten.
‘Er was toen een concert van de (in de Sovjet-unie, BvW) wereldberoemde zanger Boelat Okoedzjava in Stockholm. Ik ging erheen om oude herinneringen op te halen. Bij één van de nummers zei hij: “Dit lied gaat over een Zweed.”’
De zanger vertelde hoe hij eens op een treinreis naar de Kaukasus plotseling merkte dat de conducteur wel erg zenuwachtig was, en de coupé akelig leeg. Na verloop van tijd kwamen er twee agenten de coupé binnen. Ze waren op zoek naar een Zweed die zonder papieren reisde.
Martin-Löf: ‘Na het concert ben ik naar de zanger toegegaan, en heb gevraagd: was dat misschien in maart 1965? Dat bleek zo te zijn. Buitengewoon toevallig, inderdaad.’