В математической логике атомарная формула (также известная как атом или простая формула ) — это формула без более глубокой пропозициональной структуры, то есть формула, не содержащая логических связок , или, что то же самое, формула, не имеющая строгих подформул . Таким образом, атомы представляют собой простейшие , правильно построенные формулы логики. Сложные формулы образуются путем объединения атомарных формул с помощью логических связок.
Точная форма атомарных формул зависит от рассматриваемой логики; например, для логики высказываний пропозициональную переменную часто кратко называют «атомарной формулой», но, точнее, пропозициональная переменная - это не атомарная формула, а формальное выражение, обозначающее атомарную формулу. Для логики предикатов атомы представляют собой символы-предикаты вместе со своими аргументами, причем каждый аргумент является термином . В теории моделей атомарные формулы представляют собой просто строки символов с заданной сигнатурой , которая может быть или не быть выполнимой в отношении данной модели. [1]
Правильно сформированные термины и предложения обычной логики первого порядка имеют следующий синтаксис :
Условия :
то есть термин рекурсивно определяется как константа c (именованный объект из области дискурса ), или переменная x (действующая по объектам в области дискурса), или n -арная функция f , аргументы которой равны термины т к . Функции отображают кортежи объектов в объекты.
Предложения:
то есть предложение рекурсивно определяется как n -арный предикат P , аргументами которого являются термины t k , или выражение, состоящее из логических связок (и, или) и кванторов (для всех существует), используемых с другими предложениями. .
Атомная формула или атом — это просто предикат, применяемый к кортежу термов; то есть атомарная формула — это формула вида P ( t 1 ,…, t n ) для P — предиката и членов t n .
Все остальные корректные формулы получаются путем составления атомов логическими связками и кванторами.
Например, формула ∀ x. п ( Икс ) ∧ ∃ у. Q ( y , ж ( Икс )) ∨ ∃ z. R ( z ) содержит атомы
Поскольку в атомарной формуле нет кванторов, все вхождения переменных символов в атомарной формуле свободны. [2]