Formuła atomowa

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: $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 $\tau$ będzie ustalonym alfabetem (tzn. zbiorem stałych, symboli funkcyjnych i symboli relacyjnych) i niech $x_0,x_1,\dots$ będzie (nieskończoną) listą używanych zmiennych. Przypomnijmy, że termy języka $ℒ(\tau )$ są zdefiniowane jako elementy najmniejszego zbioru $𝐓$ takiego, że:

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

Formuły atomowe języka $ℒ(\tau )$ to wyrażenia

• $t_1=t_2$ gdzie $t_1,t_2\in 𝐓,$ oraz
• $P(t_1,\dots ,t_n)$ gdzie $t_1,\dots ,t_n\in 𝐓$ zaś $P\in \tau$ jest $n$-arnym symbolem relacyjnym.

Przykłady

• Rozważmy język $ℒ(\{\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 $ℒ(\{*\})$ 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 $ℒ(\{+,\cdot ,0,1,⩽\})$ ciał uporządkowanych (zatem $+,\cdot$ są binarnymi symbolami funkcyjnymi, a $⩽$ jest binarnym symbolem relacyjnym). Następujące wyrażenia są formułami atomowymi w tym języku:

$0⩽x_1\cdot x_1,$

$x_1+x_2=x_2\cdot x_1,$

$x_1⩽(x_1+x_2)\cdot (x_2+1).$

Zobacz też

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