Bewijslogica

Bewijslogica is een tak van modal logic die zich bezighoudt met de formele onderbouwing van bewijspraatjes in wiskundige theorieën. De centrale idee is dat een modal operator, meestal aangeduid met □, staat voor “het is provable dat”. Op die manier kan men fundamentele vragen over wat er in een formele theorie als PA (Peano-achtige arithmetica) kan worden bewezen, systematiseren en waarvan men kan verwachten dat het verantwoord is op logische wijze.

Een kernsysteem in bewijslogica is Gödel–Löb logica (GL). GL bevat de klassieke K-axiomatiek voor modaliteit, de necessitation-regel (uit A volgt □A) en de Löb-axiom: □(□A → A) → □A. Deze axioma’s vangen de specifieke eigenschappen van provability in een arithmetische theorie af. Semantisch wordt GL meestal gegeven via Kripke-semantiek met een transitive en conversieel wel-gefundeerde toegangsrelatie, die de intuïtie van ‘probeer wat er kan worden bewezen’ weerspiegelt. De arithmetische interpretatie gebruikt de bewijspredicaat Pr_T(x) als □-interpretatie.

Een belangrijke resultatenbundel in bewijslogica is Solovay’s compleetheidsstelling (1976): GL is precies de provabiliteitslogica van PA. Dat wil zeggen, voor elke modal formule A geldt: PA bewijst de aritmetische vertaling van A als en slechts als GL A bewijst. Deze theorema’s verbinden de modaliteit van bewijslast direct met formele arithmetische bewijzen.

Varianten van bewijslogica omvatten onder meer polymodale systemen zoals GLP van Japaridze, waarin meerdere modaliteiten niveaus van reflectie en provability modelleren. Toepassingen liggen in de fundamentele analyse van bewijsmethoden, metamathematische resultaten en de studie van inconsistentie- en consistentiebeweringen.

Zie ook: Provability logic, Löb’s theorem, Solovay’s theorem, Gödel’s incompleteness theorems.