Operator konsekwencji

Z Wikipedii, wolnej encyklopedii
Skocz do: nawigacja, szukaj

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[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.
  1. 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 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ść[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 . Wówczas 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 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

  1. 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