Насколько помню, автор того же Metamath ссылался на книжки
Gaisi Takeuti, Wilson M. Zaring. Axiomatic set theory
Gaisi Takeuti, Wilson M. Zaring. Introduction to axiomatic set theory
Я особо в них не вчитывался, но к формализации там должно быть аккуратное отношение. Например, обозначение применения функции отдельной операцией
, а взятия образа множества
, как это делается и в MM (или в этих книгах не совсем так — но автор MM хотя бы частично из них что-то почерпнул, это я у него в комментариях видел; кстати комментарии полезно почитать — там как раз объясняется и почему что-то сделано, и как, в том числе синтаксические подстановки опять со ссылкой на статью, где они рассматриваются, или какие-то использованные варианты аксиом логики и т. п.), когда в неформальном изложении обычно используют скобки и там, и там.
Ну и я верю, что есть и другие книги, и наверняка даже книги получше, но знаю только про эти. Стоит на всякий случай ожидать, что их мало и что они могут содержать чуть больше ошибок чем книги по областям, интерес к которым больше.
-- Вс фев 24, 2019 22:05:41 --В любом случае стоит сначала или параллельно почитать книгу вроде тех же Куратовского, Мостовского, чтобы к формализации были, скажем так, правильные вопросы. Теория множеств достаточно сложна.