Bewijzen: romantisch of cool?

Henk Barendregt & Freek Wiedijk

7 maart 2006

Samenvatting

Computers kunnen ons helpen wiskunde te doen door voor ons te rekenen, met getallen of symbolisch. Systemen hiervoor zijn goed ontwikkeld. Er worden nu ook computersystemen ontwikkeld, de zogenaamde wiskundige assistenten, die ons zelfs kunnen helpen met het verifiëren en verder ontwikkelen van het vak. Het menselijke vernuft zal hierdoor niet overbodig worden.

1. De ‘wis’ van wiskunde

Eigenwijs? Dat wordt er wel over je beweerd als je van wiskunde houdt. Het onderwerp houdt zich bezig met die dingen waarvan je zeker kunt zijn. In andere talen heet het vak mathematics, mathématiques, matématica, …. Het Nederlands heeft een heel ander woord, hoewel ‘mathesis’ vroeger ook wel gebruikt werd. De stam ‘wis’ is verwant aan ‘zeker’, aan ‘weten’. En ja, het kan eigenwijs overkomen als je je bezighoudt met deze zaken. Maar je weet ook wel dat alleen sommige dingen zeker zijn: het weer kunnen we niet op de lange termijn voorspellen. Maar dat weten we dan ook weer zeker. Trouwens, wat de zekerheid betreft die de wiskunde je geeft, het gaat niet om gelijk te krijgen, maar om gelijk te hebben!

Waar komt die zekerheid nu vandaan? Die is het gevolg van het bewijzen. Een uitspraak wordt onderzocht op al zijn mogelijke aspecten. En als dat er oneindig veel zouden zijn, dan worden er methoden ingevoerd om binnen eindige tijd al die oneindig vele gevallen te kunnen behandelen: symbolisch redeneren (‘met x en y’) en inductie (een uitspraak is waar voor alle natuurlijke getallen als die waar is voor 0 en als de waarheid voor x die voor x + 1 tot gevolg heeft). Dat geeft de precisie, kracht en zekerheid van de wiskunde die haar zo mooi (en voor sommigen: onuitstaanbaar) maakt.

Waarom geven bewijzen zekerheid? Dat komt omdat je alleen uitgaat van de definities, van wat er gegeven^{1} is, en dan op grond van een sluitende redenatie een conclusie trekt. Blijft de vraag wat een sluitende redenering is. Tijdens een werkcollege vragen studenten vaak “Mag ik deze stap maken?” Het antwoord van de docent is dan “Als je in de eerste plaats jezelf en daarna mij ervan kunt overtuigen dat deze juist is.” Het uiteindelijke oordeel van de logische en daarmee wiskundige correctheid hangt af van een mentaal oordeel. Maar het bijbehorende oordeelsvermogen moet wel getraind worden!

1Er zijn ook axioma’s, maar die vormen een impliciete definitie van het onderwerp waarmee je je bezig houdt. Zo is er voor de optelling in de natuurlijke getallen het axioma 0 + x = x.

Dit is in feite een afspraak: zo willen we optellen.

Nu kan het voorkomen dat een bewijs zeer lang is. Onze geest kan dan moe worden bij de verificatie ervan en zo kunnen er foutjes binnen sluipen. Stellingen met lange—en ook extreem lange—bewijzen komen voor. Je kunt zelfs aantonen dat er altijd nieuwe stellingen zullen zijn met alleen extreem lange bewijzen (en een relatief korte formulering). Dit treedt onder andere, maar niet uitsluitend, op als lange berekeningen onderdeel vormen van het bewijs, zoals bij de vier kleurenstelling. Om deze redenen heeft de Nederlandse wiskundige Dick de Bruijn (geboren 1918) een taal Automath ontwikkeld waarin een bewijs zodanig in stapjes uit gesplitst kan worden dat een computer met een eenvoudig programma het kan verifiëren op fouten en foutjes, zie Nederpelt, Geuvers and de Vrijer [1994]. Wij hoeven slechts éénmaal na te gaan of het computerprogramma correct is (het uiteindelijke menselijke oordeel blijft) en dan kunnen we op deze manier de hoogst mogelijke graad van zekerheid verkrijgen. Wel moeten de bewijzen dan geformaliseerd worden, dat wil zeggen van alle mogelijke details voorzien worden klaar voor de verificatie door de computer. Op interactieve wijze, door samenwerking tussen wiskundige en computer komen volledig geformaliseerde bewijzen tot stand en worden ze nagekeken. Op deze wijze resulteert wat we noemen Computer Wiskunde. We geven twee voorbeelden.

