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

В логике предикатов , обобщение (также универсальное обобщение или повсеместное внедрение , GEN ) является действительным правилом вывода . В нем говорится, что если был получен, то может быть получен. ${\ 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 \ существует z \, \ существует w \, (z \ not = w)}$ (Гипотеза)
2. ${\ Displaystyle \ существует вес \, (у \ не = ш)}$ (Экзистенциальное создание)
3. ${\ Displaystyle у \ not = х}$ (Экзистенциальное создание)
4. ${\ Displaystyle \ forall х \, (х \ not = х)}$ (Ошибочное универсальное обобщение)

Это имеет целью показать то, что является необоснованным выводом. Обратите внимание, что допустимо, если не упомянуто в (второе ограничение применять не обязательно, поскольку семантическая структура не изменяется при замене каких-либо переменных). ${\ Displaystyle \ существует z \, \ существует 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)}$

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

Число	Формула	Обоснование
1	${\ Displaystyle \ forall x \, (P (x) \ rightarrow Q (x))}$	Гипотеза
2	${\ Displaystyle \ forall x \, P (x)}$	Гипотеза
3	${\ Displaystyle (\ forall x \, (P (x) \ rightarrow Q (x))) \ rightarrow (P (y) \ rightarrow Q (y))}$	Универсальный экземпляр
4	${\ Displaystyle P (y) \ rightarrow Q (y)}$	Из (1) и (3) Modus ponens
5	${\ Displaystyle (\ forall x \, P (x)) \ rightarrow P (y)}$	Универсальный экземпляр
6	${\ Displaystyle P (у) \}$	Из (2) и (5) Modus ponens
7	${\ Displaystyle Q (у) \}$	Из (6) и (4) Modus ponens
8	${\ Displaystyle \ forall х \, Q (х)}$	Из (7) по обобщению
9	${\ Displaystyle \ forall x \, (P (x) \ rightarrow Q (x)), \ forall x \, P (x) \ vdash \ forall x \, Q (x)}$	Резюме от (1) до (8)
10	${\ Displaystyle \ forall x \, (P (x) \ rightarrow Q (x)) \ vdash \ forall x \, P (x) \ rightarrow \ forall x \, Q (x)}$	Из (9) по теореме дедукции
11	${\ Displaystyle \ vdash \ forall x \, (P (x) \ rightarrow Q (x)) \ rightarrow (\ forall x \, P (x) \ rightarrow \ forall x \, Q (x))}$	Из (10) по теореме дедукции

В этом доказательстве на шаге 8 использовалось универсальное обобщение. Теорема вывода применялась на шагах 10 и 11, поскольку перемещаемые формулы не имеют свободных переменных.

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

• Логика первого порядка
• Поспешное обобщение
• Универсальный экземпляр

использованная литература