Список правил вывода - List of rules of inference

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

Вступление

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

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

${\ 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 {\ подчеркивание {\ lnot \ psi \ quad \ quad \ quad}}}$

${\ displaystyle \ lnot \ varphi}$

Правила союзов

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

${\ displaystyle \ varphi}$

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

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

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

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

${\ displaystyle \ varphi}$

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

${\ displaystyle \ psi}$

Правила дизъюнкций

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

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

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

${\ Displaystyle {\ подчеркивание {\ 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 {\ подчеркивание {\ lnot \ varphi \ quad \ quad}}}$

${\ displaystyle \ psi}$

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

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

${\ displaystyle \ varphi}$

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

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

${\ Displaystyle \ psi \ rightarrow \ xi}$

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

${\ Displaystyle \ чи \ лор \ хи}$

Правила для двусмысленных

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

${\ 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 {\ подчеркивание {\ lnot \ varphi \ quad \ quad}}}$

${\ Displaystyle \ lnot \ psi}$

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

${\ Displaystyle {\ подчеркивание {\ 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 {\ подчеркивание {\ lnot \ psi \ lor \ lnot \ varphi}}}$

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

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

В следующих правилах это точно так же, за исключением того, что термин используется везде, где есть свободная переменная . ${\ Displaystyle \ varphi (\ бета / \ альфа)}$${\ 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 \ существует \ альфа \, \ varphi}$

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

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

${\ Displaystyle \ существует \ альфа \, \ 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}$

Таблица: Правила вывода

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

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

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

п	q		0	1	2	3	4	5	6	7		8	9	10	11	12	13	14	15
Т	Т		F	F	F	F	F	F	F	F		Т	Т	Т	Т	Т	Т	Т	Т
Т	F		F	F	F	F	Т	Т	Т	Т		F	F	F	F	Т	Т	Т	Т
F	Т		F	F	Т	Т	F	F	Т	Т		F	F	Т	Т	F	F	Т	Т
F	F		F	Т	F	Т	F	Т	F	Т		F	Т	F	Т	F	Т	F	Т

где T = истина и F = ложь, а столбцы являются логическими операторами: 0 , ложь, противоречие ; 1 , ИЛИ, логическое ИЛИ (стрелка Пирса); 2 , Конверс без импликации ; 3 , ¬p - отрицание ; 4 , материальное отсутствие импликации ; 5 , ¬q , отрицание; 6 , XOR, Исключительная дизъюнкция ; 7 , NAND, логический NAND (ход Шеффера); 8 , И, логическое соединение ; 9 , XNOR, Если и только если , Логическое двусмысленное ; 10 , д - функция проекции ; 11 , если / то, логическая импликация ; 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 \ поэтому}$${\ displaystyle p}$${\ displaystyle q}$${\ displaystyle r}$

${\ displaystyle {\ begin {align} p \ rightarrow q \\ q \ rightarrow r \\\ поэтому {\ overline {p \ rightarrow r}} \\\ конец {выровнено}}}$

Пример 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

Рекомендации

Смотрите также

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