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

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

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: ${\displaystyle (p\vee q\vee r)}$ nie jest formułą (formułą byłoby np. wyrażenie ${\displaystyle ((p\vee q)\vee r),}$ lecz interpretacja takiej formuły jest jednoznaczna i wewnętrzne nawiasy w praktyce pomija się).

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 ${\displaystyle \varphi }$ jest formułą rachunku kwantyfikatorów, to ${\displaystyle \forall x\varphi }$ oraz ${\displaystyle \exists x\varphi }$ są nią również.

Niech ${\displaystyle \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 ${\displaystyle x_{0},x_{1},\dots }$ będzie nieskończoną listą zmiennych.

Przypomnijmy, że termy języka ${\displaystyle {\mathcal {L}}(\tau )}$ to elementy najmniejszego zbioru ${\displaystyle \mathbf {T} }$ takiego, że:

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

Formuły języka ${\displaystyle {\mathcal {L}}(\tau )}$ są wprowadzane przez indukcję po ich złożoności jak następuje:

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

W formułach postaci ${\displaystyle (\exists x_{i})(\varphi )}$ i ${\displaystyle (\forall x_{i})(\varphi )}$ mówimy, że zmienna ${\displaystyle 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 ${\displaystyle (\exists x_{i})(\varphi )}$ czy też ${\displaystyle (\forall x_{i})(\varphi )}$ pojawia się jako jedna z części użytych w budowie, ale ograniczamy się do występowań zmiennej ${\displaystyle x_{i}}$ w ${\displaystyle \varphi }$ (i mówimy, że konkretne wystąpienie zmiennej jest wolne lub związane). Bardziej precyzyjnie:

• każde wystąpienie zmiennej ${\displaystyle x_{i}}$ w formule atomowej jest wolne,
• jeśli ${\displaystyle \psi }$ to formuła postaci ${\displaystyle (Qx_{i})(\varphi ),}$ to każde wystąpienie zmiennej ${\displaystyle x_{i}}$ w formule ${\displaystyle \psi }$ jest związane,
• jeśli ${\displaystyle \psi ,\varphi }$ to formuły i pewne wystąpienie zmiennej ${\displaystyle x_{i}}$ w formule ${\displaystyle \psi }$ jest związane (wolne, odpowiednio), to wystąpienie to rozważane w formułach ${\displaystyle \varphi *\psi ,}$ ${\displaystyle \psi *\varphi }$ oraz ${\displaystyle \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 ${\displaystyle x_{1},\dots ,x_{n}}$ formuły ${\displaystyle \varphi }$ nazywamy formułę ${\displaystyle \forall x_{1}\ldots \forall x_{n}\varphi .}$

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 ${\displaystyle {\mathcal {L}}(\{\in \})}$ teorii mnogości (czyli ${\displaystyle \in }$ jest binarnym symbolem relacyjnym) są:

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

${\displaystyle \exists P\forall Z(Z\in P\iff \forall x(x\in Z\Rightarrow x\in X))}$

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

${\displaystyle (\forall x_{1}\in G)((x_{1}\star x_{2})\star x_{3}=x_{1}\star (x_{2}\star x_{3})),}$

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

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

• dysjunkcyjna postać normalna
• koniunkcyjna postać normalna
• logika
• prawa De Morgana