Bewijstheorie: verschil tussen versies
Verwijderde inhoud Toegevoegde inhoud
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
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.
|