2. Het bestaan van positieve irrationale getallen met rationale macht

We geven nu een stelling en een bewijs daarvan. De uitspraak is op zichzelf niet erg interessant, maar er moet een beetje geredeneerd en gerekend worden en dat illustreert de methode van bewijsverificatie. Een reëel getal r heet rationaal als het een breuk is, dus als r = \frac{p}{q} voor zekere gehele getallen p, q. Anders heet het irrationaal.

Een romantisch bewijs

2.1. Stelling. Er bestaan positieve irrationale getallen x en y zodat hun macht x^{y} rationaal is. In symbolen ∃x, y ∈ (ℝ_{>0}\ℚ).x^{y} ∈ ℚ.

Bewijs. We weten dat \sqrt{2} ∈ ℝ_{>0}\ℚ.

Geval 1. \sqrt{2}^{\sqrt{2}} ∈ ℚ. Dan zijn we klaar: neem x = y = \sqrt{2}.

Geval 2. \sqrt{2}^{\sqrt{2}} ∉ ℚ. Neem dan x = \sqrt{2}^{\sqrt{2}} en y = \sqrt{2}. Dan zijn

x, y ∈ (ℝ_{>0}\ℚ) en x^{y} = (\sqrt{2}^{\sqrt{2}})^{\sqrt{2}} = \sqrt{2}^{\sqrt{2}·\sqrt{2}} = \sqrt{2}^{2} = 2 ∈ ℚ.

Er valt hier iets op. Hoewel we niet weten of \sqrt{2}^{\sqrt{2}} rationaal is of niet konden we toch inzien dat de stelling juist is. Als iemand ons dan vraagt ‘Geef die getallen x en y dan eens’, dan kunnen we dat niet voor x. Dit komt omdat het bewijs niet intuïtionistisch geldig is. Met behulp van intuïtionistische logica kun je alleen existentie uitspraken bewijzen als je ook daadwerkelijk voorbeelden kunt geven. Met meer moeite kan er toch een intuïtionistisch bewijs gegeven

worden. Er is de stelling van Gelfond-Schneider, die impliceert dat \sqrt{2}^{\sqrt{2}} ∉ ℚ. Dat kan intuïtionistisch bewezen worden en zo hebben we dan wel een konkreet voorbeeld voor bovenstaande stelling: x = \sqrt{2}^{\sqrt{2}}, y = \sqrt{2}.

Het bewijs van de stelling—we beperken ons tot de klassieke (niet intuïtionistische) versie—is geheel duidelijk. We noemen het een ‘romantisch’ bewijs: begrijpelijk voor de menselijke geest.

Bewijzen via de computer: eerste poging

We kunnen proberen het bewijs van de stelling 2.1 met behulp van een computer te leveren.

Numerieke berekeningen (GP/PARI calculator)

Een goed numeriek programma zal niet blijken te helpen.

? sqrt(2)
%1 = 1.414213562373095048801688724
? %1^%1
%2 = 1.632526919438152844773495381
? %2^%1
%3 = 1.999999999999999999999999999
Ook al zou het antwoord %3 = 2.000000000000000000000000000 zijn, dan

kunnen we nog niet concluderen dat dit getal rationaal is. En verder is natuurlijk helemaal niet duidelijk dat er bij %1 en %2 irrationale getallen staan.

Computeralgebra (Mathematica)

Met behulp van ‘symbolisch rekenen’ kunnen we iets meer. Een systeem dat dit

kan rekent \sqrt{2}^{\sqrt{2}} exact uit.

In[1]:= (Sqrt[2]^Sqrt[2])^Sqrt[2]
Out[1]= 2

We zouden het systeem kunnen leren dat \frac{p}{q} en dus ook 2 rationaal is. Maar weer kan er zelfs niet uitgedrukt worden dat bijvoorbeeld \sqrt{2} irrationaal is.

Bewijzen via de computer: cool

