System formalny - Polski Serwis Naukowy

System formalny – w logice i matematyce język formuł (logiki) wraz ze zbiorem reguł wyprowadzania (wywodu) i zwykle zbiorem aksjomatów. Systemy formalne są tworzone i badane zarówno jako samodzielne abstrakcyjne twory, jak i systemy opisu rzeczywistości.

W matematyce formalnie dowody twierdzeń konstruuje się w systemach formalnych zawierających aksjomaty oraz reguły dedukcji (wyprowadzania). Twierdzenia są wtedy „ostatnimi liniami” takich dowodów. Zbiór aksjomatów i wszystkich możliwych twierdzeń nazywa się domknięciem zbioru aksjomatów ze względu na wyprowadzanie. Takie podejście do matematyki nazywane jest formalizmem matematycznym. David Hilbert nazwał metamatematyką naukę badającą systemy formalne.

Metamatematyka lub meta-matematyka – matematyka zastosowana do badania matematyki. Bardziej ogólnie to refleksja o matematyce widzianej jako pewien abstrakcyjny obiekt i produkt ludzkiego umysłu.

Rozstrzygalność (decydowalność) problemu matematycznego to następująca jego właściwość: zawsze można określić czy dana odpowiedź na pytanie stawiane przez problem jest poprawna.

System formalny w matematyce zawiera następujące elementy:

Skończony zbiór symboli, z którego konstruowane są formuły.
Gramatykę opisującą jakie formuły są poprawnie skonstruowane i pozwalającą zweryfikować poprawność dowolnej formuły.
Zbiór aksjomatów, będących poprawnie skonstruowanymi formułami.
Zbiór reguł wyprowadzania.
Zbiór twierdzeń zawierający wszystkie aksjomaty oraz wszystkie poprawnie skonstruowane formuły, które da się wyprowadzić z aksjomatów za pomocą reguł wyprowadzania.

Należy pamiętać, że nawet jeżeli dana formuła jest poprawną formułą systemu, to nie oznacza to, że istnieje procedura decyzyjna określająca, czy jest ona twierdzeniem.

Operator konsekwencji - pojęcie wprowadzone do logiki przez Alfreda Tarskiego. Motywacją dla jego wprowadzenia była formalizacja pojęcia konsekwencji określonego zbioru przesłanek.

W logice matematycznej przez język rozumie się pewien zbiór symboli, przy użyciu których można tworzyć bardziej złożone wyrażenia (na przykład formuły, zdania) według ściśle określonych reguł syntaktycznych. Przyjmuje się, że w danym języku L mogą występować (w dowolnej ilości) symbole funkcyjne, relacyjne oraz symbole stałych. Zdania napisane przy użyciu języków tego typu wystarczają do opisu większości własności dowolnych struktur matematycznych oraz do wyrażenia twierdzeń mówiących o tych strukturach.

Definicja

Systemem formalnym (w zbiorze $E$ ) nazywamy trójkę $\langle E, R, A\rangle$ , gdzie $E$ jest dowolnym zbiorem, $A \subseteq E$ , a $R$ jest zbiorem reguł wnioskowania w $E$ . Elementy zbioru $E$ nazywa się wyrażeniami tego systemu, elementy zbioru $A$ nazywa – aksjomatami, a elementy zbioru $R$ – jego regułami.

System formalny jest finitarny, jeśli jego reguły są finitarne.

Aksjomat (postulat, pewnik; gr. αξιωμα aksíoma – godność, pewność, oczywistość) – jedno z podstawowych pojęć logiki matematycznej. Od czasów Euklidesa uznawano, że aksjomaty to zdania przyjmowane za prawdziwe, których nie dowodzi się w obrębie danej teorii matematycznej. We współczesnej matematyce definicja aksjomatu jest nieco inna:

Logika (gr. λόγος, logos - rozum) nauka normatywna, analizująca źródła poznania pod względem prawomocności czynności poznawczych z nimi związanych. Zajmuje się badaniem ogólnych praw, według których przebiegają wszelkie poprawne rozumowania, w szczególności wnioskowania. Logika, jako dyscyplina normatywna, nie tylko opisuje jak faktycznie przebiegają rozumowania, ale także formułuje twierdzenia normatywne, mówiące o tym, jak rozumowania powinny przebiegać.

