Semantyczne badania fragmentów Intuicjonistycznej Logiki Kontrolnej

Abstract

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.