Список правил вывода

Это список правил вывода , логических законов, относящихся к математическим формулам.

Введение [ править ]

Правила вывода - это правила синтаксического преобразования, которые можно использовать для вывода заключения из предпосылки для создания аргумента. Набор правил может использоваться для вывода любого действительного вывода, если он является полным, и никогда не делать неверного вывода, если он верен. Обоснованный и полный набор правил не обязательно должен включать каждое правило из следующего списка, поскольку многие правила являются избыточными и могут быть проверены с помощью других правил.

Правила разряда позволяют делать вывод из субдеривации на основе временного предположения. Ниже обозначение

${\ displaystyle \ varphi \ vdash \ psi}$

указывает на такое отклонение от временного допущения к .${\ displaystyle \ varphi}$${\ displaystyle \ psi}$

Правила классического сентенциального исчисления [ править ]

Исчисление предложений также известно как исчисление высказываний .

Правила отрицания [ править ]

Reductio ad absurdum (или введение отрицания )

${\ displaystyle \ varphi \ vdash \ psi}$

${\ displaystyle {\ underline {\ varphi \ vdash \ lnot \ psi}}}$

${\ Displaystyle \ lnot \ varphi}$

Reductio ad absurdum (относится к закону исключенного третьего )

${\ Displaystyle \ lnot \ varphi \ vdash \ psi}$

${\ Displaystyle {\ подчеркивание {\ lnot \ varphi \ vdash \ lnot \ psi}}}$

${\ displaystyle \ varphi}$

Исключительное противоречие quodlibet

${\ displaystyle \ varphi}$

${\ displaystyle {\ underline {\ lnot \ varphi}}}$

${\ displaystyle \ psi}$

Устранение двойного отрицания

${\ Displaystyle {\ подчеркивание {\ lnot \ lnot \ varphi}}}$

${\ displaystyle \ varphi}$

Введение двойного отрицания

${\ displaystyle {\ underline {\ varphi \ quad \ quad}}}$

${\ Displaystyle \ lnot \ lnot \ varphi}$

Правила для условных выражений [ править ]

Теорема дедукции (или условное введение )

${\ displaystyle {\ underline {\ varphi \ vdash \ psi}}}$

${\ displaystyle \ varphi \ rightarrow \ psi}$

Modus ponens (или условное исключение )

${\ displaystyle \ varphi \ rightarrow \ psi}$

${\displaystyle {\underline {\varphi \quad \quad \quad }}}$

${\displaystyle \psi }$

Modus tollens

${\displaystyle \varphi \rightarrow \psi }$

${\displaystyle {\underline {\lnot \psi \quad \quad \quad }}}$

${\displaystyle \lnot \varphi }$

Правила союзов [ править ]

Присоединение (или Введение в соединение )

${\displaystyle \varphi }$

${\displaystyle {\underline {\psi \quad \quad \ \ }}}$

${\displaystyle \varphi \land \psi }$

Упрощение (или устранение конъюнкции )

${\displaystyle {\underline {\varphi \land \psi }}}$

${\displaystyle \varphi }$

${\displaystyle {\underline {\varphi \land \psi }}}$

${\displaystyle \psi }$

Правила дизъюнкции [ править ]

Сложение (или введение дизъюнкции )

${\displaystyle {\underline {\varphi \quad \quad \ \ }}}$

${\displaystyle \varphi \lor \psi }$

${\displaystyle {\underline {\psi \quad \quad \ \ }}}$

${\displaystyle \varphi \lor \psi }$

Анализ случая (или доказательство случаями или аргументом случаями или исключение дизъюнкции )

${\displaystyle \varphi \rightarrow \chi }$

${\displaystyle \psi \rightarrow \chi }$

${\displaystyle {\underline {\varphi \lor \psi }}}$

${\displaystyle \chi }$

Дизъюнктивный силлогизм

${\displaystyle \varphi \lor \psi }$

${\displaystyle {\underline {\lnot \varphi \quad \quad }}}$

${\displaystyle \psi }$

${\displaystyle \varphi \lor \psi }$

${\displaystyle {\underline {\lnot \psi \quad \quad }}}$

${\displaystyle \varphi }$

Конструктивная дилемма

${\displaystyle \varphi \rightarrow \chi }$

${\displaystyle \psi \rightarrow \xi }$

${\displaystyle {\underline {\varphi \lor \psi }}}$

${\displaystyle \chi \lor \xi }$

Правила для двухусловных [ править ]

Двузначное введение

${\displaystyle \varphi \rightarrow \psi }$

${\displaystyle {\underline {\psi \rightarrow \varphi }}}$

${\displaystyle \varphi \leftrightarrow \psi }$

Двуусловное исключение

${\displaystyle \varphi \leftrightarrow \psi }$

