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ń[edytuj | edytuj kod]

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

Rachunek kwantyfikatorów[edytuj | edytuj kod]

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 ${\mathcal {L}}(\tau )$ są zdefiniowane jako elementy najmniejszego zbioru $\mathbf {T}$ takiego, że:

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

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

$t_{1}=t_{2}$ gdzie $t_{1},t_{2}\in \mathbf {T} ,$ oraz
$P(t_{1},\dots ,t_{n})$ gdzie $t_{1},\dots ,t_{n}\in \mathbf {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ż[edytuj | edytuj kod]