Dependence Logic: Investigations into Higher-Order Semantics Defined on Teams

Abstract

This thesis is a study of a rather new logic called dependence logic and its closure under classical negation, team logic.

In this thesis, dependence logic is investigated from several aspects. Some rules are presented for quantifier swapping in dependence logic and team logic. Such rules are among the basic tools one must be familiar with in order to gain the required intuition for using the logic for practical purposes.

The thesis compares Ehrenfeucht-Fraïssé (EF) games of first order logic and dependence logic and defines a third EF game that characterises a mixed case where first order formulas are measured in the formula rank of dependence logic.

The thesis contains detailed proofs of several translations between dependence logic, team logic, second order logic and its existential fragment. Translations are useful for showing relationships between the expressive powers of logics. Also, by inspecting the form of the translated formulas, one can see how an aspect of one logic can be expressed in the other logic.

The thesis makes preliminary investigations into proof theory of dependence logic. Attempts focus on finding a complete proof system for a modest yet nontrivial fragment of dependence logic. A key problem is identified and addressed in adapting a known proof system of classical propositional logic to become a proof system for the fragment, namely that the rule of contraction is needed but is unsound in its unrestricted form. A proof system is suggested for the fragment and its completeness conjectured.

Finally, the thesis investigates the very foundation of dependence logic. An alternative semantics called 1-semantics is suggested for the syntax of dependence logic. There are several key differences between 1-semantics and other semantics of dependence logic. 1-semantics is derived from first order semantics by a natural type shift. Therefore 1-semantics reflects an established semantics in a coherent manner. Negation in 1-semantics is a semantic operation and satisfies the law of excluded middle. A translation is provided from unrestricted formulas of existential second order logic into 1-semantics. Also game theoretic semantics are considerd in the light of 1-semantics.

Väitöskirja käsittelee uudehkoa logiikkaa nimeltään riippuvuuslogiikkaa (dependence logic) sekä sen laajennusta nimeltään tiimilogiikka (team logic). Riippuvuuslogiikan tunnusomainen piirre on mahdollisuus ilmaista tavallista monipuolisempia riippuvuussuhteita loogisten kaavojen muuttujien välillä. Riippuvuuslogiikka onkin aidosti ilmaisuvoimaisempi kuin tavallinen predikaattilogiikka. Tiimilogiikka on riippuvuuslogiikan sulkeuma klassisen negaation suhteen.

Väitöskirjan käytännöllisempiin tuloksiin kuuluvat kvanttorien vaihtosäännöt riippuvuuslogiikan kaavoissa. Lisäksi väitöskirja tutkii Ehrenfeucht-Fraïssé-pelien suhteita riippuvuuslogiikan ja predikaattilogiikan välillä. Nämä tulokset auttavat osaltaan ymmärtämään riippuvuuslogiikkaa ja edesauttavat intuition kehittämistä sen käytössä.

Abstraktimpiin tuloksiin kuuluvat useat yksityiskohtaiset käännöstulokset riippuvuuslogiikan, tiimilogiikan, toisen kertaluvun logiikan ja sen eksistentiaalisen fragmentin välillä. Käännösten avulla voidaan vertailla logiikoiden ilmaisuvoimia keskenään. Lisäksi tarkastelemalla käännettyjä kaavoja voidaan havaita, miten yhden logiikan tietyt piirteet siirtyvät toiseen logiikkaan.

Väitöskirjassa tutkitaan myös riippuvuuslogiikan todistusteoriaa. Tutkimus keskittyy riippuvuuslogiikan erääseen yksinkertaiseen fragmenttiin, joka muistuttaa klassista propositiologiikkaa. Tälle fragmentille määritellään klassisen propositiologiikan todistusjärjestelmää muistuttava järjestelmä, jossa supistussääntöä joudutaan rajoittamaan.

Lopuksi väitöskirja pureutuu riippuvuuslogiikan ytimeen ja määrittelee sille vaihtoehtoisen semantiikan nimeltään 1-semantiikka. 1-semantiikka eroaa aiemmista semantiikoista useilla tavoilla. Ensinnäkin se perustuu luontevaan tyypinnosto-operaatioon, joka johtaa riippuvuuslogiikan semantiikan yksiselitteisesti predikaattilogiikasta. Tämän seurauksena negaatiolle voidaan antaa puhtaasti semanttinen määritelmä. 1-semantiikan negaatio toteuttaa lisäksi kolmannen poissuljetun lain. 1-semantiikan ilmaisuvoiman todistetaan käännöksen avulla kattavan täsmälleen eksistentiaalinen toisen kertaluvun logiikan siinä, missä aiemmat semantiikat ovat kattaneet vain sen alaspäin suljetun fragmentin. Myös peliteoreettista semantiikkaa tarkastellaan 1-semantiikan valossa.