${\displaystyle {\underline {\varphi \quad \quad }}}$

${\displaystyle \psi }$

${\displaystyle \varphi \leftrightarrow \psi }$

${\displaystyle {\underline {\psi \quad \quad }}}$

${\displaystyle \varphi }$

${\displaystyle \varphi \leftrightarrow \psi }$

${\displaystyle {\underline {\lnot \varphi \quad \quad }}}$

${\displaystyle \lnot \psi }$

${\displaystyle \varphi \leftrightarrow \psi }$

${\displaystyle {\underline {\lnot \psi \quad \quad }}}$

${\displaystyle \lnot \varphi }$

${\displaystyle \varphi \leftrightarrow \psi }$

${\displaystyle {\underline {\psi \lor \varphi }}}$

${\displaystyle \psi \land \varphi }$

${\displaystyle \varphi \leftrightarrow \psi }$

${\displaystyle {\underline {\lnot \psi \lor \lnot \varphi }}}$

${\displaystyle \lnot \psi \land \lnot \varphi }$

Правила классического исчисления предикатов [ править ]

В следующих правилах это точно так же, за исключением того, что термин используется везде, где есть свободная переменная .${\displaystyle \varphi (\beta /\alpha )}$${\displaystyle \varphi }$${\displaystyle \beta }$${\displaystyle \varphi }$${\displaystyle \alpha }$

Универсальное обобщение (или универсальное введение )

${\displaystyle {\underline {\varphi {(\beta /\alpha )}}}}$

${\displaystyle \forall \alpha \,\varphi }$

Ограничение 1: это переменная, которая не встречается в . Ограничение 2: не упоминается ни в каких гипотезах или невыполненных предположениях.${\displaystyle \beta }$${\displaystyle \varphi }$
${\displaystyle \beta }$

Универсальное создание (или универсальное исключение )

${\displaystyle \forall \alpha \,\varphi }$

${\displaystyle {\overline {\varphi {(\beta /\alpha )}}}}$

Ограничение: Ни одно свободное вхождение in не попадает в сферу действия квантификатора, количественно определяющего переменную, встречающуюся в .${\displaystyle \alpha }$${\displaystyle \varphi }$${\displaystyle \beta }$

Экзистенциальное обобщение (или экзистенциальное введение )

${\displaystyle {\underline {\varphi (\beta /\alpha )}}}$

${\displaystyle \exists \alpha \,\varphi }$

Ограничение: Ни одно свободное вхождение in не попадает в сферу действия квантификатора, количественно определяющего переменную, встречающуюся в .${\displaystyle \alpha }$${\displaystyle \varphi }$${\displaystyle \beta }$

Экзистенциальное воплощение (или экзистенциальное исключение )

${\displaystyle \exists \alpha \,\varphi }$

${\displaystyle {\underline {\varphi (\beta /\alpha )\vdash \psi }}}$

${\displaystyle \psi }$

Ограничение 1: это переменная, которая не встречается в . Ограничение 2: Нет вхождения, свободного или связанного, in . Ограничение 3: не упоминается ни в каких гипотезах или невыполненных предположениях.${\displaystyle \beta }$${\displaystyle \varphi }$
${\displaystyle \beta }$${\displaystyle \psi }$
${\displaystyle \beta }$

Правила субструктурной логики [ править ]

Ниже приведены частные случаи универсального обобщения и экзистенциального исключения; они встречаются в субструктурной логике, такой как линейная логика .

Правило ослабления (или монотонности следования ) (также известное как теорема о запрете клонирования )

${\displaystyle \alpha \vdash \beta }$

${\displaystyle {\overline {\alpha ,\alpha \vdash \beta }}}$

Правило сокращения (или идемпотентности следования ) (также известное как теорема о запрете удаления )

${\displaystyle {\underline {\alpha ,\alpha ,\gamma \vdash \beta }}}$

${\displaystyle \alpha ,\gamma \vdash \beta }$

Таблица: Правила вывода [ править ]

Вышеуказанные правила можно обобщить в следующей таблице. ^[1] Столбец « Тавтология » показывает, как интерпретировать обозначение данного правила.

