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.

Rachunek zdań

W rachunku zdań jedynymi rodzajami atomów są zmienne zdaniowe: ${\displaystyle p,q,r,\dots }$

Rachunek kwantyfikatorów

W klasycznym rachunku predykatów (logice pierwszego rzędu) określamy formuły atomowe w następujący sposób:

Niech ${\displaystyle \tau }$ będzie ustalonym alfabetem (tzn. zbiorem stałych, symboli funkcyjnych i symboli relacyjnych) i niech ${\displaystyle x_{0},x_{1},\dots }$ będzie (nieskończoną) listą używanych zmiennych. Przypomnijmy, że termy języka ${\displaystyle {\mathcal {L}}(\tau )}$ są zdefiniowane jako elementy najmniejszego zbioru ${\displaystyle \mathbf {T} }$ takiego, że:

• wszystkie stałe i zmienne należą do ${\displaystyle \mathbf {T} ,}$
• jeśli ${\displaystyle t_{1},\dots ,t_{n}\in \mathbf {T} }$ i ${\displaystyle f\in \tau }$ jest ${\displaystyle n}$-arnym symbolem funkcyjnym, to ${\displaystyle f(t_{1},\dots ,t_{n})\in \mathbf {T} .}$

Formuły atomowe języka ${\displaystyle {\mathcal {L}}(\tau )}$ to wyrażenia

• ${\displaystyle t_{1}=t_{2}}$ gdzie ${\displaystyle t_{1},t_{2}\in \mathbf {T} ,}$ oraz
• ${\displaystyle P(t_{1},\dots ,t_{n})}$ gdzie ${\displaystyle t_{1},\dots ,t_{n}\in \mathbf {T} }$ zaś ${\displaystyle P\in \tau }$ jest ${\displaystyle n}$-arnym symbolem relacyjnym.

Przykłady

• Rozważmy język ${\displaystyle {\mathcal {L}}(\{\in \})}$ teorii mnogości (czyli ${\displaystyle \in }$ jest binarnym symbolem relacyjnym). Formuły atomowe w tym języku to fomuły postaci ${\displaystyle x_{i}=x_{j}}$ oraz ${\displaystyle x_{i}\in x_{j}.}$
• Przykładami formuł atomowych w języku ${\displaystyle {\mathcal {L}}(\{*\})}$ teorii grup (czyli ${\displaystyle *}$ jest binarnym symbolem funkcyjnym) są:

${\displaystyle x_{1}*x_{1}=x_{1},}$

${\displaystyle x_{1}*x_{2}=x_{2}*x_{1},}$

${\displaystyle (x_{1}*x_{2})*x_{3}=x_{1}*(x_{2}*x_{3}).}$

• Rozważmy teraz język ${\displaystyle {\mathcal {L}}(\{+,\cdot ,0,1,\leqslant \})}$ ciał uporządkowanych (zatem ${\displaystyle +,\cdot }$ są binarnymi symbolami funkcyjnymi, a ${\displaystyle \leqslant }$ 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},}$

${\displaystyle x_{1}+x_{2}=x_{2}\cdot x_{1},}$

${\displaystyle x_{1}\leqslant (x_{1}+x_{2})\cdot (x_{2}+1).}$

Zobacz też

• forma preneksowa
• funktor zdaniotwórczy
• koniunkcyjna postać normalna