Formuła atomowa (formuła prosta) – formuła, która nie ma żadnych właściwych podformuł. Rodzaje formuł atomowych zależą od rodzaju używanej logiki.
Formuły, które nie są atomowe nazywamy złożonymi.
W rachunku zdań jedynymi rodzajami atomów są zmienne zdaniowe:
W klasycznym rachunku predykatów (logice pierwszego rzędu) określamy formuły atomowe w następujący sposób:
Niech
będzie ustalonym alfabetem (tzn. zbiorem stałych, symboli funkcyjnych i symboli relacyjnych) i niech
będzie (nieskończoną) listą używanych zmiennych. Przypomnijmy, że termy języka
są zdefiniowane jako elementy najmniejszego zbioru
takiego, że:
- wszystkie stałe i zmienne należą do
![{\displaystyle \mathbf {T} ,}](https://wikimedia.org/api/rest_v1/media/math/render/svg/54d82d074d2fb67c09a19856005276cb16c4fbe5)
- jeśli
i
jest
-arnym symbolem funkcyjnym, to ![{\displaystyle f(t_{1},\dots ,t_{n})\in \mathbf {T} .}](https://wikimedia.org/api/rest_v1/media/math/render/svg/262d4f36f40cf4e41451864cb8fee64860c9047a)
Formuły atomowe języka
to wyrażenia
gdzie
oraz
gdzie
zaś
jest
-arnym symbolem relacyjnym.
- Przykłady
- Rozważmy język
teorii mnogości (czyli
jest binarnym symbolem relacyjnym). Formuły atomowe w tym języku to fomuły postaci
oraz ![{\displaystyle x_{i}\in x_{j}.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d0084ecf4be002041489c08aa835288364987a68)
- Przykładami formuł atomowych w języku
teorii grup (czyli
jest binarnym symbolem funkcyjnym) są:
![{\displaystyle x_{1}*x_{1}=x_{1},}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1a3bdcd1f410bfb605b10a78b3036862f5965c85)
![{\displaystyle x_{1}*x_{2}=x_{2}*x_{1},}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f3d954760f9171f298f2b04fa04a7a79df3e1f0c)
![{\displaystyle (x_{1}*x_{2})*x_{3}=x_{1}*(x_{2}*x_{3}).}](https://wikimedia.org/api/rest_v1/media/math/render/svg/936849892c78dc50538ecc43df45c2895d332074)
- Rozważmy teraz język
ciał uporządkowanych (zatem
są binarnymi symbolami funkcyjnymi, a
jest binarnym symbolem relacyjnym). Następujące wyrażenia są formułami atomowymi w tym języku:
![{\displaystyle 0\leqslant x_{1}\cdot x_{1},}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6447b7498fa27885e643e9d1c02bcb9119c3e0b8)
![{\displaystyle x_{1}+x_{2}=x_{2}\cdot x_{1},}](https://wikimedia.org/api/rest_v1/media/math/render/svg/bdbe40b96913d02ba900a8a179a01bdd04f4481b)
![{\displaystyle x_{1}\leqslant (x_{1}+x_{2})\cdot (x_{2}+1).}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e637b29b2bee7e4e614a5b2f8b41ddea431b3719)