Wiskundige inductie: hoe je oneindig veel gevallen in één keer bewijst
Stel je een lange rij dominostenen voor, duizenden stuks, zo opgesteld dat elke steen bij het omvallen de volgende raakt. Je hoeft niet elke steen apart om te duwen om zeker te weten dat ze allemaal zullen vallen. Er zijn maar twee dingen die je hoeft te controleren: dat de eerste steen omvalt, en dat elke steen die omvalt automatisch de volgende meesleurt. Kloppen die twee dingen, dan weet je met zekerheid dat de hele rij omvalt, ook al heb je nooit elke steen afzonderlijk getest.
Wiskundige inductie werkt volgens precies dezelfde redenering, maar dan voor uitspraken over getallen in plaats van dominostenen. Het is een bewijsmethode waarmee je kunt aantonen dat een bewering geldt voor alle natuurlijke getallen (1, 2, 3, 4, en zo oneindig door), zonder dat je die bewering voor elk getal apart hoeft na te rekenen. Dat klinkt als een klein technisch trucje, maar het is een van de fundamentele bouwstenen van de wiskunde. En zoals verderop blijkt, ook van de informatica: overal waar software of hardware bewezen correct moet werken, duikt dezelfde dominoredenering op.
Wat is het precies?
Een inductiebewijs bestaat uit twee stappen die je apart moet leveren.
De eerste stap heet de basisstap. Hierin toon je aan dat de bewering klopt voor het allereerste geval, meestal het getal 1 of 0. Dat is meestal simpel rekenwerk: je vult het getal in en controleert of de uitspraak waar is.
De tweede stap heet de inductiestap. Hier neem je aan dat de bewering al bewezen is voor een willekeurig getal k, de zogeheten inductiehypothese: de aanname die je tijdelijk als waar beschouwt om er iets nieuws mee te bewijzen. Vervolgens laat je zien dat, als de uitspraak klopt voor k, hij dan ook moet kloppen voor het eerstvolgende getal, k+1. Dat is precies de dominosteen die de volgende laat omvallen.
Kloppen beide stappen, dan is de bewering bewezen voor alle natuurlijke getallen tegelijk. Een bekend schoolvoorbeeld is de formule 1 + 2 + 3 + ... + n = n(n+1)/2. Voor n = 1 klopt dit meteen (1 = 1×2/2). In de inductiestap neem je aan dat de formule geldt voor n = k, en reken je uit dat het optellen van k+1 aan beide kanten precies de formule voor k+1 oplevert. Zo is de formule in één keer bewezen voor elk natuurlijk getal, hoe groot ook.
Er bestaan ook krachtigere varianten. Bij sterke inductie mag je in de inductiestap aannemen dat de bewering klopt voor alle getallen tot en met k, niet alleen voor k zelf. Bij structurele inductie, veel gebruikt in de informatica, bewijs je eigenschappen van opgebouwde structuren zoals bomen of lijsten door aan te tonen dat de eigenschap geldt voor de kleinste bouwstenen en behouden blijft wanneer de structuur groter wordt gemaakt.
Wat wil men ermee bereiken?
Het doel van wiskundige inductie is fundamenteel: het biedt een waterdichte manier om uitspraken te bewijzen die over een oneindige verzameling gevallen gaan. Zonder zo'n techniek zou je nooit met zekerheid kunnen zeggen dat een formule, eigenschap of algoritme voor élk getal werkt. Je zou hooguit kunnen zeggen dat het klopt voor alle gevallen die je tot nu toe hebt getest, wat geen garantie geeft voor de rest.
In de zuivere wiskunde is inductie onmisbaar bij het opbouwen van de natuurlijke getallen zelf en bij het bewijzen van eigenschappen van getallen, rijen en verzamelingen. Het vormt een van de axioma's, de grondregels die zonder verder bewijs worden aangenomen, in de formele opbouw van de rekenkunde.
In de informatica gaat het om iets heel praktisch: de correctheid van software. Programmeurs willen weten of een lus, een stuk code dat zich herhaalt, na elke stap dichter bij het juiste antwoord komt, en of een recursieve functie, een functie die zichzelf aanroept, voor elke invoergrootte het juiste resultaat geeft. Inductie is het wiskundige gereedschap waarmee zulke garanties hard gemaakt worden. Dat vormt weer de basis van formele verificatie: het wiskundig bewijzen dat software of hardware een bepaalde fout niet kan bevatten, in plaats van dat alleen te hopen op basis van testen.
Voorbeelden uit de praktijk
Wiskundige inductie klinkt abstract, maar duikt op in tastbare projecten en gebeurtenissen:
- Formalisering door Giuseppe Peano (1889): de Italiaanse wiskundige nam het inductieprincipe op als axioma in zijn beroemde Peano-axioma's, de eerste strikte wiskundige opbouw van de natuurlijke getallen. Dit legde de basis voor hoe inductie vandaag nog wordt onderwezen.
- De CompCert-compiler (ontwikkeld vanaf 2005 door Xavier Leroy en collega's bij het Franse onderzoeksinstituut INRIA): een compiler voor de programmeertaal C waarvan de correctheid volledig is bewezen met de bewijsassistent Coq, een programma dat wiskundige bewijzen stap voor stap controleert. Grote delen van dat bewijs steunen op structurele inductie over de opbouw van programma's.
- Het seL4-microkernel-project (rond 2009, onderzoeksinstituut NICTA, tegenwoordig onderdeel van Data61, in Australië): de eerste besturingssysteemkern waarvan wiskundig is bewezen dat de implementatie exact overeenkomt met de specificatie, met behulp van de bewijsassistent Isabelle/HOL. Ook hier is inductie een van de kernbewijstechnieken.
- Wiskundeonderwijs en -olympiades: inductie is wereldwijd standaardstof in universitaire cursussen discrete wiskunde en een terugkerend onderwerp bij wiskundeolympiades, waar deelnemers sommen, ongelijkheden en deelbaarheidseigenschappen ermee moeten bewijzen.
- Formele verificatie in de chipindustrie: na het beruchte Pentium-deelfoutincident van 1994, waarbij een fout in de rekeneenheid van Intels Pentium-processor tot verkeerde deelsommen leidde, is formele verificatie inclusief inductieve bewijstechnieken een vast onderdeel geworden van het ontwerpproces bij chipfabrikanten.
Hoe ver is de techniek?
Wiskundige inductie is geen opkomende technologie maar een eeuwenoud, volledig uitgekristalliseerd bewijsprincipe. Vroege sporen zijn te vinden bij de Perzische wiskundige Al-Karaji rond het jaar 1000, en latere uitwerkingen bij onder anderen Blaise Pascal in de zeventiende eeuw. De strikte, moderne formulering dateert van Peano in 1889.
Wat wél volop in ontwikkeling is, is de toepassing van inductie binnen geautomatiseerde bewijsassistenten zoals Coq (recent omgedoopt tot Rocq), Isabelle/HOL, Lean en Agda. Deze programma's helpen onderzoekers om inductiebewijzen op te bouwen en, belangrijker nog, door de computer te laten controleren op fouten. Grote formele-verificatieprojecten zoals het computerondersteunde bewijs van de vierkleurenstelling (Georges Gonthier, 2005) en het Flyspeck-project voor het Kepler-vermoeden over de dichtste bolstapeling (Thomas Hales, afgerond in 2014) hadden niet zonder deze combinatie van inductie en computerondersteuning gekund.
De belangrijkste obstakels liggen niet in het principe zelf, maar in de toepassing ervan. Het vinden van de juiste inductiehypothese blijft vaak mensenwerk: een te zwak geformuleerde aanname maakt de inductiestap onbewijsbaar, ook al is de oorspronkelijke bewering wel waar. Het automatisch laten vinden van geschikte inductiehypotheses door software is nog altijd een actief onderzoeksgebied, net als het opschalen van bewijsassistenten naar steeds grotere en complexere softwaresystemen, wat veel rekenkracht en mensuren blijft kosten.
Wie werken eraan?
Aan de wiskundige kant van inductie is geen bedrijf of instituut eigenaar: het is basiskennis die op vrijwel elke universiteit ter wereld wordt onderwezen en gebruikt. De ontwikkeling van geautomatiseerde bewijsgereedschappen die op inductie steunen, is wel geconcentreerd bij een beperkt aantal instituten.
Het Franse onderzoeksinstituut INRIA ontwikkelt en onderhoudt Coq/Rocq, een van de meest gebruikte bewijsassistenten. De Technische Universiteit München en de Universiteit van Cambridge onderhouden gezamenlijk Isabelle/HOL. Microsoft Research en Amazon Web Services financieren en gebruiken de bewijsassistent Lean voor interne formele-verificatieprojecten. In Australië heeft onderzoeksinstituut Data61, de opvolger van NICTA, de seL4-verificatie geleid en zet dat werk voort.
Ook chipfabrikanten zoals Intel en AMD hebben interne teams voor formele verificatie die inductieve technieken gebruiken om rekenkundige eenheden in processors te controleren, een praktijk die sinds de Pentium-deelfout van 1994 sterk is uitgebreid.