Приветствую, можете пожалуйста помочь понять, как в гильбертовском исчислении классической

Question

Приветствую, можете пожалуйста помочь понять, как в гильбертовском исчислении классической

первопорядковой логики доказать теорему:
∃хR(x,x) > ∃x∃yR(x,y)
Где > - импликация?
Хз откуда брать переменную y, если в посылке имеем исключительно переменные х

0

30.11.2023

8 ответов

34 просмотра

suhr

Ты ещё не забывай, что имена связанных переменных не существены.

0

30.11.2023

Мироед

Если без лишних правил доказывать, то ∃хR(x,x) > ∃x∃yR(x,y) ∀x∀y ~R(x,y) - посылка ∀y ~R(y,y) - подставили ~R(x,x) - опять убрали ∀x ~R(x,x) - генерализация получили ∀x∀y ~R(x,y) > ∀x ~R(x,x) осталось развернуть ~ ∀x ~R(x,x) > ~ ∀x∀y ~R(x,y) следующий шаг получаем искомое через правила о введении и устранении общности, а потом просто развернуть импликации

0

30.11.2023

Мироед

Если без лишних правил доказывать, то ∀x∀y ~R(x,y) - посылка ∀y ~R(z,y) - подставили ~R(z,z) - опять подставили ∀z ~R(z,z) - генерализация ~R(x,x) ∀x ~R(x,x) получили ∀x∀y ~R(x,y) > ∀x ~R(x,x) осталось развернуть ~ ∀x ~R(x,x) > ~ ∀x∀y ~R(x,y) следующий шаг получаем искомое исправил, там коллизия была

0

30.11.2023

Ласло Папп

Мироед
Если без лишних правил доказывать, то ∀x∀y ~R(x,y...

Каким образом можно сделать так: R(z,z) - опять подставили ∀z ~R(z,z) - генерализация z же входит в R (z,z) свободно?

0

30.11.2023

Мироед

Ласло Папп
Каким образом можно сделать так: R(z,z) - опять п...

входит, но мы же не применяли генерализацию к свободным переменным из посылок (которых нет), поэтому теорема о дедукции работает

0

30.11.2023