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

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

Введение

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

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

$\varphi \vdash \psi$

указывает на такой вывод из временного предположения $\varphi$ к $\psi$.

Правила исчисления высказываний

Правила отрицаний

Сведение к абсурду (или введение отрицания )

$\varphi \vdash \psi$

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

$\lnot \varphi$

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

$\lnot \varphi \vdash \psi$

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

$\varphi$

От любого противоречия

$\varphi$

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

$\psi$

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

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

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

$\varphi \rightarrow \psi$

Установка режима (или условное исключение )

$\varphi \rightarrow \psi$

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

$\psi$

Поднимая настроение

$\varphi \rightarrow \psi$

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

$\lnot \varphi$

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

Присоединение (или введение союза )

$\varphi$

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

$\varphi \land \psi$

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

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

$\varphi$

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

$\psi$

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

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

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

$\varphi \lor \psi$

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

$\varphi \lor \psi$

Анализ прецедентов (или «Доказательство по прецедентам» , или «Аргументация по прецедентам», или «Устранение дизъюнкции »).

$\varphi \rightarrow \chi$

$\psi \rightarrow \chi$

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

$\chi$

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

$\varphi \lor \psi$

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

$\psi$

$\varphi \lor \psi$

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

$\varphi$

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

$\varphi \rightarrow \chi$

$\psi \rightarrow \xi$

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

$\chi \lor \xi$

Правила для бикондиционалов

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

$\varphi \rightarrow \psi$

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

$\varphi \leftrightarrow \psi$

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

$\varphi \leftrightarrow \psi$

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

$\psi$

$\varphi \leftrightarrow \psi$

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

$\varphi$

$\varphi \leftrightarrow \psi$

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

$\lnot \psi$

$\varphi \leftrightarrow \psi$

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

$\lnot \varphi$

$\varphi \leftrightarrow \psi$

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

$\psi \land \varphi$

$\varphi \leftrightarrow \psi$

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

$\lnot \psi \land \lnot \varphi$

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

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

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

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

$\forall \alpha \,\varphi$

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

Универсальное создание экземпляров (или универсальное устранение )

$\forall \alpha \,\varphi$

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

Ограничение: Запрещено свободное появление $\alpha$ в $\varphi$ попадает в область действия квантора, количественно определяющего переменную, встречающуюся в $\beta$.

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

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

$\exists \alpha \,\varphi$

Ограничение: Запрещено свободное появление $\alpha$ в $\varphi$ попадает в область действия квантора, количественно определяющего переменную, встречающуюся в $\beta$.

Экзистенциальное создание экземпляров (или экзистенциальное устранение )

$\exists \alpha \,\varphi$

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

$\psi$

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

Правила субструктурной логики

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

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

$\alpha \vdash \beta$

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

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

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

$\alpha ,\gamma \vdash \beta$

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

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

Правила вывода	тавтология	Имя
${\begin{aligned}p\\p\rightarrow q\\\therefore {\overline {q\quad \quad \quad }}\\\end{aligned}}$	$(p\wedge (p\rightarrow q))\rightarrow q$	Настройка настроения
${\begin{aligned}\neg q\\p\rightarrow q\\\therefore {\overline {\neg p\quad \quad \quad }}\\\end{aligned}}$	$(\neg q\wedge (p\rightarrow q))\rightarrow \neg p$	Поднимая настроение
${\begin{aligned}p\rightarrow q\\q\rightarrow r\\\therefore {\overline {p\rightarrow r}}\\\end{aligned}}$	$((p\rightarrow q)\wedge (q\rightarrow r))\rightarrow (p\rightarrow r)$	Гипотетический силлогизм
${\begin{aligned}p\rightarrow q\\\therefore {\overline {p\rightarrow (p\wedge q)}}\\\end{aligned}}$	$(p\rightarrow q)\rightarrow (p\rightarrow (p\wedge q))$	Поглощение
${\begin{aligned}p\\q\\\therefore {\overline {p\wedge q}}\\\end{aligned}}$	$((p)\wedge (q))\rightarrow (p\wedge q)$	Знакомство с союзом
${\begin{aligned}p\wedge q\\\therefore {\overline {p\quad \quad \quad }}\\\end{aligned}}$	$(p\wedge q)\rightarrow p$	Устранение союза
${\begin{aligned}p\\\therefore {\overline {p\vee q}}\\\end{aligned}}$	$p\rightarrow (p\vee q)$	Введение в дизъюнкцию
${\begin{aligned}p\rightarrow q\\r\rightarrow q\\p\vee r\\\therefore {\overline {q\quad \quad \quad }}\\\end{aligned}}$	$((p\rightarrow q)\wedge (r\rightarrow q)\wedge (p\vee r))\rightarrow q$	Устранение дизъюнкции
${\begin{aligned}p\vee q\\\neg p\\\therefore {\overline {q\quad \quad \quad }}\\\end{aligned}}$	$((p\vee q)\wedge \neg p)\rightarrow q$	Дизъюнктивный силлогизм
${\begin{aligned}p\vee p\\\therefore {\overline {p\quad \quad \quad }}\\\end{aligned}}$	$(p\vee p)\rightarrow p$	Дизъюнктивное упрощение
${\begin{aligned}p\vee q\\\neg p\vee r\\\therefore {\overline {q\vee r}}\\\end{aligned}}$	$((p\vee q)\wedge (\neg p\vee r))\rightarrow (q\vee r)$	Разрешение
${\begin{aligned}p\rightarrow q\\q\rightarrow p\\\therefore {\overline {p\leftrightarrow q}}\\\end{aligned}}$	$((p\rightarrow q)\wedge (q\rightarrow p))\rightarrow (p\leftrightarrow q)$	Двуусловное введение

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

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

где T = true и F = false, а столбцы представляют собой логические операторы :

• 0 , ложь , противоречие ;
• 1 , НО , Логическое НО ( стрелка Пирса );
• 2. Обратная неимпликация ;
• 3 , ¬p , Отрицание ;
• 4. Отсутствие существенного значения ;
• 5 , ¬q , Отрицание ;
• 6 , XOR , Исключительная дизъюнкция ;
• 7 , NAND , Logical NAND ( Sheffer stroke );
• 8 , И , Логическое соединение ;
• 9 , XNOR , Если и только если , Логическое двуусловие ;
• 10 , q , Проекционная функция ;
• 11 , если/то , материальное условие ;
• 12 , р , Проекционная функция ;
• 13 , то/если, Обратная импликация ;
• 14 , ИЛИ , Логическая дизъюнкция ;
• 15 , верно , тавтология .

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

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

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

• Оператор столбца 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

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

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

Пример 2

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

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

См. также

• Список логических систем
• Удаление метода настройки