Logika dla informatyków/Paradygmaty dowodzenia

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania

Paradygmaty dowodzenia

Sprawdzenie, czy dana formuła rachunku zdań jest tautologią, polega zwykle na obliczeniu jej wartości dla  różnych wartościowań, gdzie jest liczbą zmiennych zdaniowych tej formuły. Jak dotąd nie są znane radykalnie szybsze metody. Dla rachunku predykatów nie istnieje w ogóle żaden algorytm sprawdzania czy dana formuła jest tautologią (Twierdzenie 3.8). W obu przypadkach istnieją jednak metody dowodzenia pozwalające na wyprowadzanie prawdziwych formuł za pomocą ustalonych procedur syntaktycznych.

Każdy system dowodzenia zawiera dwa składniki:

  • początkowy zbiór formuł (lub wyrażeń zbudowanych z wielu formuł) zwanych aksjomatami;
  • zbiór operacji przekształcających wyrażenia w wyrażenia - operacje te są nazywane regułami dowodzenia.

Reguły dowodzenia opisują warunki, przy pomocy których można otrzymać nowe wyrażenie (nazywane konkluzją) z otrzymanych już wyrażeń (nazywanych przesłankami). Dowody w systemach formalnych są ciągami wyrażeń, być może posiadającymi dodatkową strukturę pozwalającą na lepszą wizualizację.

W dalszej części opiszemy trzy systemy dowodzenia: system typu hilbertowskiego (od nazwiska Davida Hilberta), system naturalnej dedukcji oraz rachunek sekwentów. Ostatnie dwa systemy znajdują zastosowanie w pewnych działach sztucznej inteligencji oraz w systemach automatycznego dowodzenia twierdzeń.

System hilbertowski

Poniższy system dowodzenia dotyczy formuł zbudowanych przy użyciu jedynie spójnika , stałej oraz zmiennych zdaniowych. Przypomnijmy, że dla dowolnej formuły , napis jest skrótem zapisu Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi\arr\bot} . Symbole w poniższym systemie oznaczają dowolne formuły.

Aksjomaty



Reguła dowodzenia

Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle {\rm (MP)}\hspace{1cm} \frac{\varphi\ \ \ \varphi\to\psi}{\psi}}

Reguła (MP) jest nazywana regułą odrywania lub też regułą modus ponens.

Dowodem w powyższym systemie nazywamy taki ciąg formuł, w którym każda formuła albo jest aksjomatem, albo też została otrzymana z wcześniej występujących formuł w wyniku zastosowania reguły odrywania. Powiemy, że formuła ma dowód lub jest twierdzeniem systemu hilbertowskiego, co zapiszemy , gdy istnieje dowód zawierający . Powyższą definicję możemy nieco uogólnić. Niech będzie dowolnym zbiorem formuł. Powiemy, że formuła ma dowód ze zbioru hipotez (notacja ), gdy jest twierdzeniem systemu, w którym zbiór aksjomatów został poszerzony o formuły ze zbioru .

Przykład 5.1

Niech będzie zmienną zdaniową. Pokażemy, że formuła jest twierdzeniem systemu hilbertowskiego. Poniżej podajemy dowód dla tej formuły. W nawiasach podajemy nazwę aksjomatu, jeśli dana formuła jest instancją tego aksjomatu, lub też numery formuł z wcześniejszych kroków dowodu, do których jest stosowana reguła odrywania.

Zauważmy, że w powyższym przykładzie możemy wszędzie zastąpić zmienną przez dowolną formułę dostając dowód formuły .

Następujące twierdzenie jest bardzo użyteczne, gdy trzeba uzasadnić, że jakaś formuła jest twierdzeniem.

Twierdzenie 5.2 (o dedukcji)

Dla dowolnego zbioru formuł oraz dowolnych formuł , jeśli , to .

Dowód

Dowód jest indukcyjny ze względu na liczbę kroków w dowodzie formuły ze zbioru hipotez . Przypuśćmy najpierw, że dowód ten składa się tylko z jednego kroku. Jeśli , to stosując wyprowadzenie z Przykładu 5.1 dostajemy dowód formuły . Możemy oczywiście przyjąć, że formuła ta jest wyprowadzona ze zbioru hipotez . Druga możliwość jest taka, że lub też, że jest aksjomatem. W każdym z tych przypadków mamy . Wówczas stosując regułę odrywania do oraz aksjomatu , dostajemy formułę .

