\let\polishl=\l \documentclass{article} \usepackage{amssymb,url,alltt,bk0,bk1} \raggedbottom \usepackage[dutch]{babel} \usepackage{graphicx,alltt} \def\toolong{$\hspace{-10em}$} \newcommand\real{{\mathbb R}} \newcommand\rat{{\mathbb Q}} \newcommand\complex{{\mathbb C}} \newtheorem{stelling}[definition]{Stelling} \usepackage[square]{harvard} \citationmode{full} \begin{document} \bibliographystyle{eb} \title{Bewijzen: romantisch of \emph{cool}?} \author{Henk Barendregt \& Freek Wiedijk} \weg{Institute for Computing and Information Sciences \\ Radboud University Nijmegen \\ Toernooiveld 1, 6525 ED Nijmegen, The Netherlands} \maketitle \begin{abstract} \noi 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\"eren en verder ontwikkelen van het vak. Het menselijke vernuft zal hierdoor niet overbodig worden. \end{abstract} \section{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 \emph{mathematics, math\'ematiques, mat\'ematica, $\ldots$ }. 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\footnote{Er 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.} 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! 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\"eren op fouten en foutjes, zie \ncite{automath}. Wij hoeven slechts \'e\'enmaal 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 \emph{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 \emph{Computer Wiskunde}. We geven twee voorbeelden.\\ \includegraphics[height=5cm,width=10cm]{plaatje.eps} \section{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\"eel 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. \subsection*{Een romantisch bewijs} \begin{stelling}\label{2.1} Er bestaan positieve irrationale getallen $x$ en $y$ zodat hun macht $x^y$ rationaal is. In symbolen $\exists x,y\in(\real_{>0}\backslash\rat).x^y\in\rat$. \end{stelling} %\begin{proof} {\sc Bewijs.} We weten dat $\sqrt{2}\in\real_{>0}\backslash\rat$. Geval 1. $\sqrt{2}^{\sqrt{2}}\in\rat$. Dan zijn we klaar: neem $x=y=\sqrt{2}$. Geval 2. $\sqrt{2}^{\sqrt{2}}\notin\rat$. Neem dan $x=\sqrt{2}^{\sqrt{2}}$ en $y=\sqrt{2}$. Dan zijn $x,y\in(\real_{>0}\backslash\rat)$ en $x^y=(\sqrt{2}^{\sqrt{2}})^{\sqrt{2}}= \sqrt{2}^{\sqrt{2}\cdot\sqrt{2}}=\sqrt{2}^2=2\in\rat$.\qed\dwn 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 \emph{intu\ui{}tionistisch} geldig is. Met behulp van intu\ui{}tionistische logica kun je alleen existentie uitspraken bewijzen als je ook daadwerkelijk voorbeelden kunt geven. Met meer moeite kan er toch een intu\ui{}tionistisch bewijs gegeven worden. Er is de stelling van Gelfond-Schneider, die impliceert dat $\sqrt{2}^{\sqrt{2}}\notin\rat$. Dat kan intu\ui{}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\ui{}tio\-nis\-ti\-sche) versie---is geheel duidelijk. We noemen het een `romantisch' bewijs: begrijpelijk voor de menselijke geest. \subsection*{Bewijzen via de computer: eerste poging} We kunnen proberen het bewijs van de stelling \ref{2.1} met behulp van een computer te leveren. \subsubsection*{Numerieke berekeningen (GP/PARI calculator)} Een goed numeriek programma zal niet blijken te helpen. \begin{alltt} ? sqrt(2) %1 = 1.414213562373095048801688724 ? %1^%1 %2 = 1.632526919438152844773495381 ? %2^%1 %3 = 1.999999999999999999999999999 \end{alltt} Ook al zou het antwoord \cour{\%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 \cour{\%1} en \cour{\%2} irrationale getallen staan. \subsubsection*{Computeralgebra (Mathematica)} Met behulp van `symbolisch rekenen' kunnen we iets meer. Een systeem dat dit kan rekent $\sqrt{2}^{\sqrt{2}}$ exact uit. \begin{alltt} In[1]:= (Sqrt[2]^Sqrt[2])^Sqrt[2]\medskip Out[1]= 2 \end{alltt} 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. \subsection*{Bewijzen via de computer: \emph{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. \subsubsection*{Interactieve bewijsverificatie (Mizar)} Het systeem Mizar van Trybulec (Bia{\polishl}ystok, Polen, in ontwikkeling sinds 1974), dat ge\ui{}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. \begin{alltt}\footnotesize --------------------------------------------------------------- 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; --------------------------------------------------------------- \end{alltt} Gebruik wordt gemaakt van reeds eerder geverifieerde stellingen.\dwn {\tt\footnotesize \def\^{\char`^} \btab{|l|l|} \hline POWER:38\hoog{1.2em}& a > 0 implies a to\_power b to\_power c = a to\_power (b * c);\dwn POWER:53 & a to\_power 2 = a\^2;\dwn SQUARE\_1:84 & 1 < sqrt 2;\dwn SQUARE\_1:def 3& x\^2 = x * x;\dwn SQUARE\_1:def 4& 0 <= a implies 0 <= sqrt a \& (sqrt a)\^2 = a;\dwn INT\_2:44 & 2 is prime;\dwn IRRAT\_1:1 & p is prime implies sqrt p is irrational;\dwn \hline \etab}\dwn 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 $\complex$ heeft een wortel in $\complex$); de hoofdstelling van de analyse (differenti\"eren 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). \subsubsection*{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\x y, x^y,\ldots$ en gelijkheden zoals $(x^y)^z=x^{y\x 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 \emph{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. %(Vb \verb+A->B&C, C->D, ~D |- ~A+ : via resolutie %wordt dit onbegrijpelijk; wellicht eenvoudiger \verb+A->B, ~B |- ~A+). \begin{alltt}\footnotesize ----------------------- 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 -----------------------------------\medskip 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)).\toolong 58 [para_into,22.3.1.2,8.1.1] rational(x^sqrt(y))|rational(sqrt(y))| -rational(x^y).\toolong 67 [para_into,58.3.1,5.1.1,unit_del,1] rational(x^sqrt(2))| -rational(x*x).\toolong 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.\medskip ----------------------- end of proof ------------------------------- \end{alltt}% $ Op een geheel andere manier---op grond van een door Collins \ncite{coll76} en anderen verbeterd algoritme van Tarski \ncite{tars51} 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 \ncite{buchwink98} en de methode van Wu, see \ncite{chou88}. \section{Hoe win je de hand van Portia?} Vrij naar het toneelstuk ``de Koopman van Veneti\"e'' van Shakespeare heeft \ncite{smul} de volgende puzzel verzonnen. \begin{quote} \parindent=1em \noi 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 \'e\'en 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. \end{quote} 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). \subsubsection*{Interactieve bewijsverificatie (Mizar)} \begin{alltt}\footnotesize 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; \end{alltt} 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. \section{\emph{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. \begin{quote} \url{www.mizar.org} \\ \url{pauillac.inria.fr/coq/} \\ \url{www.cl.cam.ac.uk/users/jrh/hol-light/} \\ \url{www.cl.cam.ac.uk/Research/HVG/Isabelle/} \\ \url{pvs.csl.sri.com} \end{quote} Andere relevante web-site voor Computer Wiskunde (onder meer over Otter en Automath) zijn de volgende. \begin{quote} \url{www-unix.mcs.anl.gov/AR/otter/} \\ \url{automath.webhop.net} \\ \url{www.cs.ru.nl/~freek/aut/} \\ \url{www.cs.ru.nl/~freek/digimath/} \\ \url{www.cs.ru.nl/~freek/qed/qed.html} \end{quote} Een greep uit de bibliotheek van geheel geformaliseerde stellingen. %de %hoofdstelling van de algebra (ieder polynoom over $\complex$ heeft een %wortel in $\complex$); de hoofdstelling van de analyse (differenti\"eren %van de integraal van een continue functie $f$ levert $f$ zelf op);% 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\"en 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 \ncite{barewied05} en \ncite{bare05}. Ondanks deze initi\"ele 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 \emph{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\ui{}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 \emph{alle} details daadwerkelijk ingevuld \emph{zijn}. Bij romantische bewijzen heeft men de tevredenheid omdat men ervan overtuigd is dat de details ingevuld \emph{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 \`a 50 jaar---een korte periode vanuit historisch oogpunt bezien---Computer Wiskunde gemeengoed zal zijn geworden. Menselijke intu\ui{}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\footnote{Computer 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 \ncite{barecohe01}.}, onderwijzen, verifi\"eren\footnote{Referees die ingezonden artikelen beoordelen zullen nog steeds nodig zijn; niet voor de correctheid, maar voor het belang van het werk.} en toepassen van de wiskunde. \noi --------------------------------------------------------- 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. \bibliography{eu} \end{document}