This paper presents a simple decidable logic of functional dependence LFD, based on an extension of classical propositional logic with dependence atoms plus dependence quantifiers treated as modalities, within the setting of generalized assignment semantics for first order logic. The expressive strength, complete proof calculus and meta-properties of LFD are explored. Various language extensions are presented as well, up to undecidable modal-style logics for independence and dynamic logics of changing dependence models. Finally, more concrete settings for dependence are discussed: continuous (...) dependence in topological models, linear dependence in vector spaces, and temporal dependence in dynamical systems and games. (shrink)

Directed acyclic graphs (DAGs) constitute a qualitative representation for conditional independence (CI) properties of a probability distribution. It is known that every CI statement implied by the topology of a DAG is witnessed over it under a graph-theoretic criterion of d-separation. Alternatively, all such implied CI statements are derivable from the local independencies encoded by a DAG using the so-called semi-graphoid axioms. We consider Labeled Directed Acyclic Graphs (LDAGs) modeling graphically scenarios exhibiting context-specific independence (CSI). Such CSI statements are modeled (...) by labeled edges, where labels encode contexts in which the edge vanishes. We study the problem of identifying all independence statements implied by the structure and the labels of an LDAG. We show that this problem is coNP-hard for LDAGs and formulate a sound extension of the semi-graphoid axioms for the derivation of such implied independencies. Finally we connect our study to certain qualitative versions of independence ubiquitous in database theory and teams semantics. (shrink)

We prove that the form of conditional independence at play in database theory and independence logic is reducible to the first-order dividing calculus in the theory of atomless Boolean algebras. This establishes interesting connections between independence in database theory and stochastic independence. As indeed, in light of the aforementioned reduction and recent work of Ben-Yaacov :957–1012, 2013), the former case of independence can be seen as the discrete version of the latter.

In the literature on logics of imperfect information it is often stated, incorrectly, that the Game-Theoretical Semantics of Independence-Friendly quantifiers captures the idea that the players of semantical games are forced to make some moves without knowledge of the moves of other players. We survey here the alternative semantics for IF logic that have been suggested in order to enforce this “epistemic reading” of sentences. We introduce some new proposals, and a more general logical language which distinguishes between “independence from (...) actions” and “independence from strategies”. New semantics for IF logic can be obtained by choosing embeddings of the set of IF sentences into this larger language. We compare all the semantics proposed and their purported game-theoretical justifications, and disprove a few claims that have been made in the literature. (shrink)

This book illustrates the program of Logical-Informational Dynamics. Rational agents exploit the information available in the world in delicate ways, adopt a wide range of epistemic attitudes, and in that process, constantly change the world itself. Logical-Informational Dynamics is about logical systems putting such activities at center stage, focusing on the events by which we acquire information and change attitudes. Its contributions show many current logics of information and change at work, often in multi-agent settings where social behavior is essential, (...) and often stressing Johan van Benthem's pioneering work in establishing this program. However, this is not a Festschrift, but a rich tapestry for a field with a wealth of strands of its own. The reader will see the state of the art in such topics as information update, belief change, preference, learning over time, and strategic interaction in games. Moreover, no tight boundary has been enforced, and some chapters add more general mathematical or philosophical foundations or links to current trends in computer science. The theme of this book lies at the interface of many disciplines. Logic is the main methodology, but the various chapters cross easily between mathematics, computer science, philosophy, linguistics, cognitive and social sciences, while also ranging from pure theory to empirical work. Accordingly, the authors of this book represent a wide variety of original thinkers from different research communities. And their interconnected themes challenge at the same time how we think of logic, philosophy and computation. Thus, very much in line with van Benthem's work over many decades, the volume shows how all these disciplines form a natural unity in the perspective of dynamic logicians (broadly conceived) exploring their new themes today. And at the same time, in doing so, it offers a broader conception of logic with a certain grandeur, moving its horizons beyond the traditional study of consequence relations. (shrink)

We study the extension of dependence logic \ by a majority quantifier \ over finite structures. We show that the resulting logic is equi-expressive with the extension of second-order logic by second-order majority quantifiers of all arities. Our results imply that, from the point of view of descriptive complexity theory, \\) captures the complexity class counting hierarchy. We also obtain characterizations of the individual levels of the counting hierarchy by fragments of \\).

We examine the transitions between sets of possible worlds described by the compositional semantics of Modal Dependence Logic, and we use them as the basis for a dynamic version of this logic. We give a game theoretic semantics, a (compositional) transition semantics and a power game semantics for this new variant of modal Dependence Logic, and we prove their equivalence; and furthermore, we examine a few of the properties of this formalism and show that Modal Dependence Logic can be recovered (...) from it by reasoning in terms of reachability. Then we show how we can generalize this approach to a very general formalism for reasoning about transformations between pointed Kripke models. (shrink)

