Deduktionsteoremet

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 = {P₁,....P_n} 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 ${\displaystyle \vdash }$ G implicerar H ${\displaystyle \vdash }$ F→G, där symbolen, ${\displaystyle \vdash }$, betecknar syntaktisk konsekvens.

I det fall då premissmängden H är tom följer av deduktionsteoremet, att F ${\displaystyle \vdash }$G implicerar ${\displaystyle \vdash }$ F→G, vilket betyder att F→G är en tautologi.

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 ${\displaystyle \vdash }$ K implicerar H ${\displaystyle \vdash }$ ~F.

• Deduktion

• Shoenfield, Joseph R. Mathematical Logic, A K Peters, ISBN 978-1-56881-135-2, Nackit, Massachusetts 2001.