Правильно ли я понимаю, что в самом начале я воспользовался тем, что X и x непустые?
Не обязательно, если аккуратно оформить доказательство. Раскроем сначала левую часть доказываемой импликации:
означает
. Раскроем правое:
. Теперь соберём некоторые знания о выводимости в логике первого порядка вместе:
• чтобы доказать
, достаточно взять произвольный «свежий» объект
и показать
, после чего мы можем выкинуть
из рассмотрения везде, где используется
;
• из
мы получаем
для любого выражения
, включая свежевведённые переменные как выше;
• чтобы доказать
, достаточно доказать
для произвольного выражения
;
• если
, то мы можем доказать оттуда некоторое
, если можем доказать
из
для некоторой свежей (не входит в
) «переменной-константы»
.
Последнее лишь для полноты картины, чтобы вы увидели некоторую симметрию.
Теперь следите за руками.
У нас есть
и мы собираемся показать
.
Введём свежий
, для него нам надо показать
.
Значит мы можем принять
, а показать надо будет
.
Введём свежий
, для которого надо показать
.
Мы можем принять
, осталось показать
…
И вот теперь мы начнём вгрызаться в первую, изначальную, посылку!
У нас есть
, значит мы можем сказать в частности
, то есть
.
Если теперь мы покажем, что
, то мы можем получить
(и нам повезло, это как раз сразу наша цель).
У нас активно предположение, что
, и также что
. Это ровно такое
, что требуется, чтобы доказать
!
Значит,
, и значит, мы доказали всё, что хотели.
Это может смотреться немного лучше в виде дерева натурального вывода, но оно наверно будет слишком длинным в ширину.
-- Ср май 05, 2021 17:28:52 --А что буква
обозначает?
Скорее всего множество всех подмножеств.
-- Ср май 05, 2021 17:54:13 --Кстати отсюда видно, что мы доказывали очень естественный факт (плюс там ведь ещё и в обратную сторону следует): в доказательстве мы просто распаковывали и запаковывали и перекладывали без взывания к каким-то аксиомам теории множеств кроме тех, что нужны для выписывания смысла
и
в самом начале.