We introduce generalized quantifiers, as defined in Tarskian semantics by Mostowski and Lindström, in logics whose semantics is based on teams instead of assignments, e.g., IF-logic and Dependence logic. Both the monotone and the non-monotone case is considered. It is argued that to handle quantifier scope dependencies of generalized quantifiers in a satisfying way the dependence atom in Dependence logic is not well suited and that the multivalued dependence atom is a better choice. This atom is in fact definably equivalent (...) to the independence atom recently introduced by Väänänen and Grädel. (shrink)

In this paper, we introduce a logic based on team semantics, called $\mathbf {FOT} $, whose expressive power is elementary, i.e., coincides with first-order logic both on the level of sentences and (possibly open) formulas, and we also show that a sublogic of $\mathbf {FOT} $, called $\mathbf {FOT}^{\downarrow } $, captures exactly downward closed elementary (or first-order) team properties. We axiomatize completely the logic $\mathbf {FOT} $, and also extend the known partial axiomatization of dependence logic to dependence logic (...) enriched with the logical constants in $\mathbf {FOT}^{\downarrow } $. (shrink)

We analyze the causal-observational languages that were introduced in Barbero and Sandu (2018), which allow discussing interventionist counterfactuals and functional dependencies in a unified framework. In particular, we systematically investigate the expressive power of these languages in causal team semantics, and we provide complete natural deduction calculi for each language. Furthermore, we introduce a generalized semantics which allows representing uncertainty about the causal laws, and we analyze the expressive power and proof theory of the causal-observational languages over this enriched semantics.

A dichotomy result of Sevenster (2014) [29] completely classified the quantifier prefixes of regular Independence-Friendly (IF) logic according to the patterns of quantifier dependence they contain. On one hand, prefixes that contain “Henkin” or “signalling” patterns were shown to characterize fragments of IF logic that capture NP-complete problems; all the remaining prefixes were shown instead to be essentially first-order. In the present paper we develop the machinery which is needed in order to extend the results of Sevenster to non-prenex, regular (...) IF sentences. This involves shifting attention from quantifier prefixes to a (rather general) class of syntactical tree prefixes. We partially classify the fragments of regular IF logic that are thus determined by syntactical trees; in particular, a) we identify four classes of tree prefixes that are neither signaling nor Henkin, and yet express NP-complete problems and other second-order concepts; and b) we give more general criteria for checking the first-orderness of an IF sentence. (shrink)

In recent years, the logic of questions and dependencies has been investigated in the closely related frameworks of inquisitive logic and dependence logic. These investigations have assumed classical logic as the background logic of statements, and added formulas expressing questions and dependencies to this classical core. In this paper, we broaden the scope of these investigations by studying questions and dependency in the context of intuitionistic logic. We propose an intuitionistic team semantics, where teams are embedded within intuitionistic Kripke models. (...) The associated logic is a conservative extension of intuitionistic logic with questions and dependence formulas. We establish a number of results about this logic, including a normal form result, a completeness result, and translations to classical inquisitive logic and modal dependence logic. (shrink)

In this paper, we axiomatize the negatable consequences in dependence and independence logic by extending the systems of natural deduction of the logics given in [22] and [11]. We prove a characterization theorem for negatable formulas in independence logic and negatable sentences in dependence logic, and identify an interesting class of formulas that are negatable in independence logic. Dependence and independence atoms, first-order formulas belong to this class. We also demonstrate our extended system of independence logic by giving explicit derivations (...) for Armstrong's Axioms and the Geiger-Paz-Pearl axioms of dependence and independence atoms. (shrink)

We investigate extensions of dependence logic with generalized quantifiers. We also introduce and investigate the notion of a generalized atom. We define a system of semantics that can accommodate variants of dependence logic, possibly extended with generalized quantifiers and generalized atoms, under the same umbrella framework. The semantics is based on pairs of teams, or double teams. We also devise a game-theoretic semantics equivalent to the double team semantics. We make use of the double team semantics by defining a logic (...) $$\hbox {DC}^2$$ DC 2 which canonically fuses together two-variable dependence logic $$\hbox {D}^2$$ D 2 and two-variable logic with counting quantifiers $$\hbox {FOC}^2$$ FOC 2 . We establish that the satisfiability and finite satisfiability problems of $$\hbox {DC}^2$$ DC 2 are complete for $$\hbox {NEXPTIME}$$ NEXPTIME. (shrink)

Team semantics is a highly general framework for logics which describe dependencies and independencies among variables. Typically, the dependencies considered in this context are properties of sets of configurations or data records. We show how team semantics can be further generalized to support languages for the discussion of interventionist counterfactuals and causal dependencies, such as those that arise in manipulationist theories of causation. We show that the “causal teams” we introduce in the present paper can be used for modelling some (...) classical counterfactual scenarios which are not captured by the usual causal models. We then analyse the basic properties of our counterfactual languages and discuss extensively the differences with respect to the Lewisian tradition. (shrink)

