Bewijstheorie

Bewijstheorie is een tak van de wiskundige logica die bewijzen als formele wiskundige objecten opvat. Hierdoor kunnen bewijzen door middel van wiskundige technieken worden geanalyseerd. Bewijzen worden meestal gepresenteerd als inductief gedefinieerde algoritmen, die volgens de axioma's en afleidingsregels van het logisch systeem worden geconstrueerd. Als zodanig is de bewijstheorie syntactisch van aard, dit in tegenstelling tot de modeltheorie, die van nature semantisch is. Samen met de modeltheorie, de axiomatische verzamelingenleer en de recursietheorie wordt de bewijstheorie gezien als een van de vier zogenaamde pilaren van de grondslagen van de wiskunde. Bewijstheorie kan ook worden beschouwd als een tak van de filosofische logica, waarin de bewijstheoretische semantiek het belangrijkste is. Het hangt ervan af dat bepaalde ideeën in de structurele bewijstheorie al dan niet haalbaar zijn.

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 initieerde het naar hem genoemde programma van Hilbert in de grondslagen van de wiskunde. Dit programma streeft ernaar de gehele wiskunde te reduceren tot een eindig formeel systeem, basis hiervoor is de volledigheidsstelling van Gödel. Het werk werd uitgevoerd met behulp van de bewijscalculus die het Hilbert-systeem wordt genoemd. In eerste instantie hielp Kurt Gödel mee aan Hilberts programma, later echter weerlegde Gödel het uitgangspunt van het programma door met zijn onvolledigheidsstellingen aan te tonen dat het gestelde doel onbereikbaar was.

Parallel aan dit bewijstheoretische werk van Gödel, legde Gerhard Gentzen het fundament voor wat nu bekendstaat als de structurele bewijstheorie. In een relatief korte tijdsperiode introduceerde Gentzen de kernformalismen van de natuurlijke deductie, overigens gelijktijdig met en onafhankelijk van Stanislaw Jaskowski, 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 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 het programmeren in machinetaal voor een computerprogrammeur.

Formele bewijzen worden interactief 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 eenvoudig, terwijl het schrijven van een computerprogramma dat in de wiskunde bewijzen kan geven daarentegen zeer ingewikkeld is.

Nieuwe bewijzen in de literatuur zijn informeel. Deze zijn dermate ingewikkeld, dat de handmatige controle ervan weken van collegiale toetsing vereist.