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.
Definicja
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
Zbiór jest -sprzeczny, jeśli
Zbiór, który nie jest -sprzeczny, jest -niesprzeczny.
Teorie, zupełność
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ść
Operator konsekwencji jest zwarty, jeśli każdy zbiór -sprzeczny zawiera skończony -sprzeczny podzbiór.
Twierdzenia Lindenbauma
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.
Finitarność
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 Wówczas jest sprzeczny. Istnieje zatem skończony dla którego jest sprzeczny. To jednak znaczy, że co kończy dowód.
Strukturalność
Jeśli jest zbiorem formuł pewnego języka zdaniowego, to operator konsekwencji jest strukturalny, jeśli dla dowolnego homomorfizmu języka zachodzi:
- dla
Komentarze
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.
Zobacz też
Przypisy
- ↑ Wojciech Dzik, The Existence of Lindenbaum’s Extensions Is Equivalent to the Axiom of Choice. 13, 1981, 29-31.
Bibliografia
- M.Omyła, Zarys Logiki Niefregowskiej, PWN, Warszawa, 1986.
- W.A.Pogorzelski, Elementarny Słownik Logiki Formalnej, Rozprawy Uniwersytetu Warszawskiego, Białystok, 1989