Formuła logiczna

Z Wikipedii, wolnej encyklopedii
Skocz do: nawigacji, wyszukiwania

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

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

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

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

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

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

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