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