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:
(1) |
(2) |
(3) |
dla
przy czym (1) i (3) implikują, że
(4) |
Co więcej, warunki (1) – (3), równoważne są warunkowi:
(5) |
Zbiór jest -sprzeczny, jeśli
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:
Rodzina wszystkich -teorii z działaniami
jest kratą zupełną.
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:
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ą:
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, ż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
Finitarny operator konsekwencji ze skończonym zbiorem sprzecznym jest zwarty.
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:
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:
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.