Approaches to Finite Variable Dependence: Expressiveness and Computational Complexity

Abstract

Riippuvuuslogiikka on uusi formalismi, jossa tarkastellaan riippuvuuskäsitteeseen liittyviä ilmiöitä muodollisen logiikan viitekehyksessä. Muodollisiin logiikoihin liittyvissä matemaattisissa tarkasteluissa tutkimuksen kohteena on tyypillisesti logiikoiden ilmaisuvoima ja päättelyn laskennallinen vaativuus. Väitöskirjassa tarkastellaan useisiin eri riippuvuuskäsitteisiin perustuvia logiikoita. Työssä tutkitaan riippuvuuslogiikoiden ilmaisuvoimien ja laskennallisten vaativuuksien suhteita.

Työn päätuloksena on nk. IF-logiikan ja riippuvuuslogiikan D kahden muuttujan fragmenttien toteutuvuusongelmien erottelu suhteessa ratkeavuuteen. Lisäksi työ sisältää Boolen riippuvuuslogiikan ilmaisuvoiman kattavan luokittelun.

In this thesis we study computational aspects, expressive power and model-theoretic properties of fragments of various logics that are suitable for modeling diverse forms of variable dependence. In particular, we consider fragments of independence-friendly logic of Hintikka and Sandu, dependence logic of Väänänen, and first-order logic enriched with variants of partially-ordered connectives of Sandu and Väänänen closely related to the narrow Henkin quantifiers of Blass and Gurevich. Furthermore, we consider a novel variant of dependence logic called Boolean dependence logic.

The thesis consists of two principal chapters: Chapters 3 and 4. In Chapter 3 the focus is on the computational complexity and expressive power of finite variable fragments of independence-friendly logic and dependence logic. The main result of the chapter is the undecidability of the satisfiability problem for two-variable independence-friendly logic. In addition to studying the complexity of the satisfiability problem, we investigate the complexity of the related model checking problem. Moreover, we study certain model-theoretic properties of these logics: we consider the finite model property and the zero-one law. Chapter 4 is devoted on the study of the relationship between fragments of Boolean dependence logic and first-order logic enriched with partially-ordered connectives. We show that with respect to expressive power certain syntactic fragments of Boolean dependence logic correspond to natural logics enriched with partially-ordered connectives. Furthermore, we show that these fragments of Boolean dependence logic form a strict hierarchy with respect to expressive power. In addition, we establish that the expressive power of Boolean dependence logic and dependence logic coincide.