Dobrze uformowana formuła - Well-formed formula

W logice matematycznej , zdań logicznych i bazowego logiki , A dobrze uformowane wzór , w skrócie WFF lub WFF , często po prostu wzór jest skończoną sekwencję z symboli z danego alfabetu , który jest częścią formalnej języka . Język formalny można utożsamić ze zbiorem formuł w języku.

Formuła to obiekt składniowy, któremu można nadać znaczenie semantyczne za pomocą interpretacji. Dwa kluczowe zastosowania formuł to logika zdań i logika predykatów.

Wprowadzenie

Kluczowym zastosowaniem formuł jest logika zdań i logika predykatów, taka jak logika pierwszego rzędu . W tych kontekstach formuła jest ciągiem symboli φ, dla których sensowne jest pytanie „czy φ prawda?”, Po utworzeniu wystąpienia dowolnych wolnych zmiennych w φ. W logice formalnej dowody można przedstawić za pomocą ciągów formuł o określonych właściwościach, a ostateczna formuła w sekwencji jest tym, co zostało udowodnione.

Chociaż termin „wzór” może być używany do oznaczeń pisanych (na przykład na kartce papieru lub tablicy), jest on bardziej precyzyjnie rozumiany jako sekwencja wyrażanych symboli, przy czym znaki są symbolicznym przykładem wzoru. Zatem ta sama formuła może być zapisana więcej niż raz, a formuła mogłaby w zasadzie być tak długa, że ​​nie można jej w ogóle zapisać w fizycznym wszechświecie.

Same formuły są obiektami syntaktycznymi. Nadaje im się znaczenie poprzez interpretacje. Na przykład w formule zdaniowej każda zmienna zdaniowa może być interpretowana jako zdanie konkretne, tak że ogólna formuła wyraża związek między tymi zdaniami. Nie trzeba jednak interpretować wzoru, aby traktować go wyłącznie jako wzór.

Rachunek zdań

Formuły rachunku zdań , zwane także formułami zdań , to wyrażenia takie jak . Ich definicja rozpoczyna się od arbitralnego wyboru wyznaczonej V o zmiennych zdaniowych . Alfabet składa się z liter V, wraz z symboli dla zdaniotwórczych i nawiasach „(” i „)”, z których wszystkie są przejmowane nie być w V . Formuły będą określonymi wyrażeniami (czyli ciągami symboli) nad tym alfabetem.

Wzory są indukcyjnie zdefiniowane w następujący sposób:

  • Każda zmienna zdaniowa jest sama w sobie formułą.
  • Jeśli φ jest formułą, to ¬φ jest formułą.
  • Jeśli φ i ψ są formułami, a • jest dowolnym łącznikiem binarnym, to (φ • ψ) jest formułą. Tutaj • mogą być (ale nie tylko) zwykłe operatory ∨, ∧, → lub ↔.

Definicję tę można również zapisać jako gramatykę formalną w formie Backusa – Naura , pod warunkiem, że zbiór zmiennych jest skończony:

<alpha set> ::= p | q | r | s | t | u | ... (the arbitrary finite set of propositional variables)
<form> ::= <alpha set> | ¬<form> | (<form><form>) | (<form><form>) | (<form><form>) | (<form><form>)

Używając tej gramatyki, sekwencja symboli

((( p q ) ∧ ( r s )) ∨ (¬ q ∧ ¬ s ))

jest formułą, ponieważ jest poprawna gramatycznie. Sekwencja symboli

(( p q ) → ( qq )) p ))

nie jest formułą, ponieważ nie jest zgodna z gramatyką.

Złożony wzór może być trudny do odczytania, na przykład z powodu mnożenia nawiasów. Aby złagodzić to ostatnie zjawisko, wśród operatorów przyjęto reguły pierwszeństwa (podobne do standardowej matematycznej kolejności operacji ), dzięki czemu niektóre operatory są bardziej wiążące niż inne. Na przykład zakładając pierwszeństwo (od najbardziej do najmniej wiążącego) 1. ¬ 2. → 3. ∧ 4. ∨. Następnie formuła

((( p q ) ∧ ( r s )) ∨ (¬ q ∧ ¬ s ))

można skrócić jako

p q r s ∨ ¬ q ∧ ¬ s

Jest to jednak tylko konwencja stosowana w celu uproszczenia pisemnej reprezentacji wzoru. Jeśli założono by pierwszeństwo, na przykład, jako asocjacyjne lewo-prawo, w następującej kolejności: 1. ¬ 2. ∧ 3. ∨ 4. →, to ten sam wzór powyżej (bez nawiasów) zostałby przepisany jako

( p → ( q r )) → ( s ∨ ((¬ q ) ∧ (¬ s )))

Logika predykatów

Definicja formuły w logice pierwszego rzędu zależy od sygnatury danej teorii. Podpis ten określa stałe symbole, symbole predykatów i symbole funkcyjne omawianej teorii, wraz z arencjami symboli funkcji i predykatów.

