Formuła logiczna

Formuła logiczna to określenie dozwolonego wyrażenia w wielu systemach logicznych, m.in. w rachunku kwantyfikatorów oraz w rachunku zdań.

Rachunek zdań

Zdania rachunku zdań są formułami tegoż rachunku. Tak więc, każda zmienna zdaniowa $p_i$ jest formułą. Taką formułę nazywa się też formułą atomową. Formułami są także negacje formuł atomowych, tzn. $\neg p_i$. Formuły atomowe i ich negacje nazywa się też literałami. Ponadto, jeżeli $\varphi,\psi$ są formułami i $*$ jest binarnym spójnikiem zdaniowym (alternatywą $\vee$, koniunkcją $\wedge$, implikacją $\Rightarrow$ lub równoważnością $\Leftrightarrow$), to $(\varphi*\psi)$ oraz $\neg \varphi$ są formułami. Żadne inne wyrażenie nie może być formułą.

Przykłady

Wbrew definicji formalnej, w sytuacjach, gdy nie prowadzi to do nieporozumień, część nawiasów w formule opuszcza się. Przykładowo, zgodnie z definicją formalną wyrażenie :$(p \vee q \vee r)$ nie jest formułą (formułą byłoby np. wyrażenie $((p \vee q) \vee r))$, lecz interpretacja takiej formuły jest jednoznaczna i wewnętrzne nawiasy w praktyce pomija się.

Rachunek kwantyfikatorów

Rachunek kwantyfikatorów (rachunek predykatów pierwszego rzędu), jako uogólnienie rachunku zdań, posługuje się podobną definicją formalną formuły, rozszerzając ją o kwantyfikatory - jeżeli φ jest formułą rachunku kwantyfikatorów, to $\forall x \phi$ oraz $\exist x \phi$ są nią również.

Formalna definicja

Niech $\tau$ będzie ustalonym alfabetem, czyli zbiorem stałych, symboli funkcyjnych i symboli relacyjnych (predykatów). Każdy z tych symboli ma jednoznacznie określony charakter (tzn wiadomo czy jest to stała, czy symbol funkcyjny czy też predykat) i każdy z symboli funkcyjnych i predykatów ma określoną arność (która jest dodatnią liczbą całkowitą). Niech $x_0,x_1,\ldots$ będzie nieskończoną listą zmiennych.

Przypomnijmy, że termy języka ${\mathcal L}(\tau)$ to 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 języka ${\mathcal L}(\tau)$ są wprowadzane przez indukcję po ich złożoności jak następuje:

• jeśli $t_1, t_2\in {\bold T}$, to wyrażenie $t_1= t_2$ jest formułą (tzw formuła atomową),
• jeśli $t_1,\ldots,t_n\in {\bold T}$ zaś $P\in\tau$ jest $n$-arnym symbolem relacyjnym, to wyrażenie $P(t_1,\ldots,t_n)$ jest formułą (tzw formuła atomową),
• jeśli $\varphi,\psi$ są formułami oraz $*$ jest binarnym spójnikiem zdaniowym, to $(\varphi*\psi)$ oraz $\neg \varphi$ są formułami,
• jeśli $x_i$ jest zmienną oraz $\varphi$ jest formułą, to także $(\exists x_i)(\varphi)$ i $(\forall x_i)(\varphi)$ są formułami.

Zmienne wolne w formule

W formułach postaci $(\exists x_i)(\varphi)$ i $(\forall x_i)(\varphi)$ mówimy że zmienna $x_i$ znajduje się w zasięgu kwantyfikatora i jako taka jest związana. Przez indukcję po złożoności formuł, rozszerzamy to pojęcie na wszystkie formuły w których $(\exists x_i)(\varphi)$ czy też $(\forall x_i)(\varphi)$ pojawia się jako jedna z części użytych w budowie, ale ograniczamy się do występowań zmiennej $x_i$ w $\varphi$ (i mówimy że konkretne wystąpienie zmiennej jest wolne lub związane). Bardziej precyzyjnie:

• każde wystąpienie zmiennej $x_i$ w formule atomowej jest wolne,
• jeśli $\psi$ to formuła postaci $(Qx_i)(\phi)$, to każde wystąpienie zmiennej $x_i$ w formule $\psi$ jest związane,
• jeśli $\psi,\varphi$ to formuły i pewne wystąpienie zmiennej $x_i$ w formule $\psi$ jest związane (wolne, odpowiednio), to wystąpienie to rozważane w formułach $\varphi*\psi$, $\psi*\varphi$ oraz $\neg \psi$ także jest związane (wolne, odpowiednio; tutaj * jest binarnym spójnikiem zdaniowym).

Formuły w których nie ma wolnych występowań żadnych zmiennych są nazywane zdaniami (danego języka).

Domknięciem (lub domknięciem ogólnym) względem zmiennych $x_1,\ldots,x_n$ formuły $\phi$ nazywamy formułę $\forall x_1\ldots\forall x_n \phi$.

Przykłady

W praktyce, podobnie jak w rachunku zdań, gdy nie prowadzi to do niejasności, stosuje się zasadę opuszczania nawiasów.

• Przykładami formuł języka ${\mathcal L}(\{\in\})$ teorii mnogości (czyli $\in$ jest binarnym symbolem relacyjnym) są:

$\forall A \forall B (\forall x (x\in A\iff x\in B)\Rightarrow A=B)$

$\exist P \forall Z (Z\in P \iff \forall x (x\in Z \Rightarrow x\in X))$

• Przykładami formuł języka ${\mathcal L}(\{\star\})$ teorii grup (czyli $\star$ jest binarnym symbolem funkcyjnym) są:

$(\forall x_1\in G)((x_1 \star x_2) \star x_3 = x_1 \star (x_2 \star x_3))$,

$(\exists e \in G) (\forall a \in G)(e \star a = a)$,

$(\forall a \in G)(\exists b \in G)(b \star a = e)$,

Zobacz też

• Koniunktywna postać normalna
• Dysjunktywna postać normalna
• Prawa De Morgana
• Logika