System formalny – 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.
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.
Definicja
Systemem formalnym (w zbiorze
) nazywamy trójkę
gdzie
jest dowolnym zbiorem,
a
jest zbiorem reguł wnioskowania w
Elementy zbioru
nazywa się wyrażeniami tego systemu, elementy zbioru
nazywa – aksjomatami, a elementy zbioru
– jego regułami.
System formalny jest finitarny, jeśli jego reguły są finitarne.
Dowody
Niech
będzie systemem formalnym,
oraz
Dowodem elementu
ze zbiorem założeń
w systemie
jest ciąg
elementów zbioru
dla którego:
![{\displaystyle e=e_{n},}](https://wikimedia.org/api/rest_v1/media/math/render/svg/28e6a8a2734e784cdcbb5906f503938da3fb104d)
- dla każdego
zachodzi przynajmniej jeden z warunków: ![{\displaystyle e_{k}\in X\cup A,}](https://wikimedia.org/api/rest_v1/media/math/render/svg/254394c255b68b5fc404ab28c363000c9bbbf8d4)
![{\displaystyle \exists _{r\in R}\;\exists _{\Pi \subseteq \{1,\dots ,k-1\}}\;\left(\langle \{e_{i}:i\in \Pi \},e_{k}\rangle \in r\right).}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d229751578e79e1f7ea810a6ba3ed42daa039632)
Zbiór elementów mających w
dowód ze zbiorem założeń
oznacza się symbolem
Przykłady dowodów w systemach formalnych wybranych rachunków zdaniowych można znaleźć tutaj i tutaj.
Własności
![{\displaystyle X\subseteq \mathbf {Prv} _{\mathfrak {S}}(X).}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6aae21856bed7c891a2986fe880c4cc2334134e0)
![{\displaystyle X\subseteq Y\Rightarrow \mathbf {Prv} _{\mathfrak {S}}(X)\subseteq \mathbf {Prv} _{\mathfrak {S}}(Y).}](https://wikimedia.org/api/rest_v1/media/math/render/svg/213658969a3eacda263dc76796406ea31ec0dea7)
![{\displaystyle \mathbf {Prv} _{\mathfrak {S}}{\big (}\mathbf {Prv} _{\mathfrak {S}}(X){\big )}=\mathbf {Prv} _{\mathfrak {S}}(X).}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4b5acc27d6a273d55490a463bc6600d1f38ff00d)
Z własności tych wynika, że
jest operatorem domknięcia, co więcej, jest on finitarny:
![{\displaystyle e\in \mathbf {Prv} _{\mathfrak {S}}(X)\Leftrightarrow \exists _{X_{0}{\mbox{ – skończony}}}\;\left(X_{0}\subseteq X,\;e\in \mathbf {Prv} _{\mathfrak {S}}(X_{0})\right).}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2117f97958ae92d619f12b0044dd757f853b470f)
Zakres wnioskowania
Mając dany zbiór „założeń”
chciałoby się znać wszystkie „fakty”
ze zbioru
które można wywnioskować ze zbioru
Niestety okazuje się, że zbiory
nie zawsze zawierają wszystkie „wnioski”.
Otóż, niech
i ![{\displaystyle R=\{r,r_{\omega }\},}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d77f887ecbc071218b2e6d4f1db15b4122e2ff7f)
gdzie
i
Wówczas
![{\displaystyle \mathbf {Prv} _{\mathfrak {S}}(\{1\})=\{1,2,3,\dots \},}](https://wikimedia.org/api/rest_v1/media/math/render/svg/36d7a9d507aa31eab8ee655c27a682c6cb7b4b70)
choć z
można przecież wywnioskować jeszcze element
Konsekwencje i sprzeczność
Osobny artykuł: operator konsekwencji.
Zbiór
jest domknięty w
jeśli
oraz ![{\displaystyle \forall _{r\in R}\;\forall _{\langle \Pi ,e\rangle \in r}\;(\Pi \subseteq Y\Rightarrow e\in Y)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6f560ab097ca1bcabe584c4b1efd54743091fa38)
Czasami zbiory domknięte w systemie formalnym nazywa się teoriami tego systemu.
Konsekwencją zbioru
w systemie formalnym
nazywa się najmniejszy (w sensie zawierania) zbiór domknięty zawierający
Zbiór ten oznacza się jest symbolem
W ten sposób w systemie formalnym
można rozważać operator
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
i
![{\displaystyle \mathbf {Prv} _{\mathfrak {S}}(X)\subseteq \mathbf {Cn} _{\mathfrak {S}}(X),}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fcfbe9994e43879ce5332b3e9f65ca01f43aaba8)
jeżeli system formalny jest finitarny, to
![{\displaystyle \mathbf {Prv} _{\mathfrak {S}}(X)=\mathbf {Cn} _{\mathfrak {S}}(X)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/face49c63f4167bda721a5a3a6617f45a086626f)
dla każdego zbioru
Zbiór
jest sprzeczny w systemie formalnym
jeżeli
System formalny jest zwarty, jeśli każdy zbiór sprzeczny w tym systemie zawiera skończony podzbiór sprzeczny.
Porównywanie
Niech
będzie systemem formalnym i niech
będzie regułą w zbiorze
Reguła
jest dopuszczalna w
jeśli
gdzie ![{\displaystyle \langle \Pi ,e\rangle \in r.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e871c0b68356fbcdbd04fd27b2172c9507e55109)
Reguła
jest wyprowadzalna w
jeżeli
gdzie ![{\displaystyle \langle \Pi ,e\rangle \in r.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e871c0b68356fbcdbd04fd27b2172c9507e55109)
System formalny
jest niesłabszy niż
co oznacza się
gdy
oraz - wszystkie reguły w
są wyprowadzalne w ![{\displaystyle {\mathfrak {S}}_{1}.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7efd2fa5d119eca9b6a2c619409be37a9700d72c)
Systemy są równoważne, jeśli
oraz
co zapisuje się
Zobacz też
Encyklopedia internetowa (rodzaj systemu):
- Britannica: topic/logical-calculus, topic/formal-system