Формальная система исчисления предикатов

Язык логики первого порядка строится на основе сигнатуры, состоящей из множества функциональных символов и множества предикатных символов . С каждым функциональным и предикатным символом связана арность, то есть число возможных аргументов. Допускаются как функциональные, так и предикатные символы арности 0. Первые иногда выделяют в отдельное множество констант. Кроме того, используются следующие дополнительные символы

Символы переменных (обычно и т. д.),

Пропозициональные связки: ,

Кванторы: всеобщности и существования ,

Служебные символы: скобки и запятая.

Перечисленные символы вместе с символами из и образуют Алфавит логики первого порядка. Более сложные конструкции определяются индуктивно:

Терм есть символ переменной, либо имеет вид , где — функциональный символ арности , а — термы.

Атом имеет вид , где — предикатный символ арности , а — термы.

Формула — это либо атом, либо одна из следующих конструкций: , где — формулы, а — переменная.

Переменная называется связанной в формуле , если имеет вид либо , или же представима в одной из форм , причем уже связанна в , и . Если не связанна в , ее называют свободной в . Формулу без свободных переменных называют замкнутой формулой, или предложением. Теорией первого порядка называют любое множество предложений