Web - Amazon

We provide Linux to the World


We support WINRAR [What is this] - [Download .exe file(s) for Windows]

CLASSICISTRANIERI HOME PAGE - YOUTUBE CHANNEL
SITEMAP
Audiobooks by Valerio Di Stefano: Single Download - Complete Download [TAR] [WIM] [ZIP] [RAR] - Alphabetical Download  [TAR] [WIM] [ZIP] [RAR] - Download Instructions

Make a donation: IBAN: IT36M0708677020000000008016 - BIC/SWIFT:  ICRAITRRU60 - VALERIO DI STEFANO or
Privacy Policy Cookie Policy Terms and Conditions
Formuła logiczna - Wikipedia, wolna encyklopedia

Formuła logiczna

Z Wikipedii

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

Spis treści

[edytuj] Rachunek zdań

Zdania rachunku zdań są formułami tegoż rachunku. Tak więc, każda zmienna zdaniowa pi jest formułą. Taką formułę nazywa się literałem lub formułą atomową. Formułami są także negacje formuł atomowych, tzn \neg p_i. 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łą.

[edytuj] 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ę.

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

[edytuj] Formalna definicja

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 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 t1 = t2 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 xi jest zmienną oraz \varphi jest formułą, to także (\exists x_i)(\varphi) i (\forall x_i)(\varphi) są formułami.

[edytuj] Zmienne wolne w formule

W formułach postaci (\exists x_i)(\varphi) i (\forall x_i)(\varphi) mówimy że zmienna xi 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 xi w \varphi (i mówimy że konkretne wystąpienie zmiennej jest wolne lub związane). Bardziej precyzyjnie:

  • każde wystąpienie zmiennej xi w formule atomowej jest wolne,
  • jeśli ψ to formuła postaci (Qxi)(φ), to każde wystąpienie zmiennej xi w formule ψ jest związane,
  • jeśli \psi,\varphi to formuły i pewne wystąpienie zmiennej xi w formule ψ 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).

[edytuj] 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),

[edytuj] Zobacz też

Our "Network":

Project Gutenberg
https://gutenberg.classicistranieri.com

Encyclopaedia Britannica 1911
https://encyclopaediabritannica.classicistranieri.com

Librivox Audiobooks
https://librivox.classicistranieri.com

Linux Distributions
https://old.classicistranieri.com

Magnatune (MP3 Music)
https://magnatune.classicistranieri.com

Static Wikipedia (June 2008)
https://wikipedia.classicistranieri.com

Static Wikipedia (March 2008)
https://wikipedia2007.classicistranieri.com/mar2008/

Static Wikipedia (2007)
https://wikipedia2007.classicistranieri.com

Static Wikipedia (2006)
https://wikipedia2006.classicistranieri.com

Liber Liber
https://liberliber.classicistranieri.com

ZIM Files for Kiwix
https://zim.classicistranieri.com


Other Websites:

Bach - Goldberg Variations
https://www.goldbergvariations.org

Lazarillo de Tormes
https://www.lazarillodetormes.org

Madame Bovary
https://www.madamebovary.org

Il Fu Mattia Pascal
https://www.mattiapascal.it

The Voice in the Desert
https://www.thevoiceinthedesert.org

Confessione d'un amore fascista
https://www.amorefascista.it

Malinverno
https://www.malinverno.org

Debito formativo
https://www.debitoformativo.it

Adina Spire
https://www.adinaspire.com