Deduktionsteoremet (även kallad "CP-regeln", från engelska: Conditional Proof) är ett metateorem inom satslogiken. Teoremet är en vid bevisföring effektiv slutledningsregel, som ofta används då en slutsats skall härledas, där huvudoperationen är en materiell implikation. Alfred Tarski bevisade teoremet 1931, men det tidigaste publicerade beviset var av Jacques Herbrand, 1930.
Deduktionsteoremet: Om man från en premissmängd H = {P1,....Pn} jämte en formel F kan härleda slutsatsen G, så kan man från H härleda F→G.
Deduktionsteoremet uttryckt med symboler: H ʌ F G implicerar H F→G, där symbolen, , betecknar syntaktisk konsekvens.
I det fall då premissmängden H är tom följer av deduktionsteoremet, att F G implicerar F→G, vilket betyder att F→G är en tautologi.
Reductio ad absurdum
Om den härledda satsen G är en kontradiktion K, så följer av F→K och med stöd av den så kallade absurditetsregeln ("Ab-regeln") att F är falsk. Om man således, från H och F kan härleda en kontradiktion, så kan man med Ab-regeln dra slutsatsen att F är falsk. Den slutledningsregel man får vid sammansättning av CP-regeln och Ab-regeln går under namnet Reductio ad absurdum, den så kallade Reductio ad absurdum-regeln ("RAA-regeln").
RAA-regeln uttryckt med symboler: H ʌ F K implicerar H ~F.[1][2]
Se även
Källor
Wikiwand in your browser!
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.