Alleen al het formuleren op een computer van onze stelling mislukte boven. Een numeriek programma kan wel 3.7 − 1.8 = 1.9 uitrekenen, maar niet r − r als we niet vertellen wat r is en daar dan 0 uit laten komen. In een programma voor symbolisch rekenen kan dit laatste wel. Maar in zulke systemen kunnen we weer geen eigenschappen zoals rationaliteit of de ontkenning daarvan weergeven.

Interactieve bewijsverificatie (Mizar)

Het systeem Mizar van Trybulec (Białystok, Polen, in ontwikkeling sinds 1974), dat geïnspireerd is door het werk van de Bruijn, kan wel alle mogelijke wiskundige uitspraken doen. Dat komt omdat de logica (en eveneens de verzamelingenleer) is ingebouwd in dit systeem. Bewijzen zullen door de gebruiker moeten worden ingevoerd, waarna ze volledig geverifieerd worden.

---------------------------------------------------------------
theorem
 ex x, y st x is irrational & y is irrational & x^y is rational
proof
 set w = sqrt 2;
 w > 0 by SQUARE_1:84;
 then A1: (w^w)^w = w^(w*w) by POWER:38
  .= w^(w^2) by SQUARE_1:def 3
  .= w^(2) by SQUARE_1:def 4
  .= w^2 by POWER:53
  .= 2 by SQUARE_1:def 4;
 per cases;
 suppose A2: w^w is rational;
  take w, w;
  thus thesis by A2,IRRAT_1:1,INT_2:44;
 end;
 suppose A3: w^w is irrational;
  take w^w, w;
  thus thesis by A1,A3,IRRAT_1:1,INT_2:44;
 end;
end;
---------------------------------------------------------------

Gebruik wordt gemaakt van reeds eerder geverifieerde stellingen.

 POWER:38         a > 0 implies a to power b to power c = a to power (b * c);
 POWER:53         a to power 2 = a^2;
 SQUARE 1:84      1 < sqrt 2;
 SQUARE 1:def 3   x^2 = x * x;
 SQUARE 1:def 4   0 <= a implies 0 <= sqrt a & (sqrt a)^2 = a;
 INT 2:44         2 is prime;
 IRRAT 1:1        p is prime implies sqrt p is irrational;

De bibliotheek van het systeem Mizar is behoorlijk groot. Zo’n 50.000 stellingen zijn er geformaliseerd en goed bevonden. Voorbeelden van stellingen die in de Mizar bibliotheek voorkomen zijn de hoofdstelling van de algebra (ieder polynoom over ℂ heeft een wortel in ℂ); de hoofdstelling van de analyse (differentiëren van de integraal van een continue functie f levert f zelf op); de Brouwer dekpunt stelling (een continue functie van een bol naar zichzelf heeft altijd een punt dat op zijn plaats blijft).

Automatische deductie (Otter)

In tegenstelling tot Mizar zoekt het systeem Otter, ontwikkeld door McCune (Argonne, Illinois, in ontwikkeling sinds 1988), zelf naar bewijzen. Je moet dan wel een handje helpen en bijvoorbeeld voorzeggen dat \sqrt{2} irrationaal is. Omdat onze stelling vrij eenvoudig is, kan het bewijs verder door Otter zelf gevonden worden. In het algemeen duurt het te lang om een computer naar bewijzen te laten zoeken. Voor bovenstaande bewering—en met menselijke hulp—kan dat dus wel. Het systeem Otter werkt met de zogenaamde eerste orde predicatenlogica. Naast termen zoals x, y, x · y, x^{y}, … en gelijkheden zoals (x^{y})^{z} = x^{y·z} die ook al gebruikt worden in systemen voor computeralgebra, heb je nu ook een weergave voor de zogenaamde kwantoren “er is een x” en “voor alle x”. De manier waarop naar een bewijs gezocht wordt is de zogenaamde resolutie methode. Hierbij wordt geprobeerd met de resolutie methode (een bepaald soort bewijs uit het ongerijmde) de stelling aan te tonen. Het gegenereerde bewijs is meestal niet begrijpelijk, zie het volgende voorbeeld.

