Bedingte Einführung - Biconditional introduction

In der Aussagenlogik ist die bikonditionale Einführung eine gültige Inferenzregel . Es ermöglicht eine zu schließen , eine biconditional aus zwei bedingten Anweisungen . Die Regel ermöglicht es, eine bikonditionale Aussage in einen logischen Beweis einzuführen . Wenn es wahr ist und wenn es wahr ist, kann man daraus schließen, dass es wahr ist. Zum Beispiel kann aus den Aussagen "Wenn ich atme, dann lebe ich" und "Wenn ich lebe, dann atme ich" geschlossen werden, dass "ich atme genau dann, wenn ich ' Ich lebe ". Die bikonditionale Einführung ist das Gegenteil der bikonditionalen Eliminierung . Die Regel kann formal wie folgt angegeben werden: ${\ displaystyle P \ to Q}$${\ displaystyle Q \ to P}$${\ displaystyle P \ leftrightarrow Q}$

${\ displaystyle {\ frac {P \ zu Q, Q \ zu P} {\ daher P \ leftrightarrow Q}}}$

Wenn die Regel lautet, dass überall dort, wo Instanzen von " " und " " in Zeilen eines Beweises erscheinen, " " gültig in eine nachfolgende Zeile eingefügt werden kann. ${\ displaystyle P \ to Q}$${\ displaystyle Q \ to P}$${\ displaystyle P \ leftrightarrow Q}$

Formale Notation

Die bikonditionale Einführungsregel kann in fortlaufender Notation geschrieben werden:

${\ displaystyle (P \ bis Q), (Q \ bis P) \ vdash (P \ leftrightarrow Q)}$

Wo ist ein metallogisches Symbol, das eine syntaktische Konsequenz darstellt, wenn und beide in einem Beweis sind? ${\ displaystyle \ vdash}$${\ displaystyle P \ leftrightarrow Q}$${\ displaystyle P \ to Q}$${\ displaystyle Q \ to P}$

oder als Aussage einer wahrheitsfunktionalen Tautologie oder eines Satzes der Aussagenlogik:

${\ displaystyle ((P \ bis Q) \ land (Q \ bis P)) \ bis (P \ leftrightarrow Q)}$

wo und sind Sätze, die in einem formalen System ausgedrückt werden . ${\ displaystyle P}$${\ displaystyle Q}$

Verweise