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 jest formułą. Taką formułę nazywa się też formułą atomową. Formułami są także negacje formuł atomowych, tzn. Formuły atomowe i ich negacje nazywa się też literałami. Ponadto jeżeli są formułami i jest binarnym spójnikiem zdaniowym (alternatywą koniunkcją implikacją lub równoważnością ), to oraz 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: nie jest formułą (formułą byłoby np. wyrażenie 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 jest formułą rachunku kwantyfikatorów, to oraz są nią również.

Niech 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 będzie nieskończoną listą zmiennych.

Przypomnijmy, że termy języka to elementy najmniejszego zbioru takiego, że:

• wszystkie stałe i zmienne należą do
• jeśli i jest -arnym symbolem funkcyjnym, to

Formuły języka są wprowadzane przez indukcję po ich złożoności jak następuje:

• jeśli to wyrażenie jest formułą (tzw. formuła atomową),
• jeśli zaś jest -arnym symbolem relacyjnym, to wyrażenie jest formułą (tzw. formuła atomową),
• jeśli są formułami oraz jest binarnym spójnikiem zdaniowym, to oraz są formułami,
• jeśli jest zmienną oraz jest formułą, to także i są formułami.

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

• każde wystąpienie zmiennej w formule atomowej jest wolne,
• jeśli to formuła postaci to każde wystąpienie zmiennej w formule jest związane,
• jeśli to formuły i pewne wystąpienie zmiennej w formule jest związane (wolne, odpowiednio), to wystąpienie to rozważane w formułach oraz 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 formuły nazywamy formułę

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 teorii mnogości (czyli jest binarnym symbolem relacyjnym) są:

• Przykładami formuł języka teorii grup (czyli jest binarnym symbolem funkcyjnym) są:

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