----------------------- Input --------------------------------------
set(auto).
op(300, xfy, ^).
formula_list(usable).
all x (x*x = x^2).
all x (sqrt(x)^2 = x).
all x y z ((x^y)^z = x^(y*z)).
-rational(sqrt(2)).
rational(2).
end_of_list.
formula_list(sos).
-(exists x y (-rational(x) & -rational(y) & rational(x^y))).
end_of_list.
------------------------- PROOF -----------------------------------
1 [] -rational(sqrt(2)).

2 [] rational(x)|rational(y)| -rational(x^y).
3 [factor,2.1.2] rational(x)| -rational(x^x).
4 [] x*x=x^2.
6,5 [copy,4,flip.1] x^2=x*x.
7 [] sqrt(x)^2=x.
8 [copy,7,demod,6] sqrt(x)*sqrt(x)=x.
10 [] (x^y)^z=x^(y*z).
12 [] rational(2).
22 [para_from,10.1.1,2.3.1]
         rational(x^y)|rational(z)| -rational(x^(y*z)).
58 [para_into,22.3.1.2,8.1.1]
         rational(x^sqrt(y))|rational(sqrt(y))| -rational(x^y).
67 [para_into,58.3.1,5.1.1,unit_del,1]
         rational(x^sqrt(2))| -rational(x*x).
84 [para_into,67.2.1,8.1.1] rational(sqrt(x)^sqrt(2))| -rational(x).
91 [hyper,84,12] rational(sqrt(2)^sqrt(2)).
96 [hyper,91,3] rational(sqrt(2)).
97 [binary,96.1,1.1] $F.
----------------------- end of proof -------------------------------

Op een geheel andere manier—op grond van een door Collins Collins [1976] en anderen verbeterd algoritme van Tarski Tarksi [1951] dat gebruikt maakt van logische manipulaties die met name gelden voor bepaalde structuren—kunnen bewijzen voor uitspraken uit de Euclidische meetkunde automatisch gegenereerd worden, tenzij het systeem aangeeft dat de uitspraak onjuist is. De efficientie van het algoritme is matig en voor een overlappende verzameling van problemen is er het snellere algoritme van Buchberger, see Buchberger and Winkler [1998] en de methode van Wu, see Chou [1988].

3. Hoe win je de hand van Portia?

Vrij naar het toneelstuk “de Koopman van Venetië” van Shakespeare heeft Smullyan [1978] de volgende puzzel verzonnen.

De huwbare Portia heeft een gouden en een zilveren kistje. Zij kiest haar toekomstige echtgenoot uit niet op grond van zijn kracht, maar op grond van zijn intelligentie. In een van de kistjes plaatst ze een portret van haarzelf. Ze sluit de kistjes. Leesbaar op het gouden kistje staat de inscriptie “Het portret zit niet in dit kistje”. Op het zilveren kistje staat “Precies één van deze twee uitspraken is waar”. Portia legde uit aan een man die naar hand dong, dat de uitspraken waar of onwaar kunnen zijn, maar dat als hij het kistje kan uitkiezen waar haar portret in zit, zij met hem zal trouwen.

Het probleem is nu om gebruik te maken van de inscripties, zonder dat je weet of ze al dan niet waar zijn. De romantische oplossing is als volgt. Stel de uitspraak op het zilveren kistje is waar. Dan is die op het gouden kistje onwaar en dus zit het portret in dat kistje. Stel de uitspraak op het zilveren kistje is onwaar, dan moet die op het gouden kistje ook onwaar zijn. Wederom zit het portret in het gouden kistje. De slimme man wijst dus het gouden kistje aan (als hij haar tenmiste wil trouwen).

Interactieve bewijsverificatie (Mizar)

theorem
  the_gold_inscription = is_not portrait_in_gold_casket &
  the_silver_inscription =
    exactly_one_holds_of (the_gold_inscription,the_silver_inscription)
implies
  portrait_in_gold_casket is_true
proof
assume that
   A1: the_gold_inscription = is_not portrait_in_gold_casket and
   A2: the_silver_inscription =
     exactly_one_holds_of (the_gold_inscription,the_silver_inscription);
::[in order to prove]
   the_gold_inscription is_false
proof
per cases;
suppose
   A3: the_silver_inscription is_true;
then
   exactly_one_holds_of (the_gold_inscription,the_silver_inscription) is_true
by A2; then
   the_gold_inscription is_true & the_silver_inscription is_false or
   the_gold_inscription is_false & the_silver_inscription is_true