Założmy teraz, że ostatnim krokiem w wyprowadzeniu formuły jest zastosowanie reguły (MP) do formuł oraz , dla pewnej formuły . Z założenia indukcyjnego mamy oraz . Stosując regułę odrywania do oraz do aksjomatu (A2): dostajemy formułę . Ponownie stosując regułę odrywania do tej formuły oraz do dostajemy żądaną formułę . To kończy dowód twierdzenia o dedukcji.

End of proof.gif

Twierdzenie 5.3 (o poprawności)

Jeśli , to . W szczególności, jeśli , to jest tautologią.

Dowód

Dowód jest indukcyjny ze względu na liczbę kroków w wyprowadzeniu formuły  w systemie hilbertowskim ze zbioru hipotez . Jeśli dowód ten składa się tylko z jednego kroku, to albo , albo jest aksjomatem. W obu przypadkach oczywiście zachodzi .

Załóżmy teraz, że jest otrzymana przez zastosowanie reguły odrywania do formuł oraz . Z założenia indukcyjnego mamy

oraz Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle \Delta\models\psi. \hspace{3cm}(1) }

Niech będzie dowolnym wartościowaniem spełniającym wszystkie formuły z . Na mocy  (1), wartościowanie spełnia oraz spełnia . Wynika stąd, że spełnia . Tym samym udowodniliśmy, że . To kończy dowód.

End of proof.gif

Lemat 5.4

Dla dowolnych formuł zbudowanych przy użyciu oraz , następujące formuły są twierdzeniami systemu hilbertowskiego.

  1. ;
  2. ;
  3. ;

Dowód

(1)  Niech . Stosując regułę odrywania do formuł oraz dostajemy . Przez ponowne zastosowanie (MP) do tej formuły oraz do otrzymujemy wyprowadzenie . Tym samym pokazaliśmy, że . Stosując teraz trzy razy twierdzenie o dedukcji dostajemy

czyli

(2)  Ponieważ , więc z twierdzenia o dedukcji wynika . Stosując teraz (MP) do tej formuły oraz do aksjomatu (A3) w postaci otrzymujemy . Ponowne zastosowanie twierdzenia o dedukcji daje nam .

(3)  Niech . Zaczynamy od zbioru hipotez . Stosując (MP) do formuł oraz dostajemy . Ponowne zastosowanie (MP) do tej formuły oraz do  daje nam . Używając teraz twierdzenia o dedukcji do formuły otrzymujemy

Ponieważ mamy , to stosując (MP) otrzymujemy . Jeszcze raz używamy (MP) aby z i otrzymać i mamy

Na mocy twierdzenia o dedukcji . Stosując (MP) do formuły oraz do aksjomatu otrzymujemy . Dwukrotne zastosowanie twierdzenia o dedukcji daje nam . To kończy dowód lematu.

End of proof.gif

Powyższy system można łatwo rozszerzyć do systemu dla formuł opartych o pozostałe spójniki logiczne. Wystarczy w tym celu dodać aksjomaty wyrażające równoważności definiujące te spójniki.




Tak otrzymany system oznaczymy przez .

Twierdzenie 5.5 (o poprawności dla )

Dla dowolnego zbioru formuł i dla dowolnej formuły w języku z Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vee,\wedge,\arr,\bot} , jeśli Parser nie mógł rozpoznać (nieznana funkcja „\se”): {\displaystyle \displaystyle \se_{H^+}\varphi} to .

Dowód

Wystarczy sprawdzić, że aksjomaty (B1)-(B4) są tautologiami. Konkluzja wynika z  Twierdzenia 5.3 o poprawności dla .

End of proof.gif

Lemat 5.6

Dla dowolnej formuły istnieje formuła zbudowana przy użyciu jedynie oraz , taka że oraz .

Dowód

W danej formule , zastąpmy każdą podformułę postaci formułą oraz każdą podformułę postaci formułą . Aksjomaty (B1)-(B4) mówią, że zastąpione formuły są równoważne. Tak więc łatwo dostajemy oraz . Szczegóły dowodu pozostawimy Czytelnikowi.

End of proof.gif

System naturalnej dedukcji

