В логика предикатов, обобщение (также универсальное обобщение или же универсальное введение,[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, поскольку перемещаемые формулы не имеют свободных переменных.
Смотрите также
Рекомендации
- ^ Копи и Коэн
- ^ Hurley
- ^ Мур и Паркер