Универсальное обобщение

Универсальное обобщение

Тип	Правило вывода
Поле	Логика предикатов
Заявление	Предполагать $P$ верно для любого произвольно выбранного $p$, затем $P$ верно обо всем.
Символическое заявление	$\vdash \!P(x)$, $\vdash \!\forall x\,P(x)$

В логике предикатов обобщение ( также универсальное обобщение , универсальное введение , GEN , UG ) — допустимое правило вывода . В нем говорится, что если $\vdash \!P(x)$ было получено, то $\vdash \!\forall x\,P(x)$ можно вывести.

Обобщение гипотезами

Правило полного обобщения допускает гипотезы слева от турникета , но с ограничениями. Предполагать $\Gamma$ представляет собой набор формул, $\varphi$ формула и $\Gamma \vdash \varphi (y)$ было выведено. Правило обобщения гласит, что $\Gamma \vdash \forall x\,\varphi (x)$ можно вывести, если $y$ не упоминается в $\Gamma$ и $x$ не происходит в $\varphi$.

Эти ограничения необходимы для обоснованности. Без первого ограничения можно было бы заключить $\forall xP(x)$ из гипотезы $P(y)$. Без второго ограничения можно было бы сделать следующий вывод:

1. $\exists z\,\exists w\,(z\not =w)$ (гипотеза)
2. $\exists w\,(y\not =w)$ (Экзистенциальная реализация)
3. $y\not =x$ (Экзистенциальная реализация)
4. $\forall x\,(x\not =x)$ (Ошибочное универсальное обобщение)

Это претендует на то, чтобы показать, что $\exists z\,\exists w\,(z\not =w)\vdash \forall x\,(x\not =x),$ что является необоснованным выводом. Обратите внимание, что $\Gamma \vdash \forall y\,\varphi (y)$ допустимо, если $y$ не упоминается в $\Gamma$ (второе ограничение не обязательно, так как семантическая структура $\varphi (y)$ не изменяется при замене каких-либо переменных).

Пример доказательства

Доказывать: $\forall x\,(P(x)\rightarrow Q(x))\rightarrow (\forall x\,P(x)\rightarrow \forall x\,Q(x))$ выводится из $\forall x\,(P(x)\rightarrow Q(x))$ и $\forall x\,P(x)$.

Доказательство:

Шаг	Формула	Обоснование
1	$\forall x\,(P(x)\rightarrow Q(x))$	Гипотеза
2	$\forall x\,P(x)$	Гипотеза
3	$(\forall x\,(P(x)\rightarrow Q(x)))\rightarrow (P(y)\rightarrow Q(y))$	Универсальная реализация
4	$P(y)\rightarrow Q(y)$	Из (1) и (3) Modus ponens
5	$(\forall x\,P(x))\rightarrow P(y)$	Универсальная реализация
6	$P(y)\$	Из (2) и (5) Modus ponens
7	$Q(y)\$	Из (6) и (4) Modus ponens
8	$\forall x\,Q(x)$	Из (7) путем обобщения
9	$\forall x\,(P(x)\rightarrow Q(x)),\forall x\,P(x)\vdash \forall x\,Q(x)$	Краткое изложение пунктов (1)–(8)
10	$\forall x\,(P(x)\rightarrow Q(x))\vdash \forall x\,P(x)\rightarrow \forall x\,Q(x)$	Из (9) по теореме дедукции
11	$\vdash \forall x\,(P(x)\rightarrow Q(x))\rightarrow (\forall x\,P(x)\rightarrow \forall x\,Q(x))$	Из (10) по теореме дедукции

В этом доказательстве на шаге 8 использовалось универсальное обобщение. Теорема о дедукции была применима на шагах 10 и 11, поскольку в перемещаемых формулах нет свободных переменных.

См. также

• Логика первого порядка
• Поспешное обобщение
• Универсальная реализация