Атомарна формула

У математичній логіці, атомарна формула (або атом, елементарна формула) — це формула, яка не має додаткових тверджень пропозицій, тобто вона не містить логічних сполучників або, інакше кажучи, не має строгих підформул. Таким чином, атом є найпростішою правильно побудованою формулою^[en] математичної логіки. Використання логічних сполучників для поєднання атомних формул створює складні формули.

Точна форма атомарних формул залежить від логіки, що розглядається; для числення висловлювань, наприклад, змінну тверджень^[en] часто можуть називати «атомарною формулою», але, точніше кажучи, змінна тверджень не є атомарною формулою, а є формальним виразом, що позначає атомарну формулу. Для логіки предикатів, атомами є символи предикатів разом з їхніми аргументами, де кожен аргумент є термом. В теорії моделей, атомарні формули — це просто рядки символів із заданою сигнатурою, які можуть бути або не бути виконуваними^[en] відносно заданої моделі.^[1]

Атомарна формула в логіці першого порядку

Правильно побудовані терми та твердження звичайної логіки першого порядку мають такий синтаксис:

Терм:

• ${\displaystyle t\equiv c\;\mid \;x\;\mid \;f(t_{1},\dots ,t_{n}),}$

тобто терм рекурсивно визначається як константа ${\displaystyle c}$ (іменований об'єкт з області визначення), або змінна ${\displaystyle x}$ (що пробігає об'єкти в області визначення), або ${\displaystyle n}$-арна функція ${\displaystyle f}$, аргументами якої є терми ${\displaystyle f_{k}}$. Функції відображають кортежі об'єктів в об'єкти.

Твердження:

• ${\displaystyle A,B,\dots \;\equiv \;P(t_{1},\dots ,t_{n})\;\mid \;A\wedge B\;\mid \;\top \;\mid \;A\vee B\;\mid \;\bot \;\mid \;A\supset B\;\mid \;\forall x\,A\;\mid \;\exists x\,A,}$

тобто твердження рекурсивно визначається як ${\displaystyle n}$-арний предикат ${\displaystyle P}$, аргументами якого є терми ${\displaystyle t_{k}}$, або вираз, складений з логічних сполучників (і, або) та кванторів (для всіх, існує), що використовуються з іншими твердженнями.

Атомарна формула або атом — це просто предикат, застосований до кортежу термів; тобто атомарна формула має вигляд ${\displaystyle P(t_{1},\dotsc ,t_{n})}$, де ${\displaystyle P}$ — предикат, а ${\displaystyle t_{n}}$ — терми.

Усі інші правильно побудовані формули^[en] отримуються шляхом складання атомів за допомогою логічних зв'язок та кванторів.

Наприклад, формула ${\displaystyle \forall x\ P(x)\wedge \exists y\ Q(y,f(x))\vee \exists z\ R(z)}$ містить атоми:

• ${\displaystyle P(x)}$,
• ${\displaystyle Q(y,f(x))}$,
• ${\displaystyle R(z)}$.

Оскільки атомарна формула не може містити кварторів, то всі змінні в атомарних формулах є вільними змінними.^[2]

Див. також

• У теорії моделей структури надають інтерпретацію атомарним формулам.
• У теорії доведень призначення полярності для атомарних формул є важливим компонентом фокусування.
• Атомарне речення^[en].