О функциональных символах - общий подход для элимин. фун.cим

[alex_dorin]

Здравствуйте !
Подскажите общий подход для элиминации функциональных cимволов в логике первого порядка.
С уважением
Александр Дорин

[arseniiv]

Можно чуть побольше контекста? Думаю, никто против этого не будет.

[alex_dorin]

функциональные символы вводят в первопорядковую логику аксиомами для этих функциональных символов.
Их всегда можно заменить выражением или с использованием ранее использованных предикатов или с использование новых и ранее использованных предикатов. Те использование функциональные символов - это консервативной расширение теории.
Видел в нескольких местах в англоязычной литературе методику их элиминации, но места не помню.

[AGu]

Ссылку не дам, но общая идея, наверное, такая.
Как бы ни вводился $n$-местный функциональный символ $f$,
если он введен «корректно», существует такая формула

$\delta(x_1,\dots,x_n,y)$,

не содержащая символа $f$, что в рассматриваемой теории
доказуема формула

$f(x_1,\dots,x_n)=y\,\Leftrightarrow\,\delta(x_1,\dots,x_n,y)$.

(Конкретный эффективный алгоритм поиска $\delta$ не подскажу,
но он наверняка определяется расширяющей аксиоматикой.)
Ну а дальше понятно: каждая атомарная формула

$p(\dots\,f(t_1,\dots,t_n)\,\dots)$,

содержащая $f$ на любой глубине вложенности
(здесь $p$ — предикатный символ, $t_i$ — термы),
заменяется формулой

$(\exists\,y)\bigl(\delta(t_1,\dots,t_n,y)\land p(\dots\,y\,\dots)\bigr)$,

где $y$ — новая переменная, и процесс повторяется
до тех пор, пока не исчезнут все вхождения $f$.

[arseniiv]

alex_dorin в сообщении #988254 писал(а):

Их всегда можно заменить выражением или с использованием ранее использованных предикатов или с использование новых и ранее использованных предикатов. Те использование функциональные символов - это консервативной расширение теории.

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