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.