by exactly_one; hence
   the_gold_inscription is_false
by A3; end;
suppose
   A4: the_silver_inscription is_false;
then
   exactly_one_holds_of (the_gold_inscription,the_silver_inscription) is_false
by A2; then
   the_gold_inscription is_true & the_silver_inscription is_true or
   the_gold_inscription is_false & the_silver_inscription is_false
by exactly_one; hence
   the_gold_inscription is_false by A4;
end;
end;
::[in both cases we have the_gold_inscription is_false]
then
   (is_not portrait_in_gold_casket) is_false
by A1; hence
   portrait_in_gold_casket is_true
by is_not_iff_not;
end;

Het probleem heeft een logische kronkel. Een van de uitspraken is verwijst naar zichzelf. In het algemeen leidt dat tot paradoxen (“Deze uitspraak is onwaar”), maar in dit geval is dat niet zo. In de technologie van Computer geformaliseerd bewijzen wordt vaak op gebruik gemaakt van een inzichtelijk betrouwbare vorm van deze zogenaamde reflectie, verwant aan dit voorbeeld, waarbij wiskundige uitspraken onderwerp worden van andere uitspraken. Een voorbeeld van reflectie is het dualiteitsprincipe uit de projectieve meetkunde: “Een stelling blijft geldig wanneer de begrippen punt en lijn systematisch verwisseld worden.” Dit is een stelling over stellingen, verkregen uit reflectie over de axioma’s van de projectieve meetkunde.

4. State of the art

We noemen een paar systemen die momenteel gebruikt worden. Mizar (Pools), Coq (Frans), HOL (Engels), Isabelle (Engels/Duits) en PVS (Amerikaans). Zie respectievelijk de volgende web-sites.

     www.mizar.org
     pauillac.inria.fr/coq/
     www.cl.cam.ac.uk/users/jrh/hol-light/
     www.cl.cam.ac.uk/Research/HVG/Isabelle/
     pvs.csl.sri.com

Andere relevante web-site voor Computer Wiskunde (onder meer over Otter en Automath) zijn de volgende.

     www-unix.mcs.anl.gov/AR/otter/
     automath.webhop.net
     www.cs.ru.nl/^{∼}freek/aut/
     www.cs.ru.nl/^{∼}freek/digimath/
     www.cs.ru.nl/^{∼}freek/qed/qed.html

Een greep uit de bibliotheek van geheel geformaliseerde stellingen. De vierkleuren stelling (iedere landkaart in het vlak of de bol kan met vier kleuren zodanig gekleurd worden dat landen die elkaar aanraken met meer dan een punt verschillend gekleurd zijn); Bertrand’s postulate (tussen n en 2n zit altijd een priemgetal); de Jordan-curve stelling (een gesloten kromme in het vlak die zichzelf niet snijdt verdeelt het vlak in twee samenhangende gedeelten); de priemgetallen stelling (het aantal priemgetallen onder n is in de orde van \frac{n}{log n}); de onmogelijkheid met een passer en lineaal een hoek in drieën te verdelen of een kubus te verdubbelen. Toegegeven, dit is nog geen grensverleggende wiskunde, maar het potentieel om daar te komen is aanwezig. Voor een verdergaande inleiding in het vak, zie Barendregt and Wiedijk [2005] en Barendregt [2005].

Ondanks deze initiële successen worden er ook wel bezwaren tegen Computer Wiskunde ingebracht. Met name dat een bewijs gevrifieerd door een computer geverifieerd meestal niet begrijpelijk is. Dat kan waar zijn, maar het bewijs van stellingen met heel lange bewijzen zijn dat ook niet. De overgang van een overzichtelijke bewijs naar een bewijs dat niet geheel in het bewustzijn past en door een computer geverifieerd moet worden, dus van een romantisch naar een cool bewijs, kun je vergelijken met de overgang in de biologie van aandacht voor bloemen en vlinders naar dat voor genen. De romantische biologie blijft boeien, maar die van de genen heeft daar direct betrekking op, meer dan de romantici zouden willen. Een dergelijke verschuiving zal naar onze mening ook binnen de wiskunde plaats vinden. En net zoals bij biologie zal menselijk vernuft en vakintuïtie hard nodig blijven.