System naturalnej dedukcji (wprowadzony przez S. Jaśkowskiego i G. Gentzena) operuje wyrażeniami zwanymi sekwentami. Są to wyrażenia postaci , gdzie jest pewnym skończonym zbiorem formuł, a jest formułą. W odróżnieniu od systemu hilbertowskiego, w naturalnej dedukcji istotne są reguły dowodzenia, a aksjomat jest bardzo prosty. Charakterystyczną cechą naturalnej dedukcji jest to, że reguły dowodzenia (za wyjątkiem reguły (PS) "przez sprzeczność") są podzielone na grupy, po jednej dla każdego spójnika. W ramach jednej takiej grupy mamy dwa rodzaje reguł. Reguły wprowadzania mówią o tym w jakiej sytuacji można wprowadzić dany spójnik na prawo od znaku (tj. wywnioskować formułę danego kształtu). Reguły eliminacji mówią o tym, w jakiej sytuacji można ten spójnik wyeliminować, tzn. jak można użyć formuły zbudowanej z jego pomocą do wyprowadzenia innej formuły. Regułę dowodzenia "przez sprzeczność" można traktować jako "silną" regułę eliminacji . Pamiętajmy, że oznacza formułę .

Poniżej będziemy stosować następującą konwencję: Napis oznacza zbiór , przy czym nie zakładamy tu, że .

Aksjomat

Reguły dowodzenia

-intro Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle ) \hspace{.2cm} \frac{\Delta,\varphi\vdash\psi}{\Delta\vdash\varphi\to\psi} \hspace{1cm} (\to } -elim Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle ) \hspace{.2cm} \frac{\Delta\vdash\varphi\to\psi\qquad \Delta\vdash\varphi}{\Delta\vdash\psi}}


-intro Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\varphi\qquad \Delta\vdash\psi}{\Delta\vdash\varphi\wedge\psi} \hspace{1cm} (\wedge } -elim Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle ) \hspace{.2cm}\frac{\Delta\vdash\varphi\wedge\psi}{\Delta\vdash\varphi} \hspace{1cm} (\wedge } -elim Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle ) \hspace{.2cm}\frac{\Delta\vdash\varphi\wedge\psi}{\Delta\vdash\psi}}


-intro Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\varphi}{\Delta\vdash\varphi\vee\psi} \hspace{1cm} (\vee } -intro Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\psi}{\Delta\vdash\varphi\vee\psi} }


-elim Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\varphi\vee\psi\qquad \Delta,\varphi\vdash\vartheta\qquad \Delta,\psi\vdash\vartheta}{\Delta\vdash\vartheta}}


PS Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta,\neg\varphi\vdash\bot}{\Delta\vdash\varphi}}


Zauważmy, że szczególnym przypadkiem reguły ( -intro) jest następująca reguła, można ją traktować jak regułę wprowadzenia negacji.

Zauważmy też, że szczególnym przypadkiem reguły ( -elim) jest następująca reguła, można ją traktować jak regułę eliminacji negacji.

O ile dowody w systemie hilbertowskim są tradycyjnie definiowane jako ciągi, a więc struktury liniowe, to w systemie naturalnej dedukcji dowody są drzewami. Pozwala to znacznie lepiej wizualizować zależności pomiędzy przesłankami i konkluzją stosowanych reguł. Dowodem sekwentu w systemie naturalnej dedukcji nazwiemy drzewo etykietowane sekwentami tak, że korzeń ma etykietę , liście są etykietowane wystąpieniami aksjomatu oraz każdy wewnętrzny wierzchołek jest etykietowany sekwentem otrzymanym z etykiet potomków tego wierzchołka przy zastosowaniu jednej z reguł. Piszemy , gdy sekwent ma dowód w systemie naturalnej dedukcji. Gdy , to mówimy też, że jest twierdzeniem systemu naturalnej dedukcji i zapisujemy to przez . Jeśli jest zbiorem nieskończonym, to oznacza, że istnieje dowód sekwentu , dla pewnego skończonego .

Poniżej podajemy kilka przykładów dowodów w systemie naturalnej dedukcji.

Przykład 5.7

  • Pokażemy .
  • Pokażemy .
  • Pokażemy .

Twierdzenie 5.8

Dla dowolnego sekwentu mamy następującą równoważność:

Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle \Delta\vdash_{N}\varphi\hspace{.2cm} } , gdy Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle \hspace{.2cm} \Delta\vdash_{H^+}\varphi.}

Aby pokazać, że każdy dowód w daje się przerobić na dowód w wystarczy sprawdzić, że każda z reguł systemu naturalnej dedukcji jest dopuszczalna w . Tzn. wystarczy sprawdzić, że jeśli mamy dowody przesłanek w , to możemy udowodnić konkluzję. Zauważmy, że wyprowadzalność reguły( intro) jest konsekwencją twierdzenia o dedukcji, natomiast reguła ( elim) jest regułą (MP). Przykładowo pokażemy wyprowadzenie ( elim) oraz (PS) w , pozostawiając Czytelnikowi wyprowadzenie pozostałych reguł.

