
Не знаю. Если мы введём функциональные символы для аппликации и абстракции и предикаты

,

, то ведь вроде бы можно включить

-исчисление в логику предикатов. Только надо подумать, как аксиомы в такой модели вывести все. Наверно, ещё какие-нибудь допущения надо сделать? (Типа эквивалентности формул с переименованными связанными переменными.)
Только вот не помню, функциональные символы могут иметь аргументами что попало? Если да, то вроде бы ничего неправильного я не написал.
Про значение термина «эквациональная теория» могу только подозревать, что оно описывает, что все формулы состоят из двух частей, разделённых

или

, но т. к.

выглядит более «практическим», автор назвал теорию по нему.