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 | edytuj kod]

Niech E będzie dowolnym zbiorem. Operatorem konsekwencji w zbiorze E jest funkcja \mathbf{Cn}\colon\wp(E)\to\wp(E) spełniająca warunki:

X\subseteq\mathbf{Cn}(X)
(1)
X\subseteq Y\;\Rightarrow\;\mathbf{Cn}(X)\subseteq\mathbf{Cn}(Y)
(2)
\mathbf{Cn}\big(\mathbf{Cn}(X)\big)\subseteq\mathbf{Cn}(X)\;,
(3)
dla X,Y\subseteq E

przy czym (1) i (3) implikują, że

\mathbf{Cn}\big(\mathbf{Cn}(X)\big)=\mathbf{Cn}(X)
(4)

Co więcej, warunki (1)(3), równoważne są warunkowi:

X\subseteq\mathbf{Cn}(Y)\quad\Leftrightarrow\quad\mathbf{Cn}(X)\subseteq\mathbf{Cn}(Y)\;,
(5)

Zbiory sprzeczne[edytuj | edytuj kod]

Zbiór X\subseteq E jest \mathbf{Cn}-sprzeczny, jeśli

\mathbf{Cn}(X)=E

Zbiór, który nie jest \mathbf{Cn}-sprzeczny, jest \mathbf{Cn}-niesprzeczny

Teorie, zupełność[edytuj | edytuj kod]

Punkty stałe operatora konsekwencji nazywa się czasem jego teoriami.

Teoria \mathbf{Cn}-zupełna, to maksymalna teoria \mathbf{Cn}-niesprzeczna:

X\in\mathbf{Cmpl}(\mathbf{Cn})\;\Leftrightarrow\;X=\mathbf{Cn}(X)\ne E\,\wedge\,\bigwedge\nolimits_{Y\supsetneq X}\mathbf{Cn}(Y)=E
Uwaga.

Rodzina \mathbf{Th}_\mathbf{Cn} wszystkich \mathbf{Cn}-teorii z działaniami

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}

jest kratą zupełną.

dowód.
  1. Jeśli X_j\,,\;j\in J, są teoriami, to

\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).
W szczególności część wspólna dwóch teorii jest teorią, czyli w rodzinie teorii zbiór X\cap Y jest kresem dolnym pary teorii X\;\mbox{i}\;Y. Aby pokazać, że \mathbf{Cn}(X\cup Y) jest kresem górnym pary teorii X\;\mbox{i}\;Y, niech Z będzie teorią ograniczającą obie te teorie z góry. Wówczas \mathbf{Cn}(X\cup Y)\subseteq \mathbf{Cn}(Z)=Z, co kończy dowód.
2. Zupełność. Jeśli X_j\,,\;j\in J, są teoriami, to \bigcap\nolimits_{j\in J}X_j=\mathbf{inf}_{j\in J}X_j oraz \mathbf{Cn}\big(\bigcup\nolimits_{j\in J}X_j\big)=\mathbf{sup}_{j\in J}X_j.\qquad\qquad\square

Krata \mathbf{Th}_\mathbf{Cn} nie musi być rozdzielna.


Zwartość[edytuj | edytuj kod]

Operator konsekwencji jest zwarty, jeśli każdy zbiór \mathbf{Cn}-sprzeczny zawiera skończony \mathbf{Cn}-sprzeczny podzbiór.

Twierdzenia Lindenbauma[edytuj | edytuj kod]

Dla zwartych operatorów konsekwencji zachodzi następujące twierdzenie:

Twierdzenie (Lindenbaum)

Załóżmy, że \mathbf{Cn} jest zwarta. Jeśli X jest niesprzeczne, to istnieje zupełna teoria zupełna X^\star zawierająca X.

Znane także w nieco ogólniejszej wersji pod postacią:

Twierdzenie (relatywne tw. Lindenbauma)

Niech X będzie teorią i niech e\not\in X będzie takie, że dla jakiegokolwiek Y z tego, że e\in\mathbf{Cn}(Y) wynika, że e\in\mathbf{Cn}(Y_0), dla pewnego skończonego Y_0\subseteq Y. Wówczas istnieje teoria X^\star zawierająca X, dla której e\in\mathbf{Cn}(X^\star\cup\{c\}) o ile tylko c\not\in X^\star.

Oba twierdzenia łatwo się dowodzi z Lematu Kuratowskiego-Zorna. Okazuje się jednak[1], że są one równoważne Pewnikowi Wyboru.

