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

В логика предикатов, обобщение (также универсальное обобщение или же универсальное введение,[1][2][3] GEN) это действительный правило вывода. В нем говорится, что если был выведен, то можно вывести.

Обобщение с гипотезами

Правило полного обобщения допускает гипотезы слева от турникет, но с ограничениями. Предполагать это набор формул, формула и был выведен. Правило обобщения гласит, что можно получить, если не упоминается в и не встречается в .

Эти ограничения необходимы для надежности. Без первого ограничения можно было бы сделать вывод из гипотезы . Без второго ограничения можно было бы сделать следующий вывод:

  1. (Гипотеза)
  2. (Экзистенциальное создание)
  3. (Экзистенциальное создание)
  4. (Ошибочное универсальное обобщение)

Это призвано показать, что что является необоснованным выводом. Обратите внимание, что допустимо, если не упоминается в (второе ограничение применять не обязательно, поскольку семантическая структура не изменяется подстановкой каких-либо переменных).

Пример доказательства

Доказывать: выводится из и .

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

ЧислоФормулаОбоснование
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, поскольку перемещаемые формулы не имеют свободных переменных.

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

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

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