bevissteori

Bevissteori er en gren av matematisk logikk som studerer formelle beviser og deres egenskaper. Den undersøker hvilke utsagn som er beviselige innenfor et gitt aksiom-system, hvordan bevis kan formuleres og manipuleres, samt forholdet mellom bevisenes struktur og deres plass i modellteori. Bevisteori skiller ofte mellom syntaktiske aspekter (regler, symboler og beviskonstruksjoner) og semantiske aspekter (sannhet i modeller).

Hovedområder inkluderer formelle bevissystemer (for eksempel Hilbert-systemer), naturlig deduksjon og sequent-kalkulus, samt metoder for normalisering og kutte-eliminering. En sentral problemstilling er å vurdere beviskraften til ulike aksiomatiske systemer og å undersøke grenser som konsistens, fullstendighet og kompakthet.

Historisk har bevissteori sin opprinnelse i Hilberts program på tidlig 20. århundre. Gödel ga i 1931 ufullstendighetsteoremer som viser at ethvert konsistent, tilstrekkelig kraftig formelt system inneholder sanne utsagn som ikke kan bevises innenfor systemet. Gentzen demonstrerte i 1935 kutte-eliminering og andre teknikker som gir bevis for konsistensen av aritmetikk basert på svakere prinsipper. Senere utviklinger inkluderer reverse mathematics, som kartlegger hvilke aksiomer som er nødvendige for å bevise bestemte teoremer, og ordneanalyse, som måler bevisstyrken ved bruk av ordner.

Bevisteori har anvendelser i teoretisk informatikk og formell verifikasjon av programvare, samt i utviklingen av logiske systemer og typer teorier i datavitenskapen.