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.
Niech
będzie dowolnym zbiorem. Operatorem konsekwencji w zbiorze
jest funkcja
spełniająca warunki:
| | ![{\displaystyle X\subseteq \mathbf {Cn} (X)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f9e3f58881d3fccfc30d5e5db6620fee5dbcf5f6) |
|
(1) |
| | ![{\displaystyle X\subseteq Y\;\Rightarrow \;\mathbf {Cn} (X)\subseteq \mathbf {Cn} (Y)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fb5db4039edb5080dad7a018b56214e243c9009d) |
|
(2) |
| | |
|
(3) |
dla
przy czym (1) i (3) implikują, że
| | ![{\displaystyle \mathbf {Cn} {\big (}\mathbf {Cn} (X){\big )}=\mathbf {Cn} (X)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e03dbd63d4798c69e40974c2804193af42bf0341) |
|
(4) |
Co więcej, warunki (1) – (3), równoważne są warunkowi:
| | |
|
(5) |
Zbiór
jest
-sprzeczny, jeśli
![{\displaystyle \mathbf {Cn} (X)=E}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c796ec3654e764f8249040456dda3a9f5a73ce74)
Zbiór, który nie jest
-sprzeczny, jest
-niesprzeczny.
Punkty stałe operatora konsekwencji nazywa się czasem jego teoriami.
Teoria
-zupełna, to maksymalna teoria
-niesprzeczna:
![{\displaystyle X\in \mathbf {Cmpl} (\mathbf {Cn} )\;\Leftrightarrow \;X=\mathbf {Cn} (X)\neq E\,\wedge \,\bigwedge \nolimits _{Y\supsetneq X}\mathbf {Cn} (Y)=E}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6eb3c1109d6479a7ef61b5cb1b3e2b8e532e1e38)
- Uwaga.
Rodzina
wszystkich
-teorii z działaniami
![{\displaystyle X\sqcap Y=X\cap Y\quad {\mbox{i}}\quad X\sqcup Y=\mathbf {Cn} (X\cup Y)\quad ,\qquad X,Y\in \mathbf {Th} _{\mathbf {Cn} }}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b574b055c66b5de31393ecfbc5a0d5277f7e2cac)
jest kratą zupełną.
- dowód.
- Jeśli
są teoriami, to
![{\displaystyle \mathbf {Cn} (\bigcap \nolimits _{j\in J}X_{j})\subseteq \bigcap \nolimits _{j\in J}\mathbf {Cn} (X_{j})=\bigcap \nolimits _{j\in J}X_{j}\subseteq \mathbf {Cn} {\big (}\bigcap \nolimits _{j\in J}X_{j}{\big )}.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d4e2eb3d506124cbd2584ac5776f328574ab8860)
- W szczególności część wspólna dwóch teorii jest teorią, czyli w rodzinie teorii zbiór
jest kresem dolnym pary teorii
Aby pokazać, że
jest kresem górnym pary teorii
niech
będzie teorią ograniczającą obie te teorie z góry. Wówczas
co kończy dowód.
- 2. Zupełność. Jeśli
są teoriami, to
oraz ![{\displaystyle \mathbf {Cn} {\big (}\bigcup \nolimits _{j\in J}X_{j}{\big )}=\mathbf {sup} _{j\in J}X_{j}.\qquad \qquad \square }](https://wikimedia.org/api/rest_v1/media/math/render/svg/7daa994d4320fbca3778b6fb01f572638bf06c6a)
Krata
nie musi być rozdzielna.
Operator konsekwencji jest zwarty, jeśli każdy zbiór
-sprzeczny zawiera skończony
-sprzeczny podzbiór.
Dla zwartych operatorów konsekwencji zachodzi następujące twierdzenie:
- Twierdzenie (Lindenbaum)
Załóżmy, że
jest zwarta. Jeśli
jest niesprzeczne, to istnieje zupełna teoria zupełna
zawierająca
Znane także w nieco ogólniejszej wersji pod postacią:
- Twierdzenie (relatywne tw. Lindenbauma)
Niech
będzie teorią i niech
będzie takie, że dla jakiegokolwiek
z tego, że
wynika, że
dla pewnego skończonego
Wówczas istnieje teoria
zawierająca
dla której
o ile tylko
Oba twierdzenia łatwo się dowodzi z Lematu Kuratowskiego-Zorna. Okazuje się jednak[1], że są one równoważne Pewnikowi Wyboru.
Niech bowiem
będzie parami rozłączną niepustą rodziną zbiorów niepustych, niech
i niech
jest zwarty i
jest
-niesprzeczne. Istnieje zatem
-zupełna teoria
Gdyby dla pewnego
przekrój
był pusty, to zbiór
byłby niesprzecznym rozszerzeniem zbioru
co jest niemożliwe.
To wystarczy, bowiem pierwsze z twierdzeń Lindenbauma wynika z twierdzenia drugiego.
Operator konsekwencji jest finitarny, jeśli
![{\displaystyle e\in \mathbf {Cn} (X)\;\Rightarrow \;\bigvee \nolimits _{X_{0}\subseteq X}{\big (}X_{0}\,{\mbox{- skończony}}\,\wedge \,e\in \mathbf {Cn} (X_{0}){\big )}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/af9d5f34838d5a87dc716ad12ad2502cc8cb8f15)
- Uwaga.
Finitarny operator konsekwencji ze skończonym zbiorem sprzecznym jest zwarty.
- Dowód.
Niech
będzie skończonym zbiorem sprzecznym i niech dany będzie dowolny sprzeczny
Wówczas
skąd z finitarności, istnieją
dla których
Wówczas jednak,
jest sprzeczny.
![{\displaystyle \square }](https://wikimedia.org/api/rest_v1/media/math/render/svg/455831d58fa08f311b934d324adcff89a868b4e4)
Uwaga ta jest o tyle istotna, że zazwyczaj rozpatrywane operatory konsekwencji są finitarne i mają wręcz jedno-, góra dwuelementowe zbiory sprzeczne.
W niektórych przypadkach, istnieje operacja
o tej własności, że
![{\displaystyle e\in \mathbf {Cn} (X)\;\Leftrightarrow \;\mathbf {Cn} (X\cup \{Ne\})\;\;e\in E\,,\;X\subseteq E.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1a207937ec7ccc3a7f8cdc08e6cde478e9dace86)
Wówczas zachodzi:
- Fakt. Operator
jest finitarny wtedy i tylko wtedy, gdy jest zwarty.
Pokazać jedynie trzeba, że jeśli operator ten jest finitarny, to jest skończony. Niech zatem
Wówczas
jest sprzeczny. Istnieje zatem skończony
dla którego
jest sprzeczny. To jednak znaczy, że
co kończy dowód.
Jeśli
jest zbiorem formuł pewnego języka zdaniowego, to operator konsekwencji
jest strukturalny, jeśli dla dowolnego homomorfizmu
języka zachodzi:
dla ![{\displaystyle e\in E,\;X\subseteq E.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/78bb174d939e209f33b3daaef4e5965d5fa75e1c)
Z każdym systemem formalnym
związany jest operator konsekwencji
(zob. systemów formalnych). Z drugiej strony, mając operator konsekwencji
w zbiorze
można rozważać system formalny
gdzie
Wówczas
Ponadto, wychodząc od systemu formalnego
i następnie konstruując w wyżej wymieniony sposób system
dla
okaże się, że systemy
i
są równoważne. Można powiedzieć nawet więcej: systemy formalne są równoważne wtedy i tylko wtedy, gdy wyznaczają te same operatory konsekwencji.
- ↑ Wojciech Dzik, The Existence of Lindenbaum’s Extensions Is Equivalent to the Axiom of Choice. 13, 1981, 29-31.
- M.Omyła, Zarys Logiki Niefregowskiej, PWN, Warszawa, 1986.
- W.A.Pogorzelski, Elementarny Słownik Logiki Formalnej, Rozprawy Uniwersytetu Warszawskiego, Białystok, 1989