Правила вывода	Тавтология	Имя
${\displaystyle {\begin{aligned}p\\p\rightarrow q\\\therefore {\overline {q\quad \quad \quad }}\\\end{aligned}}}$	${\displaystyle (p\wedge (p\rightarrow q))\rightarrow q}$	Modus ponens
${\displaystyle {\begin{aligned}\neg q\\p\rightarrow q\\\therefore {\overline {\neg p\quad \quad \quad }}\\\end{aligned}}}$	${\displaystyle (\neg q\wedge (p\rightarrow q))\rightarrow \neg p}$	Modus tollens
${\displaystyle {\begin{aligned}(p\vee q)\vee r\\\therefore {\overline {p\vee (q\vee r)}}\\\end{aligned}}}$	${\displaystyle ((p\vee q)\vee r)\rightarrow (p\vee (q\vee r))}$	Ассоциативный
${\displaystyle {\begin{aligned}p\wedge q\\\therefore {\overline {q\wedge p}}\\\end{aligned}}}$	${\displaystyle (p\wedge q)\rightarrow (q\wedge p)}$	Коммутативный
${\displaystyle {\begin{aligned}p\rightarrow q\\q\rightarrow p\\\therefore {\overline {p\leftrightarrow q}}\\\end{aligned}}}$	${\displaystyle ((p\rightarrow q)\wedge (q\rightarrow p))\rightarrow (\ p\leftrightarrow q)}$	Закон двусмысленных предложений
${\displaystyle {\begin{aligned}(p\wedge q)\rightarrow r\\\therefore {\overline {p\rightarrow (q\rightarrow r)}}\\\end{aligned}}}$	${\displaystyle ((p\wedge q)\rightarrow r)\rightarrow (p\rightarrow (q\rightarrow r))}$	Экспорт
${\displaystyle {\begin{aligned}p\rightarrow q\\\therefore {\overline {\neg q\rightarrow \neg p}}\\\end{aligned}}}$	${\displaystyle (p\rightarrow q)\rightarrow (\neg q\rightarrow \neg p)}$	Закон транспозиции или противопоставления
${\displaystyle {\begin{aligned}p\rightarrow q\\q\rightarrow r\\\therefore {\overline {p\rightarrow r}}\\\end{aligned}}}$	${\displaystyle ((p\rightarrow q)\wedge (q\rightarrow r))\rightarrow (p\rightarrow r)}$	Гипотетический силлогизм
${\displaystyle {\begin{aligned}p\rightarrow q\\\therefore {\overline {\neg p\vee q}}\\\end{aligned}}}$	${\displaystyle (p\rightarrow q)\rightarrow (\neg p\vee q)}$	Материальное значение
${\displaystyle {\begin{aligned}(p\vee q)\wedge r\\\therefore {\overline {(p\wedge r)\vee (q\wedge r)}}\\\end{aligned}}}$	${\displaystyle ((p\vee q)\wedge r)\rightarrow ((p\wedge r)\vee (q\wedge r))}$	Распределительный
${\displaystyle {\begin{aligned}p\rightarrow q\\\therefore {\overline {p\rightarrow (p\wedge q)}}\\\end{aligned}}}$	${\displaystyle (p\rightarrow q)\rightarrow (p\rightarrow (p\wedge q))}$	Абсорбция
${\displaystyle {\begin{aligned}p\vee q\\\neg p\\\therefore {\overline {q\quad \quad \quad }}\\\end{aligned}}}$	${\displaystyle ((p\vee q)\wedge \neg p)\rightarrow q}$	Дизъюнктивный силлогизм
${\displaystyle {\begin{aligned}p\\\therefore {\overline {p\vee q}}\\\end{aligned}}}$	${\displaystyle p\rightarrow (p\vee q)}$	Добавление
${\displaystyle {\begin{aligned}p\wedge q\\\therefore {\overline {p\quad \quad \quad }}\\\end{aligned}}}$	${\displaystyle (p\wedge q)\rightarrow p}$	Упрощение
${\displaystyle {\begin{aligned}p\\q\\\therefore {\overline {p\wedge q}}\\\end{aligned}}}$	${\displaystyle ((p)\wedge (q))\rightarrow (p\wedge q)}$	Соединение
${\displaystyle {\begin{aligned}p\\\therefore {\overline {\neg \neg p}}\\\end{aligned}}}$	${\displaystyle p\rightarrow (\neg \neg p)}$	Двойное отрицание
${\displaystyle {\begin{aligned}p\vee p\\\therefore {\overline {p\quad \quad \quad }}\\\end{aligned}}}$	${\displaystyle (p\vee p)\rightarrow p}$	Дизъюнктивное упрощение
${\displaystyle {\begin{aligned}p\vee q\\\neg p\vee r\\\therefore {\overline {q\vee r}}\\\end{aligned}}}$	${\displaystyle ((p\vee q)\wedge (\neg p\vee r))\rightarrow (q\vee r)}$	Разрешение
${\displaystyle {\begin{aligned}p\rightarrow q\\r\rightarrow q\\p\vee r\\\therefore {\overline {q\quad \quad \quad }}\\\end{aligned}}}$	${\displaystyle ((p\rightarrow q)\wedge (r\rightarrow q)\wedge (p\vee r))\rightarrow q}$	Устранение дизъюнкции

