'''Bewijstheorie''' is een tak van de [[wiskundige logica]] die [[Wiskundig bewijs|bewijzen]] als formele [[wiskundig object|wiskundige objecten]] opvat. Hierdoor kunnen bewijzen door middel van wiskundige technieken worden geanalyseerd. Bewijzen worden meestal gepresenteerd als [[Deductie versus inductie#inductie (wiskunde)|inductief]] gedefinieerde [[datastructuur|datastructuren]], zoals gewone [[lijst (informatica)|lijst]]en, ''boxed'' lijsten, of [[boomstructuur|boomstructurenalgoritme]]n, die volgens de [[axioma]]'s en [[afleidingsregel]]s van het logisch systeem worden geconstrueerd. Als zodanig is de bewijstheorie [[syntaxisSyntaxis (logica)|syntactisch]] van aard, dit in tegenstelling tot de [[modeltheorie]], die van nature [[Formele semantiek|semantisch]] is. Samen met de [[modeltheorie]], de [[axiomatische verzamelingenleer]] en de [[recursietheorie]] wordt de '''bewijstheorie''' gezien als één van de vier zogenaamde pilaren van de [[grondslagen van de wiskunde]].<ref name=wang>{{citeCite book
| last = Wang
| first = Hao
| authorlink = Hao Wang (wetenschapper)
| title = Popular Lectures on Mathematical Logic (Populaire colleges in de wiskundige logica)
| publisher = Van Nostrand|Van Nostrand Reinhold Company
| year = 1981
| isbn = 0442231091
| paginas = 3–4
}}</ref>
Bewijstheorie kan ook beschouwd worden beschouwd als een tak van de [[filosofische logica]], waarwaarin het primaire interessegebied in het idee van eende ''bewijstheoretische semantiek'' ligt,het eenbelangrijkste opvattingis. dieHet afhangthangt vanervan hetaf feit ofdat bepaalde technische ideeën in de ''structurele bewijstheorie'' al ofdan 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 initiëerde het naar hem genoemde [[programma van Hilbert]] in de [[grondslagen van de wiskunde]]. InDit eerste instantie hielpprogramma [[Kurt Gödel]] Hilberts programma,streeft omernaar de gehele wiskunde te reduceren tot een eindig [[formeel systeem]], metbasis zijnhiervoor is de [[volledigheidsstelling van Gödel|volledigheidsstelling]]. goedHet vooruitwerk werd uitgevoerd met behulp van de bewijscalculus die het Hilbert-systeem wordt genoemd. LaterIn eerste instantie hielp [[Kurt Gödel]] mee aan Hilberts programma, later echter weerlegde Gödel dithet uitgangspunt van het programma door inmet zijn [[Onvolledigheidsstellingen van Gödel|onvolledigheidsstellingen]] aan te tonen dat het gestelde doel onbereikbaar iswas. 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 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]]), 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 ''[[formeelFormeel 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 het [[Programmeren (computer)|programmeringprogrammeren]] in [[machinecodemachinetaal]] voor een [[Softwareontwikkelaar|computerprogrammeur]].
Formele bewijzen worden in de [[interactieve bewijsvoering]]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 ''vinden''schrijven van bewijzeneen ([[automatisch bewijzen van stellingencomputerprogramma]]) daarentegen zeer ingewikkeld is. Een informeel bewijsdat in de wiskundeliteratuurwiskunde vereist in contrast daarmee weken van [[collegiale toetsing]] (Eng: peer review) om dit bewijs te controleren enbewijzen kan ookgeven dandaarentegen nogzeer steedsingewikkeld fouten bevattenis.
Nieuwe bewijzen in de literatuur zijn informeel. Deze zijn dermate ingewikkeld, dat de handmatige controle ervan weken van [[collegiale toetsing]] vereist.
{{References}}
|