Я не понимаю, зачем нужна отдельная сущность, как предикаты? Почему бы все не заменить функциями и оставить только равенство?
Определение. Сигнатура - это тройка

, где

- множество функциональных символов,

- функция, которая каждому функциональному символу сопоставляет его арность (начиная с нуля),

- символ равенства. Функциональных символы нулевой арности будем называть константами.
Тогда, например, исчисление предикатов можно так построить. Берем сигнатуру, символы переменных, служебные символы. Говорим, что должны быть символы

и

среди констант (для обозначения истины и лжи). Что должны быть символы

среди функциональных символов арности 2 и функциональный символ

арности 1. Дальше, говорим, что терм - это либо символ переменной, либо запись вида

, где

- функциональный символ, а

- термы, и что формула - это

, где

- термы.
Аксиомы и правила вывода будут все те же, но запись другая. Все перечислять не буду, но, чтобы была понятна логика, приведу несколько (

, естественно, имеет самый низкий приоритет):

![$$\forall x (A \to A[t/x]=T)=T$$ $$\forall x (A \to A[t/x]=T)=T$$](https://dxdy-04.korotkov.co.uk/f/f/e/9/fe9ce9d45d466613439030c1ee7db79282.png)

где

,

- формулы.
Все это, имхо, намного удобней (особенно, когда истинностных значений больше двух), логичней и красивей классического подхода.
-- 11.11.2012, 01:07 --Просьба. Если кто знает литературу по математической логике, где используется подобный подход, пожалуйста, сообщите.