Почему лямбда-исчисление свободна от логики? (Барендрегт)

[creative]

Столкнулся с совершенно непонятным утверждением в книге Барендрегт Х. — Ламбда-исчисление. Его синтаксис и семантика на 36 странице (непонятное отметил подчеркиванием):

Цитата:

Отметим, что $\lambda$ свободна от логики - это эквациональная теория. Логические связки и кванторы будут использоваться в неформальном метаязыке при описании свойств теории $\lambda$.

Насколько я понял эквациональный язык логики первого порядка это такой язык формулы которого суть тождества (источник: Артамонов В.А., Салий В.Н., Скорняков Л.А. — Общая алгебра (том 2) страница 172).

Но как это связать с утверждением из книги Барендрегта я не понимаю.
То есть я понимаю, что логические связки и кванторы в книге (где описывается сама теория) используются в неформальном метаязыке только для описания свойств теории $\lambda$, но разве сама теория не может быть описана в языке первого порядка?

[arseniiv]

Не знаю. Если мы введём функциональные символы для аппликации и абстракции и предикаты $=$, $\to$, то ведь вроде бы можно включить $\lambda$-исчисление в логику предикатов. Только надо подумать, как аксиомы в такой модели вывести все. Наверно, ещё какие-нибудь допущения надо сделать? (Типа эквивалентности формул с переименованными связанными переменными.)

Только вот не помню, функциональные символы могут иметь аргументами что попало? Если да, то вроде бы ничего неправильного я не написал.

Про значение термина «эквациональная теория» могу только подозревать, что оно описывает, что все формулы состоят из двух частей, разделённых $=$ или $\to$, но т. к. $=$ выглядит более «практическим», автор назвал теорию по нему.

[creative]

Функции в интерпретации языка первого порядка в качестве аргументов принимают объекты из предметной области и если в языке первого порядка таких предметных областей несколько, то в определении функциональных символов должен указываться сорт каждого аргумента, а сорта соответствуют предметным областям (проще говоря сорт есть тип переменной на программистский лад).
Я не разбирался в деталях, но не вижу проблем, чтобы ввести в функциональные символы для типов термов, которые есть в $\lambda$-исчислении и предиката для $=$.

Я думаю, если автор не остановился на разборе своего утверждения, то значит там есть простое и общее объяснение.

[arseniiv]

Тогда я тоже не вижу. Тогда надо разобраться только с аксиомами и правилами вывода. Как-то надо обозначить (забыл слово, в общем, чтобы она корректно вводилась, ведь мы можем добавлять только аксиомы (или схемы аксиом), и в сигнатуру функциональные и предикатные символы) замену переменных в термах, например.