Iedere wiskundige kent het gevoel van tevredenheid wanneer hij of zij een stelling bewezen heeft. In de computer wiskunde blijft dat het geval. De emotie wordt nog sterker, want het is duidelijk dat alle details daadwerkelijk ingevuld zijn. Bij romantische bewijzen heeft men de tevredenheid omdat men ervan overtuigd is dat de details ingevuld kunnen worden. Een niet-wiskundige kan de ervaring van het maken of volgen van een (gewoon romantisch) bewijs niet goed navoelen. Daarvoor moet men door de ervaring van het bewijzen heen gegaan zijn. Een vergelijkbaar effect treedt op bij het maken van een geformaliseerd bewijs: dat kan alleen naar emotionele waarde geschat worden door het gedaan te hebben. De intrinsieke waarde van de computer wiskunde ligt in de volledige duidelijkheid, correctheid en mechanische manipuleerbaarheid van de resultaten. Bij computeralgebra systemen is dit niveau nog ver te zoeken.

De verwachting is dat over zeg 10 à 50 jaar—een korte periode vanuit historisch oogpunt bezien—Computer Wiskunde gemeengoed zal zijn geworden. Menselijke intuïtie zal samenwerken met de precizie van een computer. In principe is de huidige stand van de grondslagen van de wiskunde voldoende om dit nu al te doen. De uitdaging is echter om de bestaande systemen meer gebruikers-vriendelijk voor wiskundigen te maken, door voldoende geverifieerde bibliotheken en hulpmiddelen te ontwikkelen. Het uiteindelijke doel is om mensen te helpen met het bestuderen, ontwikkelen, communiceren^{2}, onderwijzen, verifiëren^{3} en toepassen van de wiskunde. ———————————————————

Over de auteurs. Henk Barendregt studeerde mathematische logica bij Dirk van Dalen in Utrecht en promoveerde aldaar op een onderwerp in de lambda calculus. Freek Wiedijk studeerde wiskunde en theoretische fysica aan de Universiteit van Amsterdam en promoveerde aldaar op een onderwerp in de formele methoden, een deelgebied van de informatica.

Referenties

Barendregt, Henk [2005]. Foundations of Mathematics from the Perspective of Computer Verification, Mathematics, Computer Science, Logic - A Never Ending Story, Springer Verlag. To appear. See also ⟨www.cs.ru.nl/^{∼}henk/

    papers.html⟩.

Barendregt, Henk and Arjeh M. Cohen [2001]. Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants, J. Symbolic Comput. 32(1-2), pp. 3–22. Computer algebra and mechanized reasoning (St. Andrews, 2000).

2Computer wiskunde geeft vele mogelijkheden voor de electronische communicatie van betrouwbare resultaten en het voorkomen van ‘corruptie’ van het vak. Deze corruptie is niet in ethische maar technische zin bedoeld: het voortbestaan van en vertrouwen op foutieve stellingen. Dat moet worden tegen gegaan. Zie Barendregt and Cohen [2001].

3Referees die ingezonden artikelen beoordelen zullen nog steeds nodig zijn; niet voor de correctheid, maar voor het belang van het werk.

Barendregt, Henk and Freek Wiedijk [2005]. The challenge of computer mathematics, Phil. Trans. R. Soc. A. To apear.

Buchberger, B. and F. Winkler [1998]. Gröbner Bases and Applications, Cambridge University Press.

Chou, Shang-Ching [1988]. Mechanical geometry theorem proving, Mathematics and its Applications 41, D. Reidel Publishing Co., Dordrecht. With a foreword by Larry Wos.

Collins, G.E. [1976]. Quantifier elimination for real closed fields by cylindrical algebraic decomposition, in: H. Brakhage (ed.), Proc. 2nd GI Conference on Automata Theory and Formal Languages, LNCS 33, Springer-Verlag, pp. 134–183.

Nederpelt, R.P., J.H. Geuvers and R.C. de Vrijer [1994]. Selected Papers on Automath, Studies in Logic and the Foundations of Mathematics 133, Elsevier Science, Amsterdam.

Smullyan, Raymond [1978]. What is the name of this book?: The riddle of Dracula and other logical puzzles, Prentice-Hall.

Tarksi, A. [1951]. A decision method for elementary algebra and geometry, Technical Report R-109, Rand Corporation, Santa Monica, CA.