Inkluusio ja ekskluusio kvantifioinnissa

Abstract

Tässä tutkielmassa esitelemme uudet loogiset operaatiot, joita kutsumme inkluusio- ja ekskluusiokvanttoreiksi. Kun ensimmäisen kertaluvun logiikkaa laajennetaan inkluusiokvanttoreilla saadaan uusi logiikka, jota nimitämme INF-logiikaksi ('Inclusion Friendly Logic'). Vastaavasti lisäämällä ensimmäisen kertaluvun logiikkaan ekskluusiokvanttorit saadaan EXF-logiikka ('Exclusion Friendly Logic'), ja lisäämällä näistä kvanttoreista molemmat saadaan IEF-logiikka ('Inclusion-Exclusion Friendly Logic').

Esitämme tässä tutkielmassa esimerkkejä näiden kvanttorien käytöstä ilmaisemalla niiden avulla graafien ominaisuuksia, ja määrittelemme niitä käyttäen uusia hyödyllisiä loogisia operaatioita. Vertaamme lisäksi näiden uusien logiikoiden ilmaisuvoimaa inkluusio- ja ekskluusiologiikoihin, riippuvuuslogiikkaan, NDEP-logiikkaan ('Nondependence Logic') sekä lauseiden tasolla EMSO-logiikkaan ('Existential Monadic Second Order Logic').

Osoitamme, että EXF-logiikka on ilmaisuvoimaltaan vahvempi kuin yksipaikkainen riippuvuuslogiikka mutta heikompi kuin kaksipaikkainen riippuvuuslogiikka. Vastaavasti osoitamme, että INF-logiikan ilmaisuvoima sijoittuu aidosti yksi- ja kaksipaikkaisten NDEP-logiikoiden väliin. Lisäksi todistamme, että lauseiden tasolla INF-, EXF- sekä IEF-logiikka sisältyvät kaikki EMSO-logiikkaan. IEF-logiikalle pätee myös käänteinen väite, joten sen ilmaisuvoima on lauseiden tasolla täsmälleen sama kuin EMSO-logiikalla.