Универсальное обобщение Тип | Правило вывода |
---|
Поле | Логика предикатов |
---|
Заявление | Предполагать верно для любого произвольно выбранного , затем верно обо всем. |
---|
Символическое заявление | , ![{\ displaystyle \ vdash \! \ forall x \, P (x)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/15b82a59925ed0531a224874f5fa115c7c1e49dd) |
---|
В логике предикатов обобщение ( также универсальное обобщение , универсальное введение , [1] [2] [3] GEN , UG ) — допустимое правило вывода . В нем говорится, что если
было получено, то
можно вывести.
Обобщение гипотезами [ править ]
Правило полного обобщения допускает гипотезы слева от турникета , но с ограничениями. Предполагать
представляет собой набор формул,
формула и
было выведено. Правило обобщения гласит, что
можно вывести, если
не упоминается в
и
не происходит в
.
Эти ограничения необходимы для обоснованности. Без первого ограничения можно было бы заключить
из гипотезы
. Без второго ограничения можно было бы сделать следующий вывод:
(гипотеза)
(Экзистенциальная реализация)
(Экзистенциальная реализация)
(Ошибочное универсальное обобщение)
Это претендует на то, чтобы показать, что
что является необоснованным выводом. Обратите внимание, что
допустимо, если
не упоминается в
(второе ограничение не обязательно, так как семантическая структура
не изменяется при замене каких-либо переменных).
Пример доказательства [ править ]
Доказывать:
выводится из
и
.
Доказательство:
Шаг
|
Формула
|
Обоснование
|
1
|
|
Гипотеза
|
2
|
|
Гипотеза
|
3
|
|
Универсальная реализация
|
4
|
|
Из (1) и (3) установив
|
5
|
|
Универсальная реализация
|
6
|
|
Из (2) и (5) установив
|
7
|
|
Из (6) и (4) установив
|
8
|
|
Из (7) путем обобщения
|
9
|
|
Краткое изложение пунктов (1)–(8)
|
10
|
|
Из (9) по теореме дедукции
|
11
|
|
Из (10) по теореме дедукции
|
В этом доказательстве на шаге 8 использовалось универсальное обобщение. Теорема о дедукции была применима на шагах 10 и 11, поскольку в перемещаемых формулах нет свободных переменных.
- ^ Копи и Коэн
- ^ Херли
- ^ Мур и Паркер