Formuła logiczna

Formuła logiczna – 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 $\varphi$ jest formułą rachunku kwantyfikatorów, to $\forall x\varphi$ oraz $\exists x\varphi$ 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},\dots$ będzie nieskończoną listą zmiennych.

Przypomnijmy, że termy języka ${\mathcal {L}}(\tau )$ to 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 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 \mathbf {T} ,$ to wyrażenie $t_{1}=t_{2}$ jest formułą (tzw. formuła atomową),
jeśli $t_{1},\dots ,t_{n}\in \mathbf {T}$ zaś $P\in \tau$ jest $n$ -arnym symbolem relacyjnym, to wyrażenie $P(t_{1},\dots ,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})(\varphi ),$ 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},\dots ,x_{n}$ formuły $\varphi$ nazywamy formułę $\forall x_{1}\ldots \forall x_{n}\varphi .$