bevislogik

Bevislogikk er en gren av matematisk logikk som studerer formelle systemer for bevis og avledning av teoremer fra aksiomer. Den fokuserer på reglene og strukturen som gjør et bevis gyldig, og på egenskapene til bevisene snarere enn sannheten i en bestemt modell.

Sentral i bevislogikk er begrepene formelt språk, aksiomer og inferensregler, samt ulike bevissystemer som Hilbert-stil, naturlig deduksjon og sequentkalkulus. Forskningen undersøker egenskaper som lydhet (at hvert avledet teorem er sann i alle modeller den representerer), konsistens og fullstendighet, samt hvordan bevis kan omformes og forkortes gjennom normalisering eller cut-eliminering.

Historisk bidro Hilbert, Gentzen og Gödel til å gjøre bevislogikk til et selvstendig felt i mellomkrigstiden. Gödels fullstendighets- og ufullstendighetsteoremer viser henholdsvis at syntaktisk bevisbarhet for førsteordens logikk svarer til semantisk sannhet, og at noen aritmetiske systemer ikke kan bevise alle matematiske sannheter. Gentzens kut-eliminering er et sentralt resultat i strukturell bevisanalyse.

Bevislogikk har omfattende anvendelser i datavitenskap og matematikk, blant annet i formell verifikasjon, automatisert bevisføring og i utviklingen av programmeringsspråk og type-teori. Feltet gir også teoretiske verktøy som ligger til grunn for avanserte bevissystemer og verifikasjonsrammeverk.