Dowody

Niech $\mathfrak S = \langle E, R, A \rangle$ będzie systemem formalnym, $X \subseteq E$ oraz $e \in E$ .

Dowodem elementu $e$ ze zbiorem założeń $X$ w systemie $\mathfrak S$ jest ciąg $\langle e_1,\ldots,e_n\rangle$ elementów zbioru $S$ , dla którego:

$e = e_n$ ,

dla każdego $k = 1, \dots, n$ zachodzi przynajmniej jeden z warunków:

$e_k \in X \cup A$ ,

$\forall_{r \in R}\; \forall_{\Pi \subseteq \{1, \dots, k-1\}}\; \left(\langle \Pi, e_k \rangle \in r\right)$ .

Zbiór elementów mających w $\mathfrak S$ dowód ze zbiorem założeń $X$ oznacza się symbolem $\mathbf{Prv}_{\mathfrak S}(X)$ .

Przykłady dowodów w systemach formalnych wybranych rachunków zdaniowych można znaleźć tutaj i tutaj.

Operator konsekwencji - pojęcie wprowadzone do logiki przez Alfreda Tarskiego. Motywacją dla jego wprowadzenia była formalizacja pojęcia konsekwencji określonego zbioru przesłanek.

Zbiór (niegdyś mnogość, wielość) – jedno z fundamentalnych pojęć współczesnej matematyki, w teorii mnogości (teorii zbiorów) przyjmowane jako pojęcie pierwotne. Intuicyjnie: kolekcja, zestaw niepowtarzających się obiektów bez wyróżnionej kolejności nazywanych elementami.

Własności

$X \subseteq \mathbf{Prv}_{\mathfrak S}(X)$ .

$X \subseteq Y \Rightarrow \mathbf{Prv}_{\mathfrak S}(X) \subseteq \mathbf{Prv}_{\mathfrak S}(Y)$ .

$\mathbf{Prv}_{\mathfrak S}\big(\mathbf{Prv}_{\mathfrak S}(X)\big) = \mathbf{Prv}_{\mathfrak S}(X)$ .

Z własności tych wynika, że $\mathbf{Prv}$ jest operatorem domknięcia, co więcej, jest on finitarny: $e \in \mathbf{Prv}_{\mathfrak S}(X) \Leftrightarrow \forall_{X_0 \mbox{ -- skończony}}\; \left(X_0 \subseteq X,\; e \in \mathbf{Prv}_{\mathfrak S}(X_0)\right)$ .

Zakres wnioskowania

Mając dany zbiór „założeń” $X$ chciałoby się znać wszystkie „fakty” $e$ ze zbioru $E$ , które można wywnioskować ze zbioru $X$ . Niestety okazuje się, że zbiory $\mathbf{Prv}_{\mathfrak S}(X)$ nie zawsze zawierają wszystkie „wnioski”.

Otóż, niech

W logice matematycznej teorią nazywamy niesprzeczny zbiór zdań. Dokładniej, niech T będzie zbiorem zdań zapisanych w pewnym języku L. Wtedy T jest teorią, jeśli nie istnieje zdanie napisane w języku L takie że T dowodzi zarówno tego zdania, jak i jego zaprzeczenia. Zbiór zdań T dowodzi zdania X, jeśli można przeprowadzić formalny dowód zdania X przy użyciu zdań ze zbioru T oraz aksjomatów i reguł dowodzenia klasycznego rachunku logicznego.

Intuicjonistyczny rachunek zdań, INT, w wersji inwariantnej — rachunek zdaniowy w języku klasycznego rachunku zdań z regułą odrywania jako jedyną pierwotną regułą wnioskowania oraz aksjomatami następującej postaci:

$E = \{0, 1, 2, \dots\}$ i $R = \{r, r_\omega\}$ ,

gdzie $r = \left\{\langle \{n\}, n+1 \rangle\colon n \in \omega \right\}$ i $r_\omega = \left\{\langle \{1, 2, \dots\}, 0\rangle\colon n \in \omega\right\}$ . Wówczas $\mathbf{Prv}_{\mathfrak S}(\{1\}) = \{1, 2, 3, \dots\}$ ,

