Основные определения

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

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

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

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

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

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

· — множество символов для отношений (предикатов),

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

· — множество символов констант

· и функция , сопоставляющая элементам и их арность.

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

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

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

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

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