2. Что мы можем связывать кванторами всеобщности и существования? Только буквы, соотв. объектам или ТМ-абстракции также?
В любой формальной теории мы можем связывать кванторами любые переменные.
Можно ли из

и

заключить, что

?
Это должно выполняться обязательно, иначе равенство — не равенство.

Задать объект, как я понял, значит задать его поведение относительно этого символа слева и справа.
Для классов только справа. Для теории с «первообъектами» я бы выбрал использовать два набора переменных — для таких элементов и для классов — а не один на все сущности. Из-за того, что у автора один, получается вот эта ужасная непонятность. Жалко, больше никто здесь не отписывается — может, это моя личная проблема с пониманием такой формулировки.
Тут сразу возникает вопрос: если мы не можем связывать кванторами не-объекты, то как может в этой формуле

?
А там объект и стоит, хотя какой бы мы не подставили, формула будет ложной — но она ведь и не обязана на каком-то значении

быть истинной!
Хотя с конструированием формул я так и не разобрался. Было бы резонно автору где-нибудь построить теорию сразу и определить, из чего формулы состоят, из чего термы состоят, и все аксиомы. Если он этого не сделал в каком-нибудь приложении, очень жалко…