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

В логика предикатов, обобщение (также универсальное обобщение или же универсальное введение,^[1][2][3] GEN) это действительный правило вывода. В нем говорится, что если ${\displaystyle \vdash \!P(x)}$ был выведен, то ${\displaystyle \vdash \!\forall x\,P(x)}$ можно вывести.

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

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

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

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

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

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

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

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

Число	Формула	Обоснование
1	${\displaystyle \forall x\,(P(x)\rightarrow Q(x))}$	Гипотеза
2	${\displaystyle \forall x\,P(x)}$	Гипотеза
3	${\displaystyle (\forall x\,(P(x)\rightarrow Q(x)))\rightarrow (P(y)\rightarrow Q(y)))}$	Универсальное создание
4	${\displaystyle P(y)\rightarrow Q(y)}$	Из (1) и (3) по Modus ponens
5	${\displaystyle (\forall x\,P(x))\rightarrow P(y)}$	Универсальное создание
6	${\displaystyle P(y)\ }$	Из (2) и (5) по Modus ponens
7	${\displaystyle Q(y)\ }$	Из (6) и (4) по Modus ponens
8	${\displaystyle \forall x\,Q(x)}$	Из (7) по обобщению
9	${\displaystyle \forall x\,(P(x)\rightarrow Q(x)),\forall x\,P(x)\vdash \forall x\,Q(x)}$	Резюме от (1) до (8)
10	${\displaystyle \forall x\,(P(x)\rightarrow Q(x))\vdash \forall x\,P(x)\rightarrow \forall x\,Q(x)}$	Из (9) автора Теорема дедукции
11	${\displaystyle \vdash \forall x\,(P(x)\rightarrow Q(x))\rightarrow (\forall x\,P(x)\rightarrow \forall x\,Q(x))}$	Из (10) автора Теорема дедукции

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

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

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

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

1. Копи и Коэн
2. Hurley
3. Мур и Паркер