
вот это смущает
если вы о доказательстве с аксиомой объемности, то от него попахивает (хотя кому как)
Я тоже его чувствую

но сформулировать чем именно "попахивает" трудно, да и неблагодарное это дело.
Но все же, кто-то должен это сказать. Если коротко, применимость этой формулы зависит от

или от

. Например, если они построены с аксиомой бесконечности или с аксиомой выбора или еще как-то, то в интуиционизме или конструктивизме или еще в каком-то направлении, эта формула к ним не применима. Т.е. она, как логический закон остается в силе, но имеет свои ограничения, когда речь идет о некоторых предикатах, как например, предикате Кантора об образовании множеств процедурой "неограниченной свертки". Вы скажите, это проблемы теории, а не самого закона. Возможно, но в конечном счете, чем лучше теории с этим законом по сравнению с теориями, в котором его нет или есть его отрицание ? Он определенно разграничивает теории, но определенно не по критерию противоречивости.
Допустим,

перечислимые множества доказуемых утверждений двух эквивалентных теорий, а

и

- множества недоказуемых утверждений этих теорий, которые не перечислимы. Предположим, есть некое утверждение истинное в одной теории, но ложное в другой (из числа недоказуемых). Например, геделевские предложения с разными номерами. Тогда эквивалентность

ложна, т.к. одно утверждение истинно, а другое нет.
Может быть пример не удачный, но думаю, смысл который я хотел передать понятен. Наверняка, найдутся другие примеры, т.к. большинство операций не симметрично в каком-то общем трудно уловимом смысле, хотя бы тот же пример
epros с необратимыми во времени уравнениями или дополнениями неизмеримых или перечислимых множеств и т.д.
Когда речь идет о дополнениях пустого множества, в столь сильных теориях, смысл их эквивалентности теряется. Отрицание - это какое-то слишком неопределенное отношение, даже в виде отрицания принадлежности, чтобы давать что-то определенное в теориях со столь неопределенными совокупностями, не имеющими моделей.
Мне, например, это доказательство представляется чем-то вроде неочевидной аксиомы, вроде тех, которые не нравятся интуиционистам или конструктивистам. Она какая-то неестественная, оставляющая осадок неудовлетворенности.