Załóżmy, że mamy w dowody następujących sekwentów: , {.1cm} {.1cm}oraz {.1cm} . Wówczas, stosując aksjomat (B2) i regułę (MP) mamy . Zatem i ponieważ to również . Stąd . Stosując twierdzenie o dedukcji dostajemy . Skoro mamy również , to na mocy  Lematu 5.4 (3) otrzymujemy .

Dla wyprowadzenia (PS) załóżmy, że . Z twierdzenia o dedukcji dostajemy . Tak więc z (A3) i (MP) dostajemy .

Dla pokazania implikacji odwrotnej wystarczy pokazać, że wszystkie aksjomaty systemu są twierdzeniami systemu naturalnej dedukcji. Wyprowadzenia (A1) i (A3) w ND zostały podane w  Przykładzie 5.7. Przykładowo pokażemy wyprowadzenia (A2) i (B1). Zaczniemy od wyprowadzenia (A2). Niech . Mamy następujący dowód:



Stosując trzy razy ( -intro ) do sekwentu dostajemy wyprowadzenie aksjomatu (A2).

Następnie pokażemy dowód (B1) w ND. Zaczniemy od wyprowadzenia , gdzie :



Następnie wyprowadzimy sekwent . Niech



Mając wyprowadzone sekwenty oraz , możemy zakończyć dowód (B1).


Rachunek sekwentów

Dla przedstawienia rachunku sekwentów rozszerzymy nieco pojęcie sekwentu. Przez sekwent będziemy teraz rozumieć napis , gdzie oraz są skończonymi zbiorami formuł. Intuicyjnie, wyprowadzalność sekwentu w rachunku sekwentów będzie oznaczać, że alternatywa formuł z wynika z hipotez .

Podobnie jak w poprzedniej części, rozważamy formuły, zbudowane w oparciu o spójniki oraz stałą zdaniową . Negację traktujemy jako spójnik zdefiniowany przez .

Charakterystyczną cechą rachunku sekwentów jest specyficzna postać reguł. Reguły w tym systemie naturalnie dzielą się na dwie grupy: jedna grupa reguł opisuje sytuacje kiedy możemy wprowadzić dany spójnik na lewo od znaku , a druga grupa jest odpowiedzialna za wprowadzanie spójnika na prawo od . Dla każdego spójnika mamy odpowiadającą parę reguł. Aksjomat (A) można traktować jako regułę (bez przesłanek) wprowadzenia z lewej strony znaku .

Przypomnijmy, że napis oznacza zbiór .

Aksjomaty

Reguły dowodzenia

-lewa Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\Gamma,\varphi\qquad \Delta,\psi\vdash\Gamma}{\Delta,\varphi\to\psi\vdash\Gamma} \hspace{1cm}(\to } -prawa Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta,\varphi\vdash\Gamma,\psi}{\Delta\vdash\Gamma, \varphi\to\psi}}


-lewa Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta,\varphi,\psi\vdash\Gamma}{\Delta,\varphi\wedge\psi\vdash\Gamma} \hspace{1cm} (\wedge } -prawa Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\Gamma, \varphi\qquad \Delta\vdash\Gamma,\psi}{\Delta\vdash \Gamma,\varphi\wedge\psi}}


-lewa Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta, \varphi\vdash\Gamma\qquad \Delta,\psi\vdash\Gamma}{\Delta, \varphi\vee\psi \vdash\Gamma} \hspace{1cm} (\vee } -prawa Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\Gamma, \varphi, \psi}{\Delta\vdash\Gamma, \varphi\vee\psi}}


Dowodem sekwentu , tak jak poprzednio, nazywamy drzewo etykietowane sekwentami tak, że korzeń jest etykietowany przez , liście są etykietowane aksjomatami oraz wierzchołki wewnętrzne są etykietowane sekwentami otrzymanymi poprawnie przez zastosowanie reguł dowodzenia. Jeśli istnieje dowód sekwentu w rachunku sekwentów to zapisujemy to tak: . (Litera G pochodzi od nazwiska twórcy tego systemu, G. Gentzena.) Piszemy też , gdy  jest nieskończony, ale dla pewnego skończonego .