choć z $\{1, 2, \dots\}$ można przecież wywnioskować jeszcze element $0$ .

Konsekwencje i sprzeczność

Osobny artykuł: operator konsekwencji.

Zbiór $Y$ jest domknięty w $\mathfrak S$ , jeśli

$A \subseteq Y$ oraz

$\forall_{r \in R}\; \forall_{\langle \Pi, e\rangle \in r}\; (\Pi \subseteq Y \Rightarrow e \in Y)$

Czasami zbiory domknięte w systemie formalnym nazywa się teoriami tego systemu.

Konsekwencją zbioru $X$ w systemie formalnym $\mathfrak S$ nazywa się najmniejszy (w sensie zawierania) zbiór domknięty zawierający $X$ . Zbiór ten oznacza się jest symbolem $\mathbf{Cn}_{\mathfrak S}(X)$ .

David Hilbert (ur. 23 stycznia 1862 w Królewcu (Prusy Wschodnie) - zm. 14 lutego 1943 w Getyndze) - matematyk niemiecki; zajmował się algebraiczną teorią liczb, teorią równań całkowych, zagadnieniami rachunku wariacyjnego, podstawami geometrii i logiki matematycznej oraz problemami fizyki matematycznej.

Matematyka (. Ponieważ ścisłe założenia mogą dotyczyć najróżniejszych dziedzin myśli ludzkiej, a muszą być czynione w naukach ścisłych, technice a nawet w naukach humanistycznych, zakres matematyki jest szeroki i stale się powiększa.

W ten sposób w systemie formalnym $\mathfrak S$ można rozważać operator $\mathbf{Cn}_\mathfrak{S}$ nazywany operatorem konsekwencji lub domknięcia, który jak pokazuje powyższy przykład, nie zawsze jest finitarny.

Zachodzi następujący związek między operatorami $\mathbf{Cn}_{\mathfrak S}$ i $\mathbf{Prv}_{\mathfrak S}$ : $\mathbf{Prv}_\mathfrak{S}(X) \subseteq \mathbf{Cn}_\mathfrak{S}(X)$ ,

jeżeli system formalny jest finitarny, to $\mathbf{Prv}_{\mathfrak S}(X) = \mathbf{Cn}_{\mathfrak S}(X)$

dla każdego zbioru $X$ .

Zbiór $X$ jest sprzeczny w systemie formalnym $\mathfrak S$ , jeżeli $\mathrm{Cn}_{\mathfrak S}(X) = E$ . System formalny jest zwarty, jeśli każdy zbiór sprzeczny w tym systemie zawiera skończony podzbiór sprzeczny.

Porównywanie

Niech $\mathfrak S = \langle E, R, A\rangle$ będzie systemem formalnym i niech $r$ będzie regułą w zbiorze $E$ .

Reguła $r$ jest dopuszczalna w $\mathfrak S$ , jeśli $\Pi \subseteq \mathbf{Cn}_{\mathfrak S}(\varnothing) \Rightarrow e \in \mathbf{Cn}_{\mathfrak S}(\varnothing)$ , gdzie $\langle \Pi, e \rangle \in r$ .

Reguła $r$ jest wyprowadzalna w $\mathfrak S$ , jeżeli $e \in \mathbf{Cn}_{\mathfrak S}(\Pi)$ , gdzie $\langle \Pi, e \rangle \in r$ .

System formalny $\mathfrak S_1 = \langle E, R_1, A_1 \rangle$ jest niesłabszy niż $\mathfrak S$ , co oznacza się $\mathfrak S \preceq \mathfrak S_1$ , gdy

$A \subseteq \mathbf{Cn}_{\mathfrak S_1}(\varnothing)$ oraz

wszystkie reguły w $R$ są wyprowadzalne w $\mathfrak S_1$ .

Systemy są równoważne, jeśli $\mathfrak S \preceq \mathfrak S_1$ oraz $\mathfrak S_1 \preceq \mathfrak S$ , co zapisuje się $\mathfrak S \approx \mathfrak S_1$ .

Zobacz też

system domknięć

twierdzenie Lindenbauma