В математической логике основным термином формальной системы является термин , не содержащий никаких переменных . Точно так же основная формула — это формула , не содержащая переменных.
В логике первого порядка с тождеством предложение Q ( a ) ∨ P ( b ) является основной формулой, где a и b являются постоянными символами. Основное выражение — это основной термин или основная формула.
Рассмотрим следующие выражения в логике первого порядка над сигнатурой , содержащей постоянный символ 0 для числа 0, символ унарной функции s для функции-преемника и символ двоичной функции + для сложения.
Далее следует формальное определение языков первого порядка . Пусть дан язык первого порядка, где C — множество постоянных символов, V — множество (индивидуальных) переменных, F — множество функциональных операторов и P — множество предикатных символов .
Основные термины — это термины , не содержащие переменных. Они могут быть определены логической рекурсией (формула-рекурсия):
Предикат основания , атом основания или литерал основания — это атомарная формула , все члены аргумента которой являются основными членами.