In der Satzlogik, biconditional Einführung ist eine gültige Regel der Schlussfolgerung. Es berücksichtigt, um einen biconditional aus zwei bedingten Behauptungen abzuleiten. Die Regel macht es möglich, eine biconditional Behauptung in einen logischen Beweis einzuführen. Wenn wahr ist, und dann man ableiten kann, dass wahr ist. Zum Beispiel von den Behauptungen, "wenn ich dann atme, bin ich" lebendig und, "wenn ich lebendig bin, dann atme ich" kann es abgeleitet werden, dass "ich atme, wenn, und nur wenn ich lebendig bin". Einführung von Biconditional ist die gegenteilige von der biconditional Beseitigung. Die Regel kann formell als festgesetzt werden:

:

wo die Regel dass darin besteht, wo auch immer Beispiele "" und "" auf Linien eines Beweises erscheinen, "" kann auf einer nachfolgenden Linie gültig gelegt werden.

Formelle Notation

Die biconditional Einführungsregel kann in der folgenden Notation geschrieben werden:

:

wo ein metalogical Symbol ist, das bedeutet, dass das eine syntaktische Folge ist, wenn und beide in einem Beweis sind;

oder als die Behauptung einer mit der Wahrheit funktionellen Tautologie oder der Lehrsatz der Satzlogik::wo, und in einem formellen System ausgedrückte Vorschläge sind.