Все правила используют основные логические операторы. Полная таблица «логических операторов» представлена таблицей истинности , дающей определения всех возможных (16) функций истинности 2 булевых переменных ( p , q ):

где T = истина и F = ложь, а столбцы являются логическими операторами: 0 , ложь, противоречие ; 1 , ИЛИ, логическое ИЛИ (стрелка Пирса); 2 , Конверс без импликации ; 3 , ¬p - отрицание ; 4 , материальное отсутствие импликации ; 5 , ¬q , отрицание; 6 , XOR, Исключительная дизъюнкция ; 7 , NAND, логический NAND (ход Шеффера); 8 , И, логическое соединение ; 9, XNOR, Если и только если , Логическое двусмысленное ; 10 , д - функция проекции ; 11 , if / then, Логическая импликация ; 12 , п - Проекционная функция; 13 , то / если, обратная импликация ; 14 , ИЛИ, логическая дизъюнкция ; 15 , правда, тавтология .

Каждый логический оператор может использоваться в утверждении о переменных и операциях, показывая основное правило вывода. Примеры:

• Оператор столбца 14 (ИЛИ) показывает правило сложения : когда p = T (гипотеза выбирает первые две строки таблицы), мы видим (в столбце 14), что p ∨ q = T.

  Мы также видим, что с той же посылкой верны и другие выводы: столбцы 12, 14 и 15 - T.

• Оператор столбца 8 (И) показывает правило упрощения : когда p ∧ q = T (первая строка таблицы), мы видим, что p = T.

  Исходя из этого предположения, мы также заключаем, что q = T, p ∨ q = T и т. Д., Как показано в столбцах 9-15.

• Оператор столбца 11 (IF / THEN) показывает правило Modus ponens : когда p → q = T и p = T, только одна строка таблицы истинности (первая) удовлетворяет этим двум условиям. В этой строке q также верно. Следовательно, всякий раз, когда p → q истинно и p истинно, q также должно быть истинным.

Машины и хорошо обученные люди используют этот взгляд на табличный подход, чтобы делать базовые выводы и проверять, можно ли получить другие выводы (для тех же посылок).

Пример 1 [ править ]

Рассмотрим следующие допущения: «Если сегодня идет дождь, то мы не пойдем на каноэ сегодня. Если мы не отправимся на каноэ сегодня, то мы отправимся на каноэ завтра». Следовательно (Математический символ для «поэтому» есть ), если сегодня пойдет дождь, завтра поедем в поход на каноэ ». Чтобы использовать правила вывода в приведенной выше таблице, мы допустим предложение «Если сегодня пойдет дождь», «Мы не пойдем сегодня на каноэ» и пусть будет «Мы отправимся в поход на каноэ завтра». Тогда этот аргумент имеет вид:${\displaystyle \therefore }$${\displaystyle p}$${\displaystyle q}$${\displaystyle r}$

${\displaystyle {\begin{aligned}p\rightarrow q\\q\rightarrow r\\\therefore {\overline {p\rightarrow r}}\\\end{aligned}}}$

Пример 2 [ править ]

Рассмотрим более сложный набор предположений: «Сегодня не солнечно и холоднее, чем вчера». «Мы будем купаться, только если будет солнечно», «Если мы не будем купаться, то у нас будет барбекю» и «Если у нас будет барбекю, то мы будем дома к закату» приводят к заключению » Мы будем дома к закату ". Доказательство с помощью правил вывода: пусть будет предложение «Сегодня солнечно», предложение «Холоднее, чем вчера», предложение «Мы пойдем купаться», предложение «У нас будет барбекю» и предложение « Мы будем дома к закату ". Тогда гипотезы превращаются в и . Используя нашу интуицию, мы предполагаем, что вывод может быть таким:${\displaystyle p}$${\displaystyle q}$${\displaystyle r}$${\displaystyle s}$${\displaystyle t}$${\displaystyle \neg p\wedge q,r\rightarrow p,\neg r\rightarrow s}$${\displaystyle s\rightarrow t}$${\displaystyle t}$. Используя таблицу правил вывода, мы можем легко доказать гипотезу:

Шаг	Причина
1.${\displaystyle \neg p\wedge q}$	Гипотеза
2. ${\displaystyle \neg p}$	Упрощение с использованием шага 1
3. ${\displaystyle r\rightarrow p}$	Гипотеза
4. ${\displaystyle \neg r}$	Modus tollens с использованием шагов 2 и 3
5. ${\displaystyle \neg r\rightarrow s}$	Гипотеза
6. ${\displaystyle s}$	Modus ponens с использованием шагов 4 и 5
7. ${\displaystyle s\rightarrow t}$	Гипотеза
8. ${\displaystyle t}$	Modus ponens с использованием шагов 6 и 7

Ссылки [ править ]

См. Также [ править ]

Список логических систем