Внедрение Логики в строимую теории (на примере множеств)

[Mysterious Light]

Добрый день,

Вот уже который месяц задаюсь вопросом, но не могу на него найти ответ:
Каким образом происходит «внедрение» логики в ту теорию, которую мы строим?

Возьмём для примера теорию множеств, любимую. Есть несколько вариантов её построить. В любом случае, мы базируемся на представлении о том, что означают фразы «для любого x справедливо, что ...» и ей подобные, то есть у нас уже имеется некоторая построенная логика. Логику мы строим весьма абстрактно, опираясь на некоторый счетный алфавит символов переменных, содержание которых в рамках самой логики несущественно.
Моё непонимание связано с тем, как именно мы «вдыхаем» содержание в эти самые переменные, чтобы всё работало как надо. Иными словами, как именно мы объясняем формальной теории, что в одном случае квантором могут связываться только элементы, в другом случае — только множества, а в третьем случае — и то, и другое.

Я очень бы хотел, чтобы ответ базировался на NGB или на другом не-ZF варианте теории множеств, если можно.

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

[ChaosProcess]

(Оффтоп)

С НГ!

[Mysterious Light]

(Оффтоп)

И Вас также с прошедшим Новым годом и наступающим Рождеством!

Может кто-нибудь намекнуть, какую литературу стоит читать?

[AGu]

Едва ли я понял суть вопроса, но почему бы не ответить, коли просят?

Mysterious Light в сообщении #666894 писал(а):

как именно мы «вдыхаем» содержание в эти самые переменные, чтобы всё работало как надо.

«Работа» теории определяется выбором сигнатуры и аксиом (ну и правил вывода, которые обычно классические). Если сигнатура и аксиомы отвечают интуиции (содержанию), то и теоремы будут ей (ему) отвечать. Стало быть, «вдыхание содержания» осуществляется выбором сигнатуры и аксиом. Сигнатура и аксиомы какие надо $\Rightarrow$ всё работает как надо.

Mysterious Light писал(а):

как именно мы объясняем формальной теории, что в одном случае квантором могут связываться только элементы, в другом случае — только множества, а в третьем случае — и то, и другое.

Ну, во-первых, теория знать не знает о том, что мы подразумеваем под значениями переменных. Она просто работает, выводит теоремы из аксиом. А во-вторых, обычно рассматриваются теории, в которых нет разных сортов переменных. Так обстоит дело и с классической теорией множеств: коль скоро рядом с кванторами стоят переменные, причем все они -- одного сорта, а под значениями переменных мы подразумеваем множества, то квантоваться можно только по множествам. Этого вполне достаточно, если вовремя вспоминать, что элементы множеств, множества множеств, а также последовательности, функции и все прочее -- это тоже множества.

Mysterious Light писал(а):

Я очень бы хотел, чтобы ответ базировался на NGB или на другом не-ZF варианте теории множеств, если можно.

А вот одна из версий NGB -- как раз двухсортная. Там есть переменные двух сортов. Под значениями переменных одного сорта подразумеваются множества, а другого -- классы. Но это все -- неформально; теория опять-таки не в курсе, что мы там подразумеваем. Она, знай себе, теоремы выводит.

P.S. Почти уверен, что на вопрос я не ответил.

[jhanjaa]

Поищите
Introduction to Categories and Categorical
Logic
Samson Abramsky and Nikos Tzevelekos