В логике предикатов , обобщение (также универсальное обобщение или универсальное введение , [1] [2] [3] GEN ) является действительным правилом вывода . В нем говорится, что если был выведен, то можно вывести.
Правило полного обобщения допускает гипотезы слева от турникета , но с ограничениями. Предполагать набор формул, формула и был выведен. Правило обобщения гласит, что можно вывести, если не упоминается в а также не встречается в .
Эти ограничения необходимы для надежности. Без первого ограничения можно было бы сделать вывод из гипотезы . Без второго ограничения можно было бы сделать следующий вывод:
- (Гипотеза)
- (Экзистенциальная реализация)
- (Экзистенциальная реализация)
- (Ошибочное универсальное обобщение)
Это призвано показать, что что является необоснованным выводом. Обратите внимание, чтодопустимо, если не упоминается в (второе ограничение может не применяться, так как семантическая структура не изменяется подстановкой каких-либо переменных).
Доказывать: выводится из а также .
Доказательство:
Число | Формула | Обоснование |
---|
1 | | Гипотеза |
2 | | Гипотеза |
3 | | Универсальное создание |
4 | | Из (1) и (3) Modus ponens |
5 | | Универсальное создание |
6 | | Из (2) и (5) Modus ponens |
7 | | Из (6) и (4) Modus ponens |
8 | | Из (7) по обобщению |
9 | | Резюме от (1) до (8) |
10 | | Из (9) по теореме дедукции |
11 | | Из (10) по теореме дедукции |
В этом доказательстве на шаге 8 использовалось универсальное обобщение. Теорема вывода применялась на шагах 10 и 11, поскольку перемещаемые формулы не имеют свободных переменных.