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.

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

${\displaystyle X\subseteq \mathbf {Cn} (X)}$

(1)

${\displaystyle X\subseteq Y\;\Rightarrow \;\mathbf {Cn} (X)\subseteq \mathbf {Cn} (Y)}$

(2)

${\displaystyle \mathbf {Cn} {\big (}\mathbf {Cn} (X){\big )}\subseteq \mathbf {Cn} (X),}$

(3)

dla ${\displaystyle X,Y\subseteq E,}$

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

${\displaystyle \mathbf {Cn} {\big (}\mathbf {Cn} (X){\big )}=\mathbf {Cn} (X)}$

(4)

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

${\displaystyle X\subseteq \mathbf {Cn} (Y)\quad \Leftrightarrow \quad \mathbf {Cn} (X)\subseteq \mathbf {Cn} (Y),}$

(5)

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

${\displaystyle \mathbf {Cn} (X)=E}$

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

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

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

${\displaystyle X\in \mathbf {Cmpl} (\mathbf {Cn} )\;\Leftrightarrow \;X=\mathbf {Cn} (X)\neq E\,\wedge \,\bigwedge \nolimits _{Y\supsetneq X}\mathbf {Cn} (Y)=E}$

Uwaga.

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

${\displaystyle 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 ${\displaystyle X_{j}\,,\;j\in J,}$ są teoriami, to

${\displaystyle \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 ${\displaystyle X\cap Y}$ jest kresem dolnym pary teorii ${\displaystyle X\;{\mbox{i}}\;Y.}$ Aby pokazać, że ${\displaystyle \mathbf {Cn} (X\cup Y)}$ jest kresem górnym pary teorii ${\displaystyle X\;{\mbox{i}}\;Y,}$ niech ${\displaystyle Z}$ będzie teorią ograniczającą obie te teorie z góry. Wówczas ${\displaystyle \mathbf {Cn} (X\cup Y)\subseteq \mathbf {Cn} (Z)=Z,}$ co kończy dowód.

2. Zupełność. Jeśli ${\displaystyle X_{j}\,,\;j\in J,}$ są teoriami, to ${\displaystyle \bigcap \nolimits _{j\in J}X_{j}=\mathbf {inf} _{j\in J}X_{j}}$ oraz ${\displaystyle \mathbf {Cn} {\big (}\bigcup \nolimits _{j\in J}X_{j}{\big )}=\mathbf {sup} _{j\in J}X_{j}.\qquad \qquad \square }$

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

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

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

Twierdzenie (Lindenbaum)

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

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

Twierdzenie (relatywne tw. Lindenbauma)

Niech ${\displaystyle X}$ będzie teorią i niech ${\displaystyle e\not \in X}$ będzie takie, że dla jakiegokolwiek ${\displaystyle Y}$ z tego, że ${\displaystyle e\in \mathbf {Cn} (Y)}$ wynika, że ${\displaystyle e\in \mathbf {Cn} (Y_{0}),}$ dla pewnego skończonego ${\displaystyle Y_{0}\subseteq Y.}$ Wówczas istnieje teoria ${\displaystyle X^{\star }}$ zawierająca ${\displaystyle X,}$ dla której ${\displaystyle e\in \mathbf {Cn} (X^{\star }\cup \{c\})}$ o ile tylko ${\displaystyle 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 ${\displaystyle {\mathcal {A}}}$ będzie parami rozłączną niepustą rodziną zbiorów niepustych, niech ${\displaystyle E=\bigcup {\mathcal {A}}}$ i niech ${\displaystyle \mathbf {Cn} (X)={\begin{cases}X,&{\mbox{ jeśli }}|A\cap X|\leqslant 1{\mbox{ dla }}{A\in {\mathcal {A}}}\\E,&{\mbox{ w przc. wyp.}}\end{cases}}.}$ ${\displaystyle \mathbf {Cn} (X)}$ jest zwarty i ${\displaystyle \varnothing }$ jest ${\displaystyle \mathbf {Cn} }$-niesprzeczne. Istnieje zatem ${\displaystyle \mathbf {Cn} }$-zupełna teoria ${\displaystyle X^{\star }.}$ ${\displaystyle \#(X^{\star }\cap A)\leqslant 2\,,\;A\in {\mathcal {A}}.}$ Gdyby dla pewnego ${\displaystyle A\in {\mathcal {A}}}$ przekrój ${\displaystyle X^{\star }\cap A}$ był pusty, to zbiór ${\displaystyle X^{\star }\cup \{a\}}$ byłby niesprzecznym rozszerzeniem zbioru ${\displaystyle X^{\star },}$ co jest niemożliwe.

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

Operator konsekwencji jest finitarny, jeśli

${\displaystyle 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 ${\displaystyle X^{\star }=\{e_{1},\dots ,e_{n}\}}$ będzie skończonym zbiorem sprzecznym i niech dany będzie dowolny sprzeczny ${\displaystyle X.}$ Wówczas ${\displaystyle e_{1},\dots ,e_{n}\in E=\mathbf {Cn} (X),}$ skąd z finitarności, istnieją ${\displaystyle X_{1},\dots ,X_{n}\subseteq X,}$ dla których ${\displaystyle e_{1}\in \mathbf {Cn} (X_{1}),\dots ,e_{n}\in \mathbf {Cn} (X_{n}).}$ Wówczas jednak, ${\displaystyle X_{0}=X_{1}\cup \ldots \cup X_{n}\subseteq X}$ 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 ${\displaystyle N\colon E\to E}$ o tej własności, że

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

Wówczas zachodzi:

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

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

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

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

• rachunek zdaniowy
• system formalny

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