| Abstrakt: | Badamy fragmenty oraz własnosci Intuicjonistycznej Logiki Kontrolnej, która została
wprowadzona przez Ch. Lianga i D. Millera. Logike te mozna do pewnego stopnia
traktowac jako połaczenie logiki intuicjonistycznej i logiki klasycznej. Powstaje ona z Intuicjonistycznej
Logiki Zdaniowej poprzez dodanie do jezyka nowej stałej falsum oznaczanej
przez ?, róznej od falsum intuicjonistycznego oznaczanego przez 0. Dzieki temu
mozliwe jest wydefiniowanie dwóch róznych negacji: zwykłej negacji intuicjonistycznej
oraz nowej negacji posiadajacej pewne cechy negacji w logice klasycznej.
W Rozdziale 1 prezentujemy podstawowe definicje i twierdzenia dotyczace Intuicjonistycznej
Logiki Zdaniowej, na tle których w nastepnych rozdziałach jest rozpatrywana
Intuicjonistyczna Logika Kontrolna.
Rozdział 2 rozpoczynamy od przytoczenia definicji i twierdzen dotyczacych Intuicjonistycznej
Logiki Kontrolnej. Implusem do stworzenia tej logiki było poszukiwanie systemu
logicznego, w którym mozna wydefiniowac operatory kontrolne znane z funkcyjnych
jezyków programowania z równoczesnym zachowaniem siły wyrazu intuicjonistycznej implikacji.
Na gruncie Intuicjonistycznej Logiki Kontrolnej odbywa sie to poprzez nowa
negacje , co pociaga pytania o charakteryzacje negacyjnego fragmentu monadycznego
w tej logice. Podajemy kompletny opis tego fragmentu. Nastepnie badamy pozostałe
fragmenty monadyczne w odniesieniu do znanych wyników dotyczacych Intuicjonistycznej
Logiki Zdaniowej. W szczególnosci podajemy krate fragmentu monadycznego bez
intuicjonistycznego falsum.
W Rozdziale 3 rozwazamy pojecie odpowiednika modalnego (ang. modal companion)
znanego z badan nad logikami posrednimi. Intuicjonistyczna Logika Kontrolna nie jest
logika posrednia, poniewaz powstaje poprzez rozszerzenie jezyka, a nie poprzez dodanie
aksjomatów. Mimo tego mozna zanurzyc Intuicjonistyczna Logike Kontrolna w pewna
logike modalna. W szczególnosci podajemy zanurzenie tej logiki w zdaniowa logike modalna
z kwantyfikatorami zdaniowymi, która jest wyznaczona poprzez klase skonczonych
drzew z niezwrotnym korzeniem. Tak zdefiniowana logika nie jest a priori rozstrzygalna,
jednak pokazujemy, ze mozna ja zinterpretowac w monadycznej teorii drugiego rzedu
S!S, co pociaga jej rozstrzygalnosc. |