Niech bowiem \mathcal{A} będzie parami rozłączną niepustą rodziną zbiorów niepustych, niech E=\bigcup\mathcal{A} i niech \mathbf{Cn}(X)=\begin{cases}X,&\mbox{ jeśli }|A\cap X|\leqslant1\mbox{ dla }{A\in\mathcal{A}}\\E,&\mbox{ w przc. wyp.}\end{cases}. \mathbf{Cn}(X) jest zwarty i \varnothing jest \mathbf{Cn}-niesprzeczne. Istnieje zatem \mathbf{Cn}-zupełna teoria X^\star. \#(X^\star\cap A)\leqslant2\,,\;A\in\mathcal{A}. Gdyby dla pewnego A\in\mathcal{A} przekrój X^\star\cap A był pusty, to zbiór X^\star\cup\{a\} byłby niesprzecznym rozszerzeniem zbioru X^\star, co jest niemożliwe.

To wystarczy, bowiem pierwsze z twierdzeń Lindenbauma wynika z twierdzenia drugiego.

Finitarność[edytuj | edytuj kod]

Operator konsekwencji jest finitarny, jeśli

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)
Uwaga.

Finitarny operator konsekwencji ze skończonym zbiorem sprzecznym jest zwarty.

dowód.

Niech X^\star=\{e_1,\ldots,e_n\} będzie skończonym zbiorem sprzecznym i niech dany będzie dowolny sprzeczny X. Wówczas e_1,\ldots,e_n\in E=\mathbf{Cn}(X), skąd z finitarności, istnieją X_1,\ldots,X_n\subseteq X, dla których e_1\in\mathbf{Cn}(X_1),\ldots,e_n\in\mathbf{Cn}(X_n). Wówczas jednak, X_0=X_1\cup\ldots\cup X_n\subseteq X jest sprzeczny.

\square

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 N\colon E\to E o tej własności, że

e\in\mathbf{Cn}(X)\;\Leftrightarrow\;\mathbf{Cn}(X\cup\{Ne\})\;\; e\in E\,,\;X\subseteq E.

Wówczas zachodzi:

Fakt. Operator \mathbf{Cn} 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 e\in\mathbf{Cn}(X). Wówczas \mathbf{Cn}(X\cup\{Ne\}) jest sprzeczny. Istnieje zatem skończony X_0\subseteq X, dla którego \mathbf{Cn}(X_0\cup\{Ne\}) jest sprzeczny. To jednak znaczy, że e\in\mathbf{Cn}(X_0), co kończy dowód.

Strukturalność[edytuj | edytuj kod]

Jeśli E jest zbiorem formuł pewnego języka zdaniowego, to operator konsekwencji \mathbf{Cn} jest strukturalny, jeśli dla dowolnego homomorfizmu h języka zachodzi:

e\in\mathbf{Cn}(X)\;\Rightarrow\;h(e)\in\mathbf{Cn}(h\,\grave{}\,\grave{}X), dla e\in E,\; X\subseteq E.

Komentarze[edytuj | edytuj kod]

Z każdym systemem formalnym \mathfrak{S} związany jest operator konsekwencji \mathbf{Cn}_\mathfrak{S} (zob. systemów formalnych). Z drugiej strony, mając operator konsekwencji \mathbf{Cn} w zbiorze E, można rozważać system formalny \mathfrak{S}_\mathbf{Cn}=\langle E,\{\vdash_\mathbf{Cn}\},\mathbf{Cn}(\varnothing)\rangle, gdzie \vdash_\mathbf{Cn}=\{\langle \Pi,e\rangle:\,e\in\mathbf{Cn}(\Pi)\,\}. Wówczas \mathbf{Cn}_{(\mathfrak{S}_\mathbf{Cn})}=\mathbf{Cn}. Ponadto, wychodząc od systemu formalnego \mathfrak{S} i następnie konstruując w wyżej wymieniony sposób system \mathfrak{S}^\star dla \mathbf{Cn}_\mathfrak{S}, okaże się, że systemy \mathfrak{S} i \mathfrak{S}^\starró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 | edytuj kod]

Przypisy

  1. Wojciech Dzik, The Existence of Lindenbaum's Extensions Is Equivalent to the Axiom of Choice. 13, 1981, 29-31

Bibliografia[edytuj | edytuj kod]

  • M.Omyła, Zarys Logiki Niefregowskiej, PWN, Warszawa, 1986.
  • W.A.Pogorzelski, Elementarny Słownik Logiki Formalnej, Rozprawy Uniwersytetu Warszawskiego, Białystok, 1989