Итак, «подвал» страницы 90.
«Часто встречаются теории первого порядка, в которых равенство

может быть определено. Это значит, что в такой теории К имеется формула
со свободными переменными
и 
, для которой, если

обозначить через

, формулы (6), (7) выводимы в К.»
— это формула вида
где
и
только имеющиеся в формуле предметные переменные или
и
выделенные переменные с которыми мы собрались работать и в формуле могут быть и другие переменные? Дальше идет странный для меня оборот речи «если
обозначить через
». Если посмотреть в определение на странице 86, то там «Будем для сокращения писать
вместо
», но тогда и
есть
? Но это приводит к проблеме в следующем куске текста:«При этом только следует условиться считать, что если

и

— термы, не свободные соответственно для

и

в

, то

служит сокращенным обозначением не для

, а для некоторой формулы

, которая получена из

подходящим переименованием связанных переменных (см. следствие 2.22) таким образом, чтобы

и

оказались свободными соответственно для

и

в

.»
Если речь идет о том, что формула
является формулой
, то как
и
могут быть не свободны соответственно для
и
в
? «Для таких теорий К могут быть доказаны предложения, аналогичные предложениям 2.25 и 2.26, в предположении, что (7) является теоремой в К для соответствующих типов формул

. (Предоставляется читателю в качестве упражнения.)
В теориях первого порядка с равенством для выражений вида «существует один и только один предмет

такой, что...» можно использовать следующее
Определение.

означает

.»
Благодаря предыдущему замечанию Xaositect,
вопрос с последним определением полностью прояснился. Спасибо!