Operator konsekwencji
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.
Spis treści |
Definicja [edytuj]
Niech
będzie dowolnym zbiorem. Operatorem konsekwencji w zbiorze
jest funkcja
spełniająca warunki:
![]() |
(1) |
![]() |
(2) |
![]() |
(3) |
-
-
dla

-
przy czym (1) i (3) implikują, że
![]() |
(4) |
Co więcej, warunki (1) – (3), równoważne są warunkowi:
![]() |
(5) |
Zbiory sprzeczne [edytuj]
Zbiór
jest
-sprzeczny, jeśli
Zbiór, który nie jest
-sprzeczny, jest
-niesprzeczny
Teorie, zupełność [edytuj]
Punkty stałe operatora konsekwencji nazywa się czasem jego teoriami.
Teoria
-zupełna, to maksymalna teoria
-niesprzeczna:
- Uwaga.
Rodzina
wszystkich
-teorii z działaniami
jest kratą zupełną.
- dowód.
- Jeśli
są teoriami, to
.- 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 
Krata
nie musi być rozdzielna.
Zwartość [edytuj]
Operator konsekwencji jest zwarty, jeśli każdy zbiór
-sprzeczny zawiera skończony
-sprzeczny podzbiór.
Twierdzenia Lindenbauma [edytuj]
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 takze w nieco ogólniejszej wersji pod postacią:
- Twierdzenie (relatywne tw. Lindenbauma)
Niech
będzie teorią i niech
bedzie 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.
Finitarność [edytuj]
Operator konsekwencji jest finitarny, jeśli
- 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.

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
.
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
. Wowczas
jest sprzeczny. Istnieje zatem skończony
, dla którego
jest sprzeczny. To jednak znaczy, że
, co kończy dowód.
Strukturalność [edytuj]
Jeśli
jest zbiorem formuł pewnego języka zdaniowego, to operator konsekwencji
jest strukturalny, jeśli dla dowolnego homomorfizmu
języka zachodzi:
, dla
.
Komentarze [edytuj]
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 sa równoważne wtedy i tylko wtedy, gdy wyznaczają te same operatory konsekwencji.
Zobacz też [edytuj]
Przypisy
- ↑ Wojciech Dzik, The Existence of Lindenbaum's Extensions Is Equivalent to the Axiom of Choice. 13, 1981, 29-31
Bibliografia [edytuj]
- M.Omyła, Zarys Logiki Niefregowskiej, PWN, Warszawa, 1986.
- W.A.Pogorzelski, Elementarny Słownik Logiki Formalnej, Rozprawy Uniwersytetu Warszawskiego, Białystok, 1989









są teoriami, to
.
jest kresem dolnym pary teorii
. Aby pokazać, że
jest kresem górnym pary teorii
będzie teorią ograniczającą obie te teorie z góry. Wówczas
, co kończy dowód.
oraz 

.
, dla
.