Formuła atomowa

Formuła atomowa (formuła prosta) – w logice matematycznej 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: $p,q,r,\ldots$

Rachunek kwantyfikatorów

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

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

• wszystkie stałe i zmienne należą do ${\bold T}$,
• jeśli $t_1,\ldots,t_n\in {\bold T}$ i $f\in\tau$ jest $n$-arnym symbolem funkcyjnym, to $f(t_1,\ldots,t_n)\in {\bold T}$.

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

• $t_1= t_2$ gdzie $t_1, t_2\in {\bold T}$, oraz
• $P(t_1,\ldots,t_n)$ gdzie $t_1,\ldots,t_n\in {\bold T}$ zaś $P\in\tau$ jest $n$-arnym symbolem relacyjnym.

Przykłady

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

$x_1*x_1=x_1$,

$x_1*x_2=x_2*x_1$,

$(x_1*x_2)*x_3=x_1*(x_2*x_3)$.

• Rozważmy teraz język ${\mathcal L}(\{+,\cdot,0,1,\leqslant\})$ ciał uporządkowanych (zatem $+,\cdot$ są binarnymi symbolami funkcyjnymi, a $\leqslant$ jest binarnym symbolem relacyjnym). Następujące wyrażenia są formułami atomowymi w tym języku:

$0\leqslant x_1\cdot x_1$,

$x_1+x_2=x_2\cdot x_1$,

$x_1\leqslant (x_1+x_2)\cdot (x_2+1)$

Zobacz też

• Forma preneksowa
• Funktor zdaniotwórczy
• Koniunkcyjna postać normalna