Zauważmy, że jeśli mamy sekwent to stosując aksjomat (), a następnie ( -lewa) dostajemy sekwent . Zatem natępująca reguła jest dopuszczalna w systemie (tj. jeśli dodamy ją do systemu, to zbiór wyprowadzalnych sekwentów nie ulegnie zmianie):

-lewa Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\Gamma,\varphi}{\Delta, \neg\varphi\vdash\Gamma}}

Ponadto zauważmy, że jeśli mamy dowód sekwentu , to dla każdej formuły możemy ją dodać do prawej strony każdego sekwentu w tym dowodzie i otrzymamy dowód sekwentu . Łatwy dowód indukcyjny pozostawiamy Czytelnikowi ( Ćwiczenie 12).
W szczególności, jeśli mamy udowodniony sekwent , to możemy też udowodnić sekwent .
Stosując do niego regułę ( -prawa) otrzymujemy sekwent . Tym samym pokazaliśmy, że następująca reguła jest dopuszczalna w systemie :

-prawa Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle)\hspace{.2cm} \frac{\Delta,\varphi\vdash\Gamma}{\Delta \vdash\Gamma,\neg\varphi}}

Twierdzenie 5.9

Dla każdych i mamy następującą równoważność

Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle \Delta\vdash_G\varphi\hspace{.2cm} } wtedy i tylko wtedy, gdy Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle \hspace{.2cm} \Delta\vdash_{H^+}\varphi.}

Powyższe twierdzenie pozostawimy bez dowodu. Łatwo jest "przetłumaczyć" każde wyprowadzenie w systemie na dowód w stylu Hilberta. Dla dowodu implikacji odwrotnej rozszerza się system przez dodanie nowej reguły zwanej cięciem.

cięcie Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta,\varphi\vdash\Gamma\hspace{.7cm} \Delta\vdash\varphi, \Gamma}{\Delta\vdash\Gamma}}

Niech oznacza system gentzenowski z cięciem. Bez trudu można pokazać, że reguła odrywania jest dopuszczalna w . Zatem, korzystając z twierdzenia o pełności dla systemu hilbertowskiego, łatwo pokazujemy, że każda tautologia jest twierdzeniem systemu . Główna trudność w dowodzie  Twierdzenia 5.9 polega na udowodnieniu następującego twierdzenia o eliminacji cięcia. Twierdzenie to podajemy bez dowodu.

Twierdzenie 5.10 (o eliminacji cięcia)

Jeśli , to .

Główna zaleta dowodów w rachunku sekwentów (bez cięcia) wynika z następującej własności podformuł: wszystkie formuły występujące w przesłance dowolnej reguły są podformułami formuł występujących w konkluzji. Zatem np. w dowodzie sekwentu mamy do czynienia tylko z podformułami formuły . Dla danej formuły , łatwiej więc znaleźć dowód w sensie Gentzena niż np. dowód w sensie Hilberta. Dlatego systemy zbliżone do rachunku sekwentów znajdują zastosowanie w automatycznym dowodzeniu twierdzeń. Pokażemy to na przykładzie.

Przykład 5.11

  1. Poszukamy dowodu sekwentu w

. Ponieważ najbardziej zewnętrznym spójnikiem w rozważanej formule jest , to ostatnią regułą w poszukiwanym dowodzie musiała być reguła ( -prawa). Zatem wystarczy znaleźć dowód sekwentu . Najbardziej zewnętrznym spójnikiem formuły po lewej stronie jest , a zatem na mocy reguły ( -lewa) wystarczy udowodnić sekwent . Podobnie, na mocy reguły ( -prawa), wystarczy udowodnić sekwent , a on przecież jest aksjomatem.

  1. Jeśli zastosujemy powyższą procedurę do formuły, która

nie jest tautologią, to dostaniemy wskazówkę na to gdzie należy szukać wartościowania falsyfikującego tę formułę. (Wartościowanie falsyfikujące sekwent to takie, które spełnia wszystkie formuły z oraz falsyfikuje wszystkie formuły z .) Dla zilustrowania tej tezy weźmy bardzo prosty sekwent . Postępując podobnie jak poprzednio, dochodzimy do sekwentu , który nie jest aksjomatem, i którego nie możemy już dalej rozłożyć. Jako wartościowanie falsyfikujące wystarczy wziąć wartościowanie spełniające i falsyfikujące .

Z własności podformuł wynika też własność konserwatywności systemu nad swoimi fragmentami: jeśli formuła, w której nie występuje jakiś spójnik jest tautologią, to jej wyprowadzenie nie wymaga reguł związanych z tym spójnikiem.