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

Правило вывода в логике предикатов

В логике предикатов обобщение ( также универсальное обобщение , универсальное введение , ^{[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. Мур и Паркер