Какой занимательный подход. Если уж на то пошло, нигде в аксиомах не сказано, что
определена
только на
[это следует читать не так, как это написано, потому что
— это ведь функциональный символ, и он нигде не определён, но об этом теперь можно прочитать ниже].
А вообще, пусть меня поправят, но это какие-то весьма странные аксиомы. Если уж есть теория множеств и
, можно определить
прямее; если теорию множеств не включать, то надо убрать и
, заменив принадлежности множествам предикатами, при этом заменив
тавтологиями, и т. д.. А то какая-то непонятная середина.
-- Чт дек 24, 2015 14:06:46 --Но, допустим, мы всё-таки решили иметь дело с такими аксиомами. Ладно. Тогда
1. Если переменные здесь только одного типа — и, видимо, интерпретируются как множества, и потому есть ещё некоторое число не показанных здесь аксиом, касающихся
— то
, безусловно, как нормальный обычный функциональный символ, интерпретируется функцией
на всех множествах. (Ну или тех объектах, которыми мы заполняем область интерпретаций.) В том числе на
, и даже на
. И вопроса не стоит.
2. Если переменные нескольких сортов — например, натуральные(?) числа и подмножества
(
?) — то сначала надо дорассказать, чем мы это всё-таки интерпретируем (а то вон сколько сомнений), какого сорта терм
и какого сорта туда подставляемый
должны быть. А некорректность как-нибудь потом.