Я не понимаю, зачем нужна отдельная сущность, как предикаты? Почему бы все не заменить функциями и оставить только равенство?
Определение. Сигнатура - это тройка
, где
- множество функциональных символов,
- функция, которая каждому функциональному символу сопоставляет его арность (начиная с нуля),
- символ равенства. Функциональных символы нулевой арности будем называть константами.
Тогда, например, исчисление предикатов можно так построить. Берем сигнатуру, символы переменных, служебные символы. Говорим, что должны быть символы
и
среди констант (для обозначения истины и лжи). Что должны быть символы
среди функциональных символов арности 2 и функциональный символ
арности 1. Дальше, говорим, что терм - это либо символ переменной, либо запись вида
, где
- функциональный символ, а
- термы, и что формула - это
, где
- термы.
Аксиомы и правила вывода будут все те же, но запись другая. Все перечислять не буду, но, чтобы была понятна логика, приведу несколько (
, естественно, имеет самый низкий приоритет):
где
,
- формулы.
Все это, имхо, намного удобней (особенно, когда истинностных значений больше двух), логичней и красивей классического подхода.
-- 11.11.2012, 01:07 --Просьба. Если кто знает литературу по математической логике, где используется подобный подход, пожалуйста, сообщите.