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

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

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

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

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

Терм:

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

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

Твердження:

$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,$

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

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

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

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

$P(x)$ ,
$Q(y,f(x))$ ,
$R(z)$ .

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

Див. також

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

Примітки

↑ W. Hodges (1997). A Shorter Model Theory. Cambridge University Press, pp. 11–14. ISBN 0-521-58713-1.
↑ W. V. O. Quine (1981). Mathematical Logic. Harvard University Press, p. 161. ISBN 0-674-55451-5.

Додаткова література

P. Hinman (2005). Fundamentals of Mathematical Logic. A K Peters, ISBN 1-56881-262-0.

[hodges1997-1] W. Hodges (1997). A Shorter Model Theory. Cambridge University Press, pp. 11–14. ISBN 0-521-58713-1.

[quine1981-2] W. V. O. Quine (1981). Mathematical Logic. Harvard University Press, p. 161. ISBN 0-674-55451-5.

[1]

[2]