Двуусловное введение

Двуусловное введение

Тип	Правило вывода
Поле	Пропозициональное исчисление
Заявление	Если $P\to Q$ верно, и если $Q\to P$ верно, то можно сделать вывод, что $P\leftrightarrow Q$ это правда.
Символическое заявление	${\frac {P\to Q,Q\to P}{\therefore P\leftrightarrow Q}}$

В высказываний логике двуусловное введение является действительным правилом вывода . Это позволяет вывести из двустороннее условие двух условных утверждений . Правило позволяет ввести в логическое доказательство двуусловное утверждение . Если $P\to Q$ верно, и если $Q\to P$ верно, то можно сделать вывод, что $P\leftrightarrow Q$ это правда. Например, из утверждений «если я дышу, то я жив» и «если я жив, то я дышу» можно сделать вывод, что «я дышу тогда и только тогда, когда я Я жив». Двуусловное введение является обратным двуусловному исключению . Формально это правило можно сформулировать так:

${\frac {P\to Q,Q\to P}{\therefore P\leftrightarrow Q}}$

где правило таково: везде, где встречаются экземпляры " $P\to Q$" и " $Q\to P$"появляются в строках доказательства", $P\leftrightarrow Q$" может быть размещено на следующей строке.

Формальные обозначения

Правило двуусловного введения можно записать в последовательных обозначениях:

$(P\to Q),(Q\to P)\vdash (P\leftrightarrow Q)$

где $\vdash$ металогический символ , означающий, что $P\leftrightarrow Q$ является синтаксическим следствием, когда $P\to Q$ и $Q\to P$ оба находятся в доказательстве;

или как утверждение истинностной тавтологии или теоремы логики высказываний:

$((P\to Q)\land (Q\to P))\to (P\leftrightarrow Q)$

где $P$, и $Q$ Это предложения, выраженные в некоторой формальной системе .