Bewijstheorie: verschil tussen versies

Verwijderde inhoud Toegevoegde inhoud
JRB (overleg | bijdragen)
kGeen bewerkingssamenvatting
kGeen bewerkingssamenvatting
Regel 12:
 
== Geschiedenis ==
Hoewel de formalisering van de logica veel te danken heeft aan het werk van [[Gottlob Frege]], [[Giuseppe Peano]], [[Bertrand Russell]] en [[Richard Dedekind]], wordt [[David Hilbert]] vaak als de grondlegger van de moderne bewijstheorie gezien. Hij initiëerde het naar hem genoemde [[programma van Hilbert]] in de [[grondslagen van de wiskunde]]. In eerste instantie hielp [[Kurt Gödel]]'s Hilberts's programma om de gehele wiskunde te reduceren tot een eindig [[formeel systeem]] met zijn [[Volledigheidsstellingen van Gödel|volledigheidsstellingen]] goed vooruit. Later echter weerlegde Gödel dit programma door in zijn [[Onvolledigheidsstellingen van Gödel|onvolledigheidsstellingen]] aan te tonen dat het gestelde doel onbereikbaar is. Al dit werk werd uitgevoerd met behulp van de bewijscalculus die het [[Hilbert systeem]] wordt genoemd.
 
Parallel aan dit bewijstheoretische werk van Gödel, legde [[Gerhard Gentzen]] het fundament voor wat nu bekend staat als de [[structurele bewijstheorie]]. In een relatief korte tijdsperiode introduceerde Gentzen de kern formalismen van de natuurlijke deductie (gelijktijdig met en onafhankelijk van Jaskowski), de volgorde-calculus, boekte hij fundamentele vooruitgang bij de formalisering van intuïtionistische logica, introduceerde hij het belangrijke idee van een [[analytisch bewijs]], en leverde hij het eerste combinatorische bewijs van de consistentie van de [[Peano rekenkunde]].
 
==Formeel en informeel bewijs==
De ''informele'' bewijzen uit de wiskundige dagelijkse praktijk komen niet overeen met de ''[[formeel bewijs|formele'' bewijzen]]'' uit de bewijstheorie. Men kan informele bewijzen nog het beste vergelijken met schetsen, waarin de grote lijnen worden uitgezet, aan de hand waarvan een expert met genoeg tijd en geduld een formeel bewijs kan reconstrueren. Voor de meeste wiskundigen zou het schrijven van een volledig formeel bewijs echter dezelfde nadelen hebben als [[programmeren|programmering]] in [[machinecode]] voor een [[computerprogrammeur]].
 
Formele bewijzen worden in de [[interactieve bewijsvoering]] met de hulp van speciale [[software]] op de [[computer]] geconstrueerd. Belangrijker is echter dat deze bewijzen op deze computer automatisch kunnen worden gecontroleerd. Het controleren van formele bewijzen is meestal triviaal, terwijl het ''vinden'' van bewijzen ([[automatisch bewijzen van stellingen]]) daarentegen zeer ingewikkeld is. Een informeel bewijs in de wiskunde literatuur vereist in contrast daarmee weken van de [[collegiale toetsing]] (eng: peer review) om dit bewijs te controleren en kan ook dan nog steeds fouten bevatten.