Сама подмена
на выражение есть очень привычная замена переменной на её значение
Речь идёт о схеме аксиом, то есть, о способе записи бесконечного множества аксиом. Здесь для каждой высказывательной функции
определяется своя аксиома. Схема аксиом формулируется не в языке предметной теории (здесь — теории множеств), а в метаязыке, в котором определяется язык предметной теории (чаще всего это просто естественный язык). Поэтому к предметной теории эти замены отношения не имеют.
Да, конечно, но сам логический вывод имеет место быть и для палок
К сожалению, у нас нет формализованной теории палок. Когда Вы её создадите, тогда будете говорить о логическом выводе в теории палок и сравнивать его с логическим выводом в теории множеств.
Вообще в изложении того же Куратовского и Мостовского фигурируют два понятия - элемент и множество.
Тяжёлый случай. Я не понимаю, как можно было вычитать такое в тексте данной книги. Фраза "
является элементом множества
" является словесной записью формулы
, то есть, слово "элемент" — это ссылка на символ "
" в формуле. Теория, излагаемая в книге Куратовского и Мостовского — это ZFC минус аксиома регулярности и плюс аксиома реляционных типов. В ней нет никаких "элементов", кроме множеств.
в выражении указано обязательное условие - икс принадлежит игрек
Нет там никакого "обязательного условия". В этом месте доказательства происходит консервативное расширение языка теории множеств: вводится постоянная "
", и для этой постоянной формулируется аксиома
которая служит определением множества
(словами: произвольно взятое множество
является элементом множества
тогда и только тогда, когда
является элементом самого себя). Сокращённо это записывается как
(словами:
— множество всех таких множеств, каждое из которых является элементом самого себя). Делается это просто для удобства. В свою очередь, запись аксиомы также является сокращением, а полная запись может выглядеть, например, так:
В рассматриваемом выражении ясно указано - икс входит в игрек
Но точно так же икс входит и в игрек.
Это какое-то недоразумение. "
" и "
" — это просто символы. Они "входить" друг в друга не могут. В данном случае они используются как имена некоторых множеств (постоянная "
" является именем некоторого вполне определённого множества, а переменная
— именем произвольно взятого множества).
Вы явно перепутали два совершенно разных понятия: «буква "
" входит в формулу
» (это означает, что если мы посмотрим на запись формулы, например, "
", то в этой записи найдём букву "
") и «число
входит в число
» (никакое число ни в какое другое не входит; не надо придумывать какой-нибудь специальный смысл для этого "входит"; множества тоже не "входят" друг в друга).