We develop a semantics for independence logic with respect to what we will call general models. We then introduce a simpler entailment semantics for the same logic, and we reduce the validity problem in the former to the validity problem in the latter. Then we build a proof system for independence logic and prove its soundness and completeness with respect to entailment semantics.

Accounts of logical independence which coincide when applied in the case of classical logic diverge elsewhere, raising the question of what a satisfactory all-purpose account of logical independence might look like. ‘All-purpose’ here means: working satisfactorily as applied across different logics, taken as consequence relations. Principal candidate characterizations of independence relative to a consequence relation are that there the consequence relation concerned is determined by only by classes of valuations providing for all possible truth-value combinations for the formulas whose independence (...) is at issue, and that the consequence relation ‘says’ nothing special about how those formulas are related that it does not say about arbitrary formulas. Each of these proposals returns counterintuitive verdicts in certain cases—the truth-value inspired approach classifying certain cases one would like to describe as involving failures of independence as being cases of independence, and the de Jongh approach counting some intuitively independent pairs of formulas as not being independent after all. In final section, a modification of the latter approach is tentatively sketched to correct for these misclassifications. The attention is on conceptual clarification throughout, rather than the provision of technical results. Proofs, as well as further elaborations, are lodged in the ‘longer notes’ in a final Appendix. (shrink)

This paper investigates formal logics for reasoning about determinacy and independence. Propositional Dependence Logic D and Propositional Independence Logic I are recently developed logical systems, based on team semantics, that provide a framework for such reasoning tasks. We introduce two new logics L_D and L_I, based on Kripke semantics, and propose them as alternatives for D and I, respectively. We analyse the relative expressive powers of these four logics and discuss the way these systems relate to natural language. We argue (...) that L_D and L_I naturally resolve a range of interpretational problems that arise in D and I.We also obtain sound and complete axiomatizations for L_D and L_I . (shrink)

Dependence logic, introduced in Väänänen [11], cannot be axiomatized. However, first-order consequences of dependence logic sentences can be axiomatized, and this is what we shall do in this paper. We give an explicit axiomatization and prove the respective Completeness Theorem.

We examine the relationship between dependence logic and game logics. A variant of dynamic game logic, called Transition Logic, is developed, and we show that its relationship with dependence logic is comparable to the one between first-order logic and dynamic game logic discussed by van Benthem. This suggests a new perspective on the interpretation of dependence logic formulas, in terms of assertions about reachability in games of imperfect information against Nature. We then capitalize on this intuition by developing expressively equivalent (...) variants of dependence logic in which this interpretation is taken to the foreground. (shrink)

Inspired by Kit Fine’s theory of arbitrary objects, we explore some ways in which the generic structure of the natural numbers can be presented. Following a suggestion of Saul Kripke’s, we discuss how basic facts and questions about this generic structure can be expressed in the framework of Carnapian quantified modal logic.

Inclusion logic is a variant of dependence logic that was shown to have the same expressive power as positive greatest fixed‐point logic. Inclusion logic is not axiomatisable in full, but its first order consequences can be axiomatized. In this paper, we provide such an explicit partial axiomatization by introducing a system of natural deduction for inclusion logic that is sound and complete for first order consequences in inclusion logic.

I contribute this paper on anonymity to honor the birthday of John Crossley. I am not only John’s friend, but also his grandson in the academic sense—as my doct.

Dependence logic and its many variants are new logics that aim at establishing a unified logical theory of dependence and independence underlying seemingly unrelated subjects. The area of dependence logic has developed rapidly in the past few years. We will give a short introduction to dependence logic and review some of the recent developments in the area.

We continue the work on the relations between independence logic and the model-theoretic analysis of independence, generalizing the results of [15] and [16] to the framework of abstract independence relations for an arbitrary AEC. We give a model-theoretic interpretation of the independence atom and characterize under which conditions we can prove a completeness result with respect to the deductive system that axiomatizes independence in team semantics and statistics.

We characterize the expressive power of extensions of Dependence Logic and Independence Logic by monotone generalized quanti ers in terms of quanti er extensions of existential second-order logic.

We analyse the two definitions of generalized quantifiers for logics of dependence and independence that have been proposed by F. Engström, comparing them with a more general, higher order definition of team quantifier. We show that Engström’s definitions can be identified, by means of appropriate lifts, with special classes of team quantifiers. We point out that the new team quantifiers express a quantitative and a qualitative component, while Engström’s quantifiers only range over the latter. We further argue that Engström’s definitions (...) are just embeddings of the first-order generalized quantifiers into team semantics, and fail to capture an adequate notion of team-theoretical generalized quantifier, save for the special cases in which the quantifiers are applied to flat formulas. We also raise several doubts concerning the meaningfulness of the monotone/nonmonotone distinction in this context. In the appendix we develop some proof theory for Engström’s quantifiers. (shrink)