Characterizing Strongly First Order Dependencies: The Non-Jumping Relativizable Case

Pietro Galliani
(Free University of Bozen-Bolzano)

Team Semantics generalizes Tarski's Semantics for First Order Logic by allowing formulas to be satisfied or not satisfied by sets of assignments rather than by single assignments. Because of this, in Team Semantics it is possible to extend the language of First Order Logic via new types of atomic formulas that express dependencies between different assignments.

Some of these extensions are much more expressive than First Order Logic proper; but the problem of which atoms can instead be added to First Order Logic without increasing its expressive power is still unsolved.

In this work, I provide an answer to this question under the additional assumptions (true of most atoms studied so far) that the dependency atoms are relativizable and non-jumping. Furthermore, I show that the global (or Boolean) disjunction connective can be added to any strongly first order family of dependencies without increasing the expressive power, but that the same is not true in general for non strongly first order dependencies.

In Jérôme Leroux and Jean-Francois Raskin: Proceedings Tenth International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2019), Bordeaux, France, 2-3rd September 2019, Electronic Proceedings in Theoretical Computer Science 305, pp. 66–82.
Published: 18th September 2019.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: