bevisteori

Bevisteori är en gren av matematisk logik som studerar formella bevis och de system som används för att bevisa matematiska påståenden. Den fokuserar på syntaktiska regler och bevisstrukturer inom ett givet formellt språk, samt hur bevis byggs, transformerar och analyseras. Bevisteori skiljer sig från modellteori genom att den inte primärt studerar hur påståenden är sanna i olika modeller utan hur de kan härledas inom ett officiellt system.

Historiskt utgår bevisteorin från Hilbertprogrammet på 1920-talet, som sökte en säker grund för aritmetik genom finita och mekaniskt kontrollerbara bevis. Nya former av formella system utvecklades, bland annat sequent calculus och natural deduction. Gentzen visade viktiga resultat som cut-elimination och Hauptsatz, vilket lade grunden för ett strukturerat synsätt på bevis och normalisering. På 1930-talet visade Gödels ofullständighetssatser att varje tillräckligt kraftfullt konsistent formellt system inte kan bevisa sin egen konsistens eller allt som är sant i aritmetik, vilket satte gränser för programmet. Dessa insikter ledde till utvecklingen av modern bevisteori och dess relation till grundläggande frågor i matematiken.

Viktiga begrepp inom bevisteori inkluderar formella system, derivationer, bevislängd, normalisering och cut-elimination, samt koncept som konsistens och fullständighet. Tillämpningar finns bland annat inom teoretisk datalogi, automatiserad bevisföring och formell verifiering av program och hårdvara. Bevisteori är ofta samverkan mellan syntaktiska metoder och strukturella analyser av bevis.