Teorembevisning

Teorembevisning er prosessen med å vise at en matematisk påstand er sann innenfor et bestemt aksiomsystem. Et bevis består av en sekvens av påstander der hver påstand følger logisk fra aksiomer, definisjoner og tidligere bevis ved hjelp av gyldige slutningsregler. For at et bevis skal være gyldig, må det kunne etterprøves ut fra de gitte forutsetningene uten tvil.

Bevis brukes for å etablere teorem; de skiller seg fra empiri eller heuristiske argumenter ved at de gir en nødvendigvis sann konklusjon, gitt aksepterte prinsipper. I praksis innebærer beviset en konstruksjon hvor hver del er begrunnet i tidligere etablerte resultater.

Vanlige bevismetoder inkluderer direkte bevis, bevis ved motsigelse, bevis ved kontraposisjon og matematisk induksjon. Innenfor logikk og bevis-teori studeres hvordan bevis formuleres i formelle systemer, og sentrale begreper inkluderer aksiomer, definisjoner, bevisbarhet, konsistens og fullstendighet. Gödel's ufullstendighetsteoremer viser at i hvert tilstrekkelig kraftig system finnes sannheter som ikke kan bevises innenfor systemet selv.

I informatikk brukes bevis også til formell verifikasjon av programvare og hardware. Bevisassistenter og automatiserte verktøy som Coq, Isabelle/HOL og Lean hjelper til med å bygge og kontrollere formelle bevis, og bidrar til pålitelighet i programvareutvikling og sikkerhetskritiske systemer.

Bevis er sentralt for troverdighet og stringens i matematikk og naturvitenskap, og utgjør grunnlaget for det som ofte omtales som matematikkens nødvendige sikkerhetsnett.