Definicja wzoru składa się z kilku części. Po pierwsze, zestaw terminów jest definiowany rekurencyjnie. Terminy nieformalnie są wyrażeniami, które reprezentują przedmioty z domeny dyskursu .

  1. Każda zmienna jest terminem.
  2. Każdy stały symbol z podpisu jest terminem
  3. wyrażenie postaci f ( t 1 ,…, t n ), gdzie f jest n -arnym symbolem funkcji, a t 1 ,…, t n są terminami, jest znowu terminem.

Następnym krokiem jest zdefiniowanie wzorów atomowych .

  1. Jeżeli T 1 i T 2 są terminami następnie T 1 = T 2 jest wzór atomowy
  2. Jeśli R jest n -arnym symbolem predykatu, a t 1 ,…, t n są terminami, to R ( t 1 ,…, t n ) jest formułą atomową

Ostatecznie zbiór formuł jest zdefiniowany jako najmniejszy zbiór zawierający zbiór formuł atomowych, który spełnia następujące warunki:

  1. jest formułą, kiedy jest formułą
  2. i są formułami, kiedy i są formułami;
  3. jest formułą, gdy jest zmienną i jest formułą;
  4. jest formułą, gdy jest zmienną i jest formułą (alternatywnie można ją zdefiniować jako skrót dla ).

Jeśli formuła nie występuje ani dla żadnej zmiennej , wówczas nazywa się ją wolną od kwantyfikatorów . Egzystencjalny wzór jest wzorem wychodząc z sekwencji ilościowego egzystencji następnie wzorze kwantyfikatora wolne.

Formuły atomowe i otwarte

Wzór atomowa jest preparatem, który zawiera nie spójników logicznych ani kwantyfikatorów lub równoważnie formułę, która nie ma określonych subformulas. Dokładna postać formuł atomowych zależy od rozważanego systemu formalnego; dla logiki zdań , na przykład, formuły atomowe są zmiennymi zdań . W przypadku logiki predykatów atomy są symbolami predykatów wraz z ich argumentami, przy czym każdy argument jest terminem .

Według pewnej terminologii formuła otwarta jest tworzona przez łączenie formuł atomowych przy użyciu tylko logicznych łączników, z wyłączeniem kwantyfikatorów. Nie należy tego mylić z formułą, która nie jest zamknięta.

Formuły zamknięte

Zamknięta formuła , również mielone formuła lub zdanie , to formuła, w której nie istnieją darmowe wystąpienia jakiejkolwiek zmiennej . Jeśli jest wzorem języka pierwszego rzędu, w którym zmienne v 1 , ..., v n mają wolne zdarzenia, następnie poprzedzone V 1v n jest zamknięcie A .

Właściwości mające zastosowanie do wzorów

  • Formuła w języku jest ważny , jeśli jest prawdziwa dla każdej interpretacji z dnia .
  • Formuła w języku jest spełnialna jeśli prawdą jest, dla niektórych interpretacji z dnia .
  • Formuła A języka arytmetyki jest rozstrzygalna, jeśli reprezentuje zbiór rozstrzygalny , tj. Jeśli istnieje skuteczna metoda, która po zastąpieniu wolnych zmiennych A mówi, że albo wynikowy przypadek A jest możliwy do udowodnienia, albo jego negacja jest .

Wykorzystanie terminologii

We wcześniejszych pracach nad logiką matematyczną (np. Autorstwa Churcha ) formuły odnosiły się do dowolnych ciągów symboli, a wśród tych ciągów formuły dobrze uformowane były ciągami zgodnymi z regułami tworzenia (prawidłowych) formuł.

Kilku autorów po prostu podaje formułę. Współczesne zwyczaje (zwłaszcza w kontekście informatyki z oprogramowaniem matematycznym, takim jak weryfikatory modeli , automatyczne dowody twierdzeń , interaktywne dowody twierdzeń ) skłaniają się do zachowania pojęcia wzoru jedynie w koncepcji algebraicznej i pozostawiają kwestię poprawności , tj. konkretna reprezentacja ciągów formuł (używanie tego lub innego symbolu dla łączników i kwantyfikatorów, używanie tej lub innej konwencji nawiasów , używanie notacji polskiej lub wrostkowej itp.) jako zwykły problem notacyjny.

Chociaż wyrażenie dobrze sformułowana formuła jest nadal w użyciu, autorzy ci niekoniecznie używają go w przeciwieństwie do starego sensu wzoru , który nie jest już powszechny w logice matematycznej.

Do kultury popularnej wkradło się również wyrażenie „dobrze sformułowane formuły” (WFF). WFF jest częścią ezoterycznej gry słów używanej w nazwie gry akademickiej „ WFF 'N PROOF : The Game of Modern Logic” autorstwa Laymana Allena, opracowanej, gdy był w Yale Law School (był później profesorem na Uniwersytecie Michigan ). Zestaw gier ma na celu nauczenie dzieci zasad logiki symbolicznej (w notacji polskiej ). Jego nazwa jest echem whiffenpoof , nonsensownego słowa używanego jako okrzyk na Uniwersytecie Yale, spopularyzowanego w The Whiffenpoof Song i The Whiffenpoofs .

Zobacz też

Uwagi

Bibliografia

Zewnętrzne linki