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

В логике предикатов обобщение ( также универсальное обобщение , универсальное введение , ^{[1] [2] [3]} GEN , UG ) является действительным правилом вывода . В нем говорится, что если было получено, то и может быть получено. ${\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)}$

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

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

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

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

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

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