Authors: Valentin Goranko, Antti Kuusisto
Categories: cs.LO, math.LO
Valentin Goranko
Department of Philosophy
Stockholm University
Sweden
Department of Mathematics
University of Johannesburg
South Africa¹
Visiting professorship
Antti Kuusisto
FB3: Mathematics/Computer Science
University of Bremen
Germany
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.
In this paper we investigate the notions of propositional determinacy and propositional independence. We begin with a brief overview of related concepts.
Dependence and independence are abstract notions that have played an important role in mathematics and the natural sciences since antiquity. Today the concepts are omnipresent in virtually all fields of science. There exists a wide range of different scientific notions of dependence, e.g., statistical correlation, the causal relationship, and functional dependence. Likewise, the notion of independence has different meanings in different contexts, e.g., probabilistic and linear independence in mathematics, as well as political and behavioural independence in social vernacular.
An early formal logical analysis of dependence was proposed in [Gre39]². Dependencies in relational databases have been studied since (at least) the pioneering work of Codd in the early 1970’s. Of the many relevant references we only note here Armstrong’s work ([Arm74]) which provides a set of axioms for the notion of functional dependence in databases.
Also available as a reprint in [SvE88].
The concept of dependence has also appeared in various philosophical contexts under various different names. From the point of view of the current article, the notion of supervenience is perhaps the most important related concept. The paper [MB14] describes supervenience formally as follows:
“A set of properties A supervenes upon another set B just in case no two things can differ with respect to A-properties without also differing with respect to their B-properties. In slogan form, ‘there cannot be an A-difference without a B-difference’.”
On the formal level, perhaps the closest in spirit to the present study regarding dependence is Humberstone’s logical formalisation and study of supervenience as a generalisation of logical consequence in, e.g., [Hum92, Hum93, Hum98]. Another notion related to the current paper is the notion of contingency. Formal investigations of contingency can be found in, inter alia, [MR66], [Hum95, Hum02], as well as [Piz07, Piz13]. For a recent study of the contingency operator in various modal logics see [FWvD15].
We also mention two very recent and closely related papers written after the appearance of the earlier version [GK16] of the present paper. The two papers have at least partially been written as a response to [GK16]. The first one of them is [Fan16] which develops a formal modal logic of supervenience and also addresses some research questions raised in [GK16] and reiterated here in Section 8. The other one is [Hum17] which explores, inter alia, connections between supervenience and dependence and discusses in detail some aspects of [GK16].
In the context of logical semantics, the notion of independence has been investigated perhaps most prominently in Independence Friendly (IF) Logic originally defined in [HS89]; see also [Hin96]. IF logic was first formulated in terms of game-theoretic semantics, and no compositional semantics for that logic was originally available. Later on, Hodges developed ([Hod97]) a compositional semantics for the system, currently know as team semantics. The idea of team semantics, in turn, lead to Väänänen’s development of Dependence Logic in [Vää07]. Dependence logic sparked a renewed interest in logical formalisation and analysis of dependence and initiated an active related research programme. For an overview of the work in that direction, see [Kon13, GV14] and the references therein.
Väänänen’s Dependence Logic extends classical first-order logic with dependence atoms
D(x₁,...,xₖ;y)
with the intuitive meaning that the choice of an interpretation for y is functionally determined by the choices of interpretations for x₁,...,xₖ in evaluation games based on game-theoretic semantics. Since the introduction of dependence atoms, research on logics based on team semantics has flourished and several kinds of related logical systems have been investigated.
A propositional modal variant of Dependence Logic, called Modal Dependence Logic, was defined in [Vää08]. That logic extends the syntax of ordinary modal logic with a new operator D and formulae D(p₁,…,pₖ;q) with the intuitive interpretation that the truth values of p₁,…,pₖ determine the truth value of q. The propositional fragment of Modal Dependence Logic extended with D gives rise to Propositional Dependence Logic D. In the logic D, sets of propositional assignments are called teams; recall that a propositional assignment is simply a function from a set of atomic proposition symbols to the Boolean domain {0,1}. Intuitively, a team can be regarded as a set of possible worlds. A formula D(p;q) is then defined to be true in a team W if and only if each pair of possible worlds w,u∈ W that give the same truth value to p, must also give the same value to q. The more complex atoms D(p₁,…,pₖ;q) are interpreted in a similar fashion: any pair of worlds in W that agree on the truth values of p₁,…,pₖ, must also agree on the value of q (see Section 2 for the formal definition.) The propositions p₁,…,pₖ are said to determine q.
The notion of independence which we investigate in this paper originates from Independence Logic defined in [GV13]. Analogously to Dependence Logic, Independence Logic extends first-order logic by independence atoms
with the intuitive meaning that for any fixed set of values for y₁,…,yⱼ, the possible values for x₁,…,xᵢ are independent of the possible values for z₁,…,zₖ. A propositional variant of Independence Logic, called Propositional Independence Logic (and denoted here by I) has been investigated in the literature (in, e.g., [KMSV14], [Yan14]), and it relates to Independence Logic the same way Propositional Dependence Logic relates to Dependence Logic.
Dependence Logic and Independence Logic, together with the Inclusion Logic of [Gal12], are currently the central logical systems studied in the framework of team semantics. It is also worth noting here that Propositional Dependence Logic is closely related to inquisitive logic [Cia09, CR11]. In particular, the system InqL of inquisitive logic is a propositional team-based logic equi-expressive with D. For investigations on the relations between inquisitive logic and D, see, e.g., [Yan14, YV16, Cia16a, Cia16b].
While many of the semantic choices underlying Propositional Dependence Logic D are natural and justified, we will identify in this paper a range of issues that are problematic. One such issue is the interpretation of formulae that use combinations of determinacy operators D and disjunctions ∨. We will argue that while team semantics gives a sensible interpretation to formulae D(p₁,...,pₖ;q) as well as disjunctive formulae φ∨ψ free of operators D, interpretations of certain simple formulae that combine D and ∨ become strange from the point of view of natural language. We also discuss similar issues related to the team semantics interpretation of negation (together with D).
Motivated by the interpretational problems of D, we develop here an alternative natural logic of determinacy called Propositional Logic of Determinacy and denoted by L_D. The logics D and L_D have essentially the same set of formulae,³ but the semantic approaches differ. Instead of team semantics, the system L_D is essentially based on Kripke semantics. A formula D(φ₁,...,φₖ;ψ) is true⁴ in a possible world w if the set R(w) of accessible alternatives of w satisfies the determinacy condition: for all u,v∈ R(w), if u and v agree on the truth values of each φᵢ, they also agree on the truth value of ψ. The Boolean connectives as well as proposition symbols are interpreted in L_D in the same way as in Kripke semantics, and thus L_D can be regarded as a modal logic with a generalized modality D that talks about determinacy rather than possibility or necessity. Mainly in order to keep matters technically simple in this initial work on L_D, we assume the accessibility relation R to be the universal relation, so the set of successors of any world w is in fact the whole domain of the model. At the end of the paper we briefly discuss the general case with other kinds of accessibility relations.
Strictly speaking, L_D has more formulae than D because of the typical syntactic restrictions applied in D and team semantics in general. This issue is discussed in more detail in the sections below.
This truth definition was first suggested as an alternative to team semantics in [Kuu14] and its later versions such as, e.g., [Kuu15].
As an important part of our discourse on L_D, we present a range or arguments for the naturalness of L_D in relation to natural language. In particular, we argue that L_D resolves reasonably well the interpretational problems that we identify for D.
It turns out that Propositional Independence Logic I is burdened by virtually the same issues as Propositional Dependence Logic D, and these issues can be remedied by defining Propositional Logic of Independence L_ I analogously to L_D but based on the independence operator I rather than the dependence operator D.
In addition to introducing the logics L_D and L_ I and discussing how they, as well as D and I, relate to each other and to natural language, we also provide a comparative analysis of the expressive powers of these four logics. We show that, while D and I are both strictly contained in L_D and L_ I, the latter two logics are equally expressive. In fact, we establish in Sections 3 and 4 that L_D and L_ I are maximally expressive, or expressively complete, in a certain natural sense. Since it is well known from the literature on team semantics that D is strictly contained in I, we eventually obtain a complete classification of the relative expressive powers of the four logics.
We also prove that while both D and I translate into both L_D and L_ I, there exists no compositional translation⁵ from either of the team-semantics-based logics into L_D or L_ I. Intuitively, this indicates that team semantics and the Kripke-style semantics of L_D and L_ I are substantially different logical frameworks, at least from the technical point of view.
See Section 6.4 for the definition of compositional translations.
In addition to studying expressivity issues, we provide sound and complete axiomatizations for L_D and L_ I. This turns out to be a relatively straightforward, yet interesting exercise, due to certain close connections—to be identified below—between L_D, L_ I and Contingency Logic from [MR66]. Contingency Logic is the variant of modal logic with a modality C, where Cφ is interpreted to mean that φ is non-contingent at the state of evaluation, i.e., has the same truth value at every successor of that state. We also show that there do not exist finite axiomatisations for L_D and L_ I, assuming a standard notion of an axiomatic deduction system.
The structure of this paper is as follows. In Section 2 we provide the necessary background for the rest of the paper, including definitions of the logics D and I based on team semantics. In Sections 3 and 4 we define the logics L_D and L_ I and study their basic properties. Section 5 analyses the logics D, I, L_D and L_ I in relation to natural language. Section 6 investigates expressivity issues and Section 7 provides sound and complete axiomatizations for L_D and L_ I. Section 8 briefly discusses a range of future research directions and concludes the paper.
The agenda and main idea of the current paper, i.e., investigating dependence logic with a Kripke-style semantics instead of team semantics, has been first mentioned and briefly motivated in [Kuu14] and its later incarnations such as, e.g., [Kuu15]. Similar ideas have subsequently been developed in [Cia16b]. The current paper develops the ideas of [Kuu14] in detail, and furthermore, provides an extensive collection of related technical results concerning the expressivity and axiomatizability of L_D and related systems.
Section 6.7.2 of [Cia16b] contains an explicit comparison of L_D with a logic InqB ^⇒ that employs a Kripke-style approach (with some extra machinery) to semantics and thereby exhibits the same principle as L_D that dependence statements are modal statements. One of the main differences between InqB ^⇒ and L_D is that InqB ^⇒ contains an explicit machinery for questions and thereby allows semantically elaborate assertions about, e.g., dependence. Dependence statements in L_D are relations between statements, while in InqB ^⇒, dependence statements are construed as a relation between questions. See Sections 6.7.2 and 6.5 of [Cia16b] for further details.
Determinacy of a function by a set of functions is a central concept in this article. We will define it here in the general setting, though will use it further only on Boolean functions.
Let k∈ℤ₊ be a positive integer and let X,X₁,…,Xₖ,U be nonempty sets. Let f:U→ X be function, and consider a family of functions
{fᵢ:U→ Xᵢ | i=1,…,k} .
Given a set W⊆ U, we say that the function f is determined by the family of functions {f₁,…,fₖ} on W, or that the family {f₁,…,fₖ} determines the function f on W, if there exists a function F:X₁ ×…× Xₖ → X such that f is the composition of F and the functions f₁,…,fₖ on W, that is, f(w)=F(f₁(w),…,fₖ(w)) for every w∈ W. We also fix this definition in the following special case: we say that a function g:U→ X is determined by ∅ on W⊆ U if g is constant on W, i.e., g(w₁)=g(w₂) for all w₁,w₂ ∈ W.
This definition generalises straightforwardly to determinacy of a function by any family of functions {fᵢ:U→ Xᵢ | i∈ I} indexed with an arbitrary (possibly infinite) set I.
Equivalently, f is determined by the (possibly empty) family {f₁,…,fₖ} on W if and only if the following condition holds.
Det: For every w₁,w₂ ∈ W, it holds that if fᵢ(w₁)=fᵢ(w₂) for each i=1,…,k, then f(w₁)=f(w₂).
Indeed, if f is the composition of a mapping F with f₁,…,fₖ on W and fᵢ(w₁)=fᵢ(w₂) for each i=1,…,k, then F(f₁(w₁),…,fₖ(w₁))=F(f₁(w₂),…,fₖ(w₂)), i.e., f(w₁)=f(w₂). Conversely, if the condition Det holds, then we can define a mapping F:X₁ ×…× Xₖ → X as follows:
The condition Det guarantees that this is well-defined. ∎
We let Det_W(f₁,…,fₖ;f) denote the assertion that f is determined by the family of functions {f₁,…,fₖ} on W. When k=0, we write Det_W(∅ ;f).
We typically denote formulae by φ,ψ,χ,θ,α,β and sets of formulae by Φ,Ψ. Throughout the paper, we let PROP denote a fixed countably infinite set of proposition symbols. All formulae considered in the paper will be assumed to be built over PROP.
Let Φ={φ₁,…,φₖ} be a finite nonempty set of formulae. We define a set DNF() as follows.
We call the formulae in DNF() type normal form formulae over Φ.
In the above definition, ∅ is assumed to be the formula p p for some proposition symbol p∈PROP. We will not assume that the logical constant symbols → p, are available as primitives in the languages we consider. However, we will use these symbols as abbreviations for the formulae p p and p p, respectively. For technical convenience, we define DNF(∅):= → p, and Conj(∅):= → p, and thus we let → p be the unique type over ∅.
When we write a formula θ(q₁,…,qₖ), we indicate that all the propositional variables occurring in θ are amongst q₁,…,qₖ. Given a formula θ=θ(q₁,…,qₖ) and a tuple of formulae φ₁,…,φₖ, we denote by θ(φ₁,…,φₖ) the result of a uniform substitution of φ₁,…,φₖ, respectively, for q₁,…,qₖ in the formula θ.
Let L be a logic. A relation of equivalence ≡_L between formulae of L satisfies the equivalent replacements property (ER) (with respect to ≡_L), if for every L-formula θ(q₁,…,qₖ) and all tuples of φ₁,…,φₖ,ψ₁,…,ψₖ such that φᵢ≡_L ψᵢ for each i=1,…,k, it holds that θ(φ₁,…,φₖ)≡_L θ(ψ₁,…,ψₖ).
Recall that PROP denotes a fixed countably infinite set of proposition symbols. An assignment for PROP is any mapping f:PROP→ 0,1. Following Carnap, we occasionally call assignments also state descriptions.
Any (possibly empty) set W of state descriptions will be called a state description model (or SD-model). The reason we include the empty model in the picture is technical and related to the the fact that we will deal, inter alia, with logics based on team semantics. In team semantics, as we will see, the empty team plays an important role.
Especially in the more technical parts of the paper, we often talk about points or worlds of W rather than assignments or state descriptions.
In this paper we use a variant L_U of the modal logic with the universal modality from [GP92]. Formally, the syntax of the logic L_U is given by the grammar
where p∈PROP. We define ⟨U⟩ to be the dual of [U], i.e., ⟨ U ⟩φ:=[ U ]φ.
The semantics of L_U is defined with respect to SD-models W and assignments w∈ W as follows.
Thus, W,w_ U ⟨ U ⟩φ iff W,u_ U φ for some u∈ W.
As customary in modal logic, we define W_ U φ iff W,w_ U φ for all w∈ W. We also define, in the standard way, that _ U φ iff W_ U φ for all SD-models W.
We now define Propositional Dependence Logic D, which first appeared in the literature on team semantics as a syntactic fragment of Modal Dependence Logic, defined in [Vää08]. The paper [Vää08] did not make explicit references to D, and the semantics for Modal Dependence Logic—including its propositional fragment—was formulated in [Vää08] in terms of Kripke models rather than SD-models.
Propositional Dependence Logic, with that explicit name, and variants of the logic have recently been studied in, e.g., [HLSV14, HKMV15, Yan14, YV16]. The models for Propositional Dependence Logic are currently typically defined in the literature as SD-models where the set of proposition symbols in consideration is finite; thus the related SD-models are sets of finite state descriptions, i.e., finite assignments. For most purposes, it makes little difference whether SD-models with finite or infinite sets of proposition symbols are used. Similarly, it is mostly unimportant whether the models under consideration are Kripke models or SD-models. Such distinctions could, however, become more important in extensions and variants of the logics considered in this paper.
The syntax of Propositional Dependence Logic D is given by the following grammar (cf. [Vää08]),
where p,q,p_1,…,p_k∈PROP and k∈ℕ. When considering formulae D(p₁,…,pₖ;q) where k=0, we write⁶ Cφ instead of D(;q) or D(ε ; q), where ε denotes the empty sequence of proposition symbols.
Here C stands for ‘constancy’ but, as Humberstone has noted, it might be confused with ‘contingency’ which is, in fact, its opposite.
We let FOR( D ) denote the set of formulae of D. Note that formulae of D are in negation normal form, and the operator D takes as inputs only proposition symbols.
Let W be a state description model. The semantics of Propositional Dependence Logic D, to be defined below, is based on team semantics⁷, given by the following clauses (cf. [Vää08, YV16]).
Throughout this paper, the turnstile is reserved for logics based on team semantics and the turnstile for logics with a Kripke-style semantics. The reader is warned that we often use different turnstiles when comparing different logics, and the related change of turnstile may sometimes be difficult to spot at first.
(W_ D p, iff, w(p)=1for allw∈ W; W_ D p, iff, w(p)=0for allw∈ W; W_ D D(p₁,…,pₖ;q), iff, forallu,v∈ W,ifu(pᵢ)=v(pᵢ); ·, ·, holdsforall i≤k, thenu(q)=v(q); W_ D D(p₁,…,pₖ;q), iff, W=∅; W_ D φ, iff, W_ D φ and W_ D; W_ D φ, iff, U_ D φ and V_ D for some U,V⊆ W; ·, ·, such thatU∪ V=W)
We observe that W C p iff v(p)=u(p) for all u,v∈ W, i.e., the truth value of p is constant in W.
The rationale for the truth condition of D (p_1,…,p_k;q), as stated in [Vää07, p.24] and reiterated in [LV13], is as follows. Suppose we wish to maintain the same duality between D(p₁,…,pₖ;q) and D (p_1,…,p_k;q) as the one that holds for the truth conditions for p and p. We then end up with the definition that W_ D D (p_1,…,p_k;q) iff for all u,v∈ W,
where the expression above is obtained by negating the condition provided in the truth definition of D(p₁,…,pₖ;q) after the universal quantification of u and v.⁸ We then observe that according to the obtained definition, W_ D D (p_1,…,p_k;q) iff W=∅.
In other words, if we abbreviate the truth condition for p by ∀ w∈ W:Ψ and the truth condition for D(p₁,…,pₖ;q) by ∀ u,v∈ W:Ψ′, then the truth condition for p is ∀ w∈ W: and thus we define the condition for D (p_1,…,p_k;q) to be ∀ u,v∈ W:^′. How natural this choice is exactly, is a question that calls for further analysis. We will briefly discuss issues related to this matter in Section 5.
Another possible rationale for the truth definition of formulas D (p_1,…,p_k;q) can be obtained via an algebraic interpretation of formulae, as given in [Roe13]. Here formulae are associated with non-empty and downwards closed sets of SD-models. Such sets correspond to possible meanings of formulae. This approach leads to a Heyting algebra. Negation is interpreted as the pseudo-complement operation, and for the formula D (p_1,…,p_n;q) this gives an interpretation that is equivalent to the clause given above, i.e., D (p_1,…,p_n;q) is satisfied by an SD-model W iff W=∅. See [Roe13] for further details.
While team semantics may seem strange at first, the following proposition justifies its naturalness with respect to propositional logic, i.e., the sublanguage of D without formulae of the type D(p₁,…,pₖ;q) and D (p_1,…,p_k;q). Recall that the turnstile _ U refers to L_U.
Let φ be a formula of propositional logic in negation normal form. Then W_ D φ iff W,w_ U φ for all w∈ W. In other words, W_ D φ iff W_ U φ.
This proposition shows that team semantics simply lifts the semantics of propositional logic (in negation normal form) from the level of individual assignments onto the level of sets of assignments. Thus, team semantics can be used in scenarios where assertions (encoded by formulae of propositional logic) are made about sets of possible worlds, and the intention of the assertions is to claim that any world in the set satisfies the formula. We will consider examples of such scenarios in Section 5, where we discuss the relation between natural language and the logic D.
We next present Propositional Independence Logic I which was conceived as a fragment of Modal Independence Logic in [KMSV14] and studied further in, e.g., [HKVV15]. Propositional Independence Logic relates to Independence Logic of [GV13] in the same way D relates to Väänänen’s Dependence Logic. There are, of course, different kinds of notions of (propositional) independence, and the logic I provides a formal approach to a particular such notion. The logic is similar in spirit to D, being based on team semantics.
The syntax of I is given by the following grammar.
where p and each of the symbols pᵢ,rᵢ,qᵢ are proposition symbols in PROP. We denote by FOR( I ) the set of formulae of I. The numbers k and n are positive integers and m a non-negative integer. When m=0, the formula
is written (p₁,…,pₖ) I(q₁,…,qₙ). Also, when any of the three tuples of proposition symbols in the formula (p₁,…,pₖ) I_(r₁,…,rₘ)(q₁,…,qₙ) contains exactly one formula, the brackets around the tuple are usually left out, as for example in the formula p Iᵣ q.
Notice that, in line with the definition of I in [KMSV14, HKVV15], negation and I can only be applied to propositional symbols. In particular, formulae
may not occur negated. The same convention applies to independence atoms in Independence Logic [GV13].
The semantics of I is defined with respect to SD-models. Intuitively, the formula
asserts that when the truth values of the proposition symbols r₁,…,rₘ are fixed, then the tuples of truth values of (p₁,…,pₖ) and (q₁,…,qₙ) are informationally independent in a way explained further after the formal truth definition of I.
We use _ I as the semantic turnstile of I. The formal semantic clauses of I for propositional literals and Boolean connectives are exactly the same as those for the logic D, while the semantics of the formulae
is defined as follows. Let W be a state description model. We define
iff for all w₁,w₂ ∈ W that agree on r₁,…,rₘ (i.e., are such that w₁(rᵢ)=w₂(rᵢ) for each i∈{1,…,m}), there exists some v∈ W such that
Thus, the formula (p₁,…,pₖ) I_(r₁,…,rₘ)(q₁,…,qₙ) asserts that for every tuple (b₁,…,bₘ) of truth values for the propositions r₁,…,rₘ, if we restrict attention to the set S of those assignments in W that assign the values b₁,…,bₘ to r₁,…,rₘ, then the following condition holds: the tuples of truth values for (p₁,…,pₖ) and (q₁,…,qₙ) are informationally independent of each other on S in the sense that for every two assignments w₁,w₂ ∈ S, there is an assignment v∈ S that combines w₁ restricted to (p₁,…,pₖ) with w₂ restricted to (q₁,…,qₙ).
It is worth noting that, intuitively, the formula p I q can be interpreted to state that nothing new can be concluded about the truth value of p in a possible world w by finding out the truth value of q in w (and vice versa): an agent who fully knows the model W but has no idea which w∈ W is the actual world, cannot conclude anything new about the truth value of q in the actual world by learning the truth value of p in that world.
This interpretation explains the initially perhaps counterintuitive fact that the formula p I p is satisfiable even in nonempty models: W_ I p I p holds iff p is constant in W, i.e., if every assignment in W gives the same truth value to p. Indeed, p being constant means exactly that nothing new can be concluded about the truth value p in the actual world by learning the truth value of p in the actual world. If p was not constant, the truth value of p in the actual world would obviously reveal new information.
It is worth pointing out here that in the semantics of D and I, there is no explicit actual world present. Next we will consider the logics L_D and L_ I whose semantics are given in a way similar to Kripke semantics in terms of pairs (W,w), where W is a SD-model and w∈ W an assignment which can be taken to correspond to an appointed actual world.
We now introduce a new logic which extends propositional logic PL with dependence formulae D(φ₁,…,φₖ;ψ), where φ₁,…,φₖ,ψ are arbitrary formulae in the language. We call this logic Propositional Logic of Determinacy and denote it by L_D.
Recall that PROP denotes a fixed countably infinite set of proposition symbols. The formulae of L_D over PROP are defined by the following grammar.
where p∈PROP, and where the tuple (φ,…,φ ;φ) contains k+1 formulae for any k∈ℕ. We consider the Boolean connectives ,, as abreviations in the usual way. When k=0, we write Cφ instead of D(ε;φ), where ε is the empty sequence of formulae. We let FOR( L _ D ) denote the set of formulae of L_D. Notice indeed that each of the operators ,→, D can be freely used in the language of L_D; no syntactic restrictions apply.
Intuitively, D(φ₁,…,φₖ;ψ) means that the truth value of φ is determined by the set of truth values of the formulae φ₁,…,φₖ on the SD-model in consideration. In particular, Cφ means that the truth value of φ is constant in the model.
We define truth of an L_D-formula φ at a state description w in an SD-model W, denoted⁹ W,w_ D φ, inductively on the structure of formulae as follows.
We sometimes write W,w_ L _ D φ instead or even simply W,wφ.
(W,w_ D p, iff, w(p)=1; W,w_ D φ, iff, W,w_ D φ; W,w_ D φ→, iff, W,w_ D φ or W,w_ D; W,w_ D D(φ₁,…,φₖ;), iff, forallu,v∈ W,iftheequivalence; ·, ·, (W,u_ D φᵢ W,v_ D φᵢ) holds for; ·, ·, all i≤k, then(W,u_ D W,v_ D))
When an SD-model W is fixed, the assignments w∈ W can be extended to truth assignments w^ :FOR( L _ D )→ 0,1 in the natural way. The same, of course, applies to L_U.
Note that the truth definition of D(φ₁,…,φₖ;φ) extends the semantics of D in the logic D and does not here depend on the current state description w but only on the entire SD-model W. In particular, the semantics of C is as follows: W,w C φ iff for all u,v∈ W, we have that W,uφ iff W,vφ. In other words, W,w C φ iff the truth value of φ is constant in the model.
Let us rephrase the semantic definition of D above in terms of explicit functional dependence. Every formula φ∈FOR( L _ D ) determines the function t^Wᵩ:W→{0,1} such that t^Wᵩ(w):=w∗(φ). Now we have W,w D (φ_1,…,φ_n;φ) if and only if t^Wᵩ is determined by t^W_φ₁,…,t^W_φₙ on W in the sense of Definition 2.1, i.e.,
The semantics of L_D is similar to Kripke semantics (in the case where the accessibility relation of a model W is the universal relation W× W). Therefore it is natural to define for L_D the notions of validity and satisfiability analogously to the corresponding definitions in modal logic:
Let φ∈FOR( L _ D ).
The following definition is analogous to the definition of local equivalence in modal logic:
Let φ and ψ be formulae of L_D. We write φ≡_L_Dψ if the equivalence W,wφ W,w holds for all SD-models W and all w∈ W. We will often omit the subscript L_D when no confusion arises.
We note that validity in an SD-model can be expressed locally in L_D in the sense that for all assignments w∈ W, we have Wφ iff W,wφ C φ. If we know that W=∅, then Wφ iff W,wφ C φ for some w∈ W. Thus φ C φ plays the role of the universal modality. Hence we define the notation [u]φ:=φ∧Cφ as well as ⟨ u ⟩φ:=[ u ]φ (which can easily be seen to be equivalent to φ C φ). Note that [u]φ and ⟨u⟩φ are simply abbreviations of formulae of L_D, they are not formulae of L_U. (The box and diamond operators in L_U are denoted by [U] and ⟨U⟩ instead of [u] and ⟨u⟩.)
In turn, D is expressible in terms of [u] in the following sense:
Let us denote the formula on the right hand side by Δ(φ₁,…,φₖ;ψ). Consider any SD-model W. Define []_W:= w∈ W| W,w. For each w∈ W, let χ_w be the unique type over {φ₁,…,φₖ} which is true at w; in the case k=0, let χ_w:=→ p. Define
Now, suppose W,w D (φ_1,…,φ_k;). We claim that W,w u . Indeed, take any v∈ W. If W,v, then v∈[ψ]W and W,vχ_v by definition, whence W,vχ(W,). Conversely, suppose W,vχ_(W,). Then W,vχ_u for some u∈[ψ]W. Therefore W,u and χᵥ=χᵤ, i.e., for each i=1,…,k, we have that W,uφ_i iff W,vφ_i. Since W,w D (φ_1,…,φ_k;), we thus have W,u iff W,v. Therefore we infer that W,v. Thus W,vχ(W,) for every v∈ W. Hence W,w u , so W,wΔ(φ_1,…,φ_k;).
Conversely, suppose W,wΔ(φ_1,…,φ_k;). Thus W,w u for some formula χ ∈ DNF(φ_1,…,φ_k). Suppose u,v∈ W are such that W,uφ_i iff W,vφ_i for each i=1,…,k. Then W,uχ iff W,vχ, whence W,u iff W,v because W,uχ and W,vχ. Thus we have proved that W,w D (φ_1,…,φ_k;). ∎
Proposition 3.3 establishes that the operator D is definable in terms of [u]. As a particular case of this definability, we obtain that C [ u ][ u ]. Since D and [u] are interdefinable, it follows that the logics L_D and L_U are clearly equiexpressive: we can translate L_D into L_U by making use of Proposition 3.3, and, on the other hand, we can translate L_U into L_D with the help of our earlier observation that the formula φ∧Cφ simulates the universal modality. Below we will make significant use of this interdefinability of the operators D and [u].
The above results suggest obvious equivalence-preserving translations between L_D and L_U. However, while this connection between L_D and L_U is interesting and useful, the primary aim of this paper is to study the notion of determinacy and the operator D taken as a primitive. Indeed, one of our principal objectives is to compare Propositional Dependence Logic D and the new logic L_D and investigate how well they can be used in order to formalise statements about propositional determinacy and how well the two logics relate to natural language. The interdefinability of L_D and L_U can thus be regarded as an interesting fact that nevertheless will play mainly a technical role in this paper. Furthermore, neither of the above mentioned translations is polynomial, and in the more general framework of Kripke semantics (see Section 8.2 below) it is not always possible to define the box modality in terms of the determinacy operator D. We leave investigations of that more general framework for the future.
The following is a straightforward observation about L_D which we will use later on.
The logic L_D satisfies the equivalent replacement property ER with respect to the equivalence given in Definition 3.2.
We say that a class C of SD-models is definable in L_D (resp., in L_U), if there exists a formula φ of L_D (resp., of L_U) such that Wφ iff W∈C.
Let w:PROP→ 0,1 be an assignment function, and let ⊆PROP. We let w|_Φ denote the restriction of w to Φ, i.e., the function f:Φ→{0,1} defined so that f(p)=w(p) for all p∈Φ. We define W|_Φ:={w|_Φ | w∈ W}.
Two SD-models W₁ and W₂ are Φ-equivalent, denoted W₁≡_Φ W₂, if W₁|_Φ=W₂|_Φ.
A class of SD-models C is closed under finite propositional equivalence, if the following conditions hold.
The first condition above has been included for technical convenience. Note that the empty model satisfies every formula of L_U and L_D.
A class of SD-models is definable in L_U iff it is closed under finite propositional equivalence.
Suppose a class of SD-models C is definable in L_U by some formula φ and let ⊆PROP be the set of proposition symbols that occur in φ. Then for all SD-models W₁ and W₂, if W₁ ∈C and W₁≡_Φ W₂, then W_1φ and thus W_2φ, whence W₂ ∈C. Thus C is closed under finite propositional equivalence.
Now, suppose C is closed under finite propositional equivalence and let ⊆PROP be a finite set such that for all nonempty SD-models W₁ and W₂, if W₁ ∈C and W₁≡_Φ W₂, then W₂ ∈C. Define a characteristic formula φ_W of a model W=∅ as follows. For each w∈ W, let χ_w be the unique propositional type in Conj() such that W,wχ_w. Define
which of course can be regarded as a finite formula since we can eliminate repeated conjuncts and disjuncts.
Let
which again can be regarded as a finite formula.
Then C is defined by Δ(Φ,C). Indeed, Δ(Φ,C) is true in every model W∈C. Conversely, every SD-model U=∅ satisfying Δ(Φ,C) satisfies some disjunct, i.e., some characteristic formula φ_W of some model W∈C∖{∅}, because the truth value of each disjunct of Δ(Φ,C) is constant across the worlds of a given SD-model. Clearly U≡_Φ W, whence we have U∈C. ∎
Consequently, we obtain a characterisation of the expressive power of L_D:
A class of SD-models is definable in L_D iff it is closed under finite propositional equivalence.
Let =∅ be a finite subset of PROP. Let C denote the set of all SD-models in restriction to Φ, i.e., the set {W|_Φ | Wis an SD-model}. We call C the set of Φ-models and denote it by M(Φ). Let S⊆M(Φ). We say that S is definable in L_U (L_D) in restriction to M(Φ), if there is a formula φ of L_U (L_D) Such that for all W∈M(Φ), we have Wφ iff W∈S.
L_U and L_D are expressively complete in the sense that for any finite nonempty ⊆PROP and any S⊆M(Φ) with ∅∈S, the set S is definable in restriction to M(Φ) in both L_U and L_D.
The claim for L_U is established by an argument that is almost identical to the proof of Proposition 3.7. The claim for L_D then follows by the equiexpressivity of the logics L_D and L_U. ∎
We have defined the logic of L_D as an extension of propositional logic PL with the operator D. Next we introduce Propositional Logic of Independence L_ I which extends PL in a similar way, but now with the operator I instead of D. The logic L_ I relates to Propositional Independence Logic I analogously to the way L_D relates to Propositional Dependence Logic D.
The language of Propositional Logic of Independence L_ I is given by the following grammar.
where p∈PROP, and each of the three tuples (φ,…,φ) in the expression
is a finite tuple of formulae; the tuples in the same expression may be of different lengths, but only the tuple in the subscript may possibly be empty. Instead of writing (φ,…,φ) I_∅ (φ,…,φ), we simply write (φ,…,φ) I(φ,…,φ). As in L_D, we consider the Boolean connectives ,, definable as usual. Sometimes we leave out brackets of formulae of L_ I, following the convention that the operator I has a higher priority than all binary connectives, while negation has a higher priority than all other operators (including I). We let FOR( L _ I ) denote the set of formulae of L_ I.
The semantics of L_ I is similar to that of L_D and also defined with respect to SD-models W and assignments w∈ W. Propositional symbols and Boolean operators are interpreted exactly as in L_D. To define the semantics for I, recall that in an SD-model W and for a logic with a Kripke-style semantics, each w∈ W can be extended to a truth function w∗ from the set of formulae to {0,1} such that w∗(φ)=1 iff W,wφ. The truth definition of the operator I extends the one in the logic I as follows. We define W,w_ L _ I (φ_1,…,φ_k) I _(θ_1,…,θ_m)(_1,…,_n) iff for all w₁,w₂ ∈ W that agree on θ₁,…,θₘ (i.e., are such that w∗₁(θᵢ)=w∗₂(θᵢ) for all i∈{1,…,m}), there exists some v∈ W such that
Thus the operator I of L_ I extends I of I so that in L_ I the operator can be applied to all formulae, not only proposition symbols. Note that the semantics of I (which we defined with respect to the model W and world w∈ W) does not directly depend on the world w but is global in the model.
Analogously to the conventions fixed in Definition 3.1 for L_D, we say that a formula φ of L_ I is valid in a model W (denoted W_ L _ I φ), if φ is true in every world of W, and that φ is valid (denoted _ L _ I φ) if W_ L _ I φ for every model W. Two formulae φ and ψ of L_ I are equivalent, denoted φ≡L I ψ, if the equivalence W,w_ L _ I φ W,w_ L _ I holds for all models W and all w∈ W.
The following two lemmas are straightforward to prove. For Lemma 4.2, recall the definition of Φ-equivalence of SD-models from Definition 3.5.
The logic L_ I satisfies the equivalent replacements property ER with respect to ≡L I.
Let φ be a formula of L_D or L_ I. Let Φ be the set of proposition symbols occurring in φ. For nonempty models W and U and points w∈ W and u∈ U, if W≡_Φ U, then we have W,wφ iff U,uφ.
Since both logics L_D and L_ I are interpreted with respect to SD-models W and assignments w∈ W, it is easy to compare them. We define the following simple translation t from L_D into L_ I:
In particular, we have t(Cψ):=t(ψ) I t(ψ). (Recall our discussion in Section 2.6 concerning formulae of the type p I p.)
Now we make some simple but interesting observations.
L_D embeds into L_ I and D embeds into I, in the following sense.
The proof of the first claim is straightforward, using the translation t defined above. The second claim is also straightforward, based on the obvious variant t′ of the translation t that keeps proposition symbols and Boolean connectives the same and translates D(p₁,…,pₖ ; q) to q I_(p₁,…,pₖ) q. ∎
We note that the translation from D into I mentioned in the above proof is well known from the literature on team semantics.
We define [u′]φ to be an abbreviation for the formula φ∧ φ I φ of L_ I, and we let ⟨u′⟩φ denote [ u ^′]φ. Note that [u′] corresponds to the universal modality in an obvious way. To see how the independence operator I can be expressed in terms of ⟨u′⟩, consider a formula (φ₁,...,φₖ) I_(θ₁,...,θₘ)(ψ₁,...,ψₙ) of L_ I. Recall the notation Conj() from Section 2.2, including also the special case for Φ=∅ which stipulates that Conj(∅)= → p. Define
It is easy to see that the bottom formula describes the semantics of the operator I in terms of ⟨u′⟩ in a rather direct way. ∎
We will complete the expressivity analysis of the logics L_D, L_ I, D, and I in Section 6.
In this section we interpret the logics D and L_D in relation to natural language and compare their respective properties. We will not discuss I explicitly here, but since I is technically quite similar to D, many of the observations below concerning D apply to I as well. Here we take Wφ (respectively, W) to mean that a sensible agent who considers W to be the set of all possible scenarios, considers φ (resp., ψ) to hold. This kind of reading of SD-models as information states is in line with the the intuitions of modal logic and also inquisitive logic.
The principal argument of the section is that L_D is—at least in some important respects—a better match than propositional dependence logic D with natural language intuitions concerning statements about logical determinacy. It is sufficient for our purposes to consider formulae with only the connectives and ∨ together with determinacy assertions of the type D(p;q). We make the assumption that the desirable natural language counterparts of and ∨ should always be “it is not the case that” and “or,” respectively. Formulae D(p;q) should correspond to assertions stating that “whether P holds, determines whether Q holds.” Here P and Q denote suitable natural language interpretations of p and q. A different kind of analysis would arise if, for example, was to be read as “it is never the case that” or “it is impossible that.”
Our argument will proceed as follows. We first argue that the semantics of formulae of the type p∨ q is a good match with natural language intuitions in both logics L_D and D. We then turn to examples concerning formulae of the type D(p;q), and again argue that the semantics of both logics is reasonable. (In this context we also briefly discuss more complex formulae of the type D(p,q;r), but this is not crucial from the point of view of our discussion.) We then argue that, despite both p∨ q and D(p;q) having a reasonable semantics in D, formulae of the type D(p;q)∨D(p′;q′), which combine ∨ and D, are problematic. In fact, we show this even for the formula D(p;q)∨D(p;q), where both disjuncts are the same. We then continue by arguing that L_D, in turn, gives natural interpretations for these problematic examples. Finally, we briefly discuss formulae of the type D (p;q).
As we saw in the previous section (cf. Proposition 2.3), team semantics is simply classical semantics lifted to the level of sets: if φ is a formula of propositional logic PL, then, in the setting of team semantics, Wφ simply means that each world in W satisifies φ. Even the semantics of disjunction ∨, which may appear strange at first, makes perfect sense from that perspective. Let us consider an example where team semantics seems to give a correct interpretation (from the natural language perspective) to the disjunctive formula p∨ q.
Consider the following propositions.
Assume a set W={w₁,w₂,w₃} of possible scenarios has been identified by a clinician after inspecting a patient with vertigo, where
w₁(p)=1,w₁(q)=0; w₂(p)=0,w₁(q)=1; w₃(p)=1,w₃(q)=1.
The set W={w₁,w₂,w₃} is assumed here to be the set of exactly all scenarios which the clinician considers possible. The clinician has informed the patient about his situation, so the patient also considers W to be the set of all possible scenarios. To summarize the discussion with the patient, and to repeat what the situation is, the clinician then states to the patient:
``So, you have an ear infection or high blood pressure."
The clinician seems to be asserting that “W p q,” i.e., that the set W of all possible scenarios splits into worlds that satisfy p and worlds that satisfy q. Thus team semantics works correctly here. The interpretation “W p or W q” has a different meaning, which is false in this case.
In this example, the assertion p∨ q was made about the set W of possible states of affairs, i.e., sets of assignments. Since team semantics is based on sets of assignments (rather than individual assignments), it is a natural framework for interpreting determinacy atoms D(p₁,…,pₖ;q). We next give natural language examples that should convince the reader that the semantics of the operator D given by D is a good match with intuitions concerning statements about propositional determinacy.
Consider now a scenario with two containers of water in two laboratory ovens. Fix the following propositions.
Assume the setting is encoded by the set W={w₁,w₂}, with one possible world for each container, such that w₁={p,q} and w₂=∅. By w₁={p,q} we of course mean that w₁(p)=1 and w₁(q)=1, and analogously, w₂=∅ means that w₂(p)=0 and w₂(q)=0.
Consider the following assertion:
“Whether the temperature is over 100^ Celsius
determines whether the water is boiling.”
It is natural to interpret the assertion to mean that W D (p;q). Thus the semantics of D seems to work fine here. For another example, extend the above setting with a third oven w₃ with a water container and a new proposition r which asserts that the air pressure in the oven is over 1 bar. Let W={w₁,w₂,w₃}, where
This time the temperature being over 100^ Celsius does not determine whether the water is boiling, i.e., W D (p;q), because both w₁ and w₃ satisfy p, but the two worlds disagree on the truth value of q. However, we do have that W D (p,r;q). By adding yet another world w₄={p,q,r} encoding a fourth oven, we end up with a laboratory where W D (p,r;q).
A scenario where D(p,r;q) seems to hold universally, i.e., in every correctly designed set W of possible worlds, can be obtained for example by considering a setting where each world is associated with a balance scale and two equally heavy weights. Let p encode the assertion that exactly one weight has been placed on the left tray of the balance scale, and r the corresponding assertion concerning the right tray; q is the assertion that the scale is in balance. Now, indeed, D(p,r;q) holds for any collection of physically possible worlds, with q being true exactly when either p and r are both true or when they are both false.
We have seen that team semantics works fine on simple disjunctive formulae p∨ q and and determinacy statements D(p;q). We next combine disjunctions and determinacy statements and show that this leads to problematic interpretations from the point of view of natural language (cf. [Kuu14]).
Let p denote the assertion that the sun is shining and q the assertion that it is winter. Consider a setting where W={w₁,w₂,w₃,w₄}, with all possible distributions of truth values for p and q realized. Now clearly W D (p;q), so whether the sun is shining does not determine whether it is winter. However, now W D (p;q) D (p;q) holds in D. This seems strange. Consider the following translation of the formula D(p;q)∨D(p;q) into natural language.
The intuitively correct interpretation of the above statement seems to be the (indeed false) assertion that
“W D (p;q) or W D (p;q),”
rather than the (true) assertion “W D (p;q) D (p;q)” suggested by team semantics. The natural language statement “Whether the sun is shining determines whether it is winter, or, whether the sun is shining determines whether it is winter” seems obviously false. Therefore team semantics here gives an undesired interpretation to the formula D(p;q)∨D(p;q). In fact, we observe that the formula φ:=D(p;q)∨D(p;q) is a validity of D, i.e., we have Wφ for every SD-model W.
For another example, consider the formula D(p;q)∨D(r;q), where p, q and r stand for “It is dark”, “John is at home”, and ”It is cold” respectively. Assume all distributions of truth values of the propositions p,q,r are realized in W. Now W D (p;q) D (r;q) holds in D. This is again counterintuitive from the natural language point of view. Like the formula D(p;q)∨D(p;q), also the formula D(p;q)∨D(r;q) is a validity of D. In fact, every formula of the type D(p₁,…,pₖ;q)∨D(r₁,…,rₙ;q) is a validity of D, because every SD-model W can be split into sets U,V⊆ W such that U∪ V=W and each assignment in U satisfies q while each assignment in V satisfies q.
Before we discuss how L_D deals with the above formulae, we note once more that our analysis assumes that ∨ should correspond to the natural language “or.” We do not want to claim that the natural language word or has always a unique interpretation.¹⁰ However, L_D works quite nicely in the above examples, as we will next demonstrate.
There exist arguments essentially promoting the uniqueness of the meaning of disjunction (see [Alo16] for an overview). On the other hand, already for example the inclusive and exclusive modes of or are sometimes taken to demonstrate ambiguity of disjunction. While we wish to refrain from taking any definite position in this debate, this issue is worth mentioning here. (We also want to point out that in the formal proofs and definitions of this article, the word or is used in the standard inclusive fashion as is customary in standard mathematical practice.)
Concerning the formula p∨ q in the beginning of the section, we have W p q iff W p q. Also, for determinacy statements φ:=D(p₁,...,pₖ;q), we have Wφ iff Wφ. Finally, for the problematic formulae D(p;q)∨D(p;q) and D(p;q)∨D(r;q), the semantics of L_D gives the desired interpretations: we have W D (p;q) D (p;q) iff (W D (p;q) or W D (p;q)) and similarly for the formula D(p;q)∨D(r;q).
We will not try to give an elaborated account of how well exactly L_D corresponds to natural language, but it is essential to notice that L_D can be considered to have a similar level of naturalness as standard S5 modal logic or modal logic with the universal modality. The reason for this is that a similar Kripke style semantics is used, and furthermore, it can be argued that L_D is simply a fragment of the modal logic S5. This is because determinacy statements are naturally definable in terms of statements about possibility: simply consider the direct natural language translation of the equivalence
where ⟨u⟩ should be read as “it is possible that.” The natural language translation of this equivalence indeed seems intuitively immediately appealing, and importantly, the equivalence essentially just states the formal semantics of D(p;q) (determinacy) in terms of the diamonds ⟨u⟩ (possibility), thus demonstrating that statements of determinacy can be very naturally and directly formulated in terms of possibility statements. Therefore L_D can be considered a fragment of modal logic (with the universal or S5 modality in the particular case of this paper), and the level of correspondence between natural language and L_D is similar to the corresponding relationship for (S5) modal logic. We note that the restriction to S5 frames is of no importance here. We also note that the above equivalence deals only with the simple determinacy formula D(p;q) but it is easy to generalize our argument to more complex formulae. (See also Proposition 3.3.)
In addition to disjunction ∨, also the semantics of negation in D can be counterintuitive if the reading “it is not the case that” is desired for . For example, let p and q denote the assertions “the Riemann hypothesis holds” and “it is raining,” respectively. Let W be a nonempty SD-model. Now we have W D (p;q) in D. In L_D, we have W D (p;q) in (for example) every model W where the truth value of p is the same in every possible world and where q is true in some worlds and false in others.¹¹
Perhaps alternative readings of could work better in D. For example, in [Kuu15], the reading “it is never the case that” for the negation of D is suggested. This reading is not meant to necessarily have any temporal connotations, but instead could alternatively be read as “it is impossible that.” We shall not try analyze here how well such a reading could actually work.
Finally, concerning L_D, it is worth noting the triviality that just as in S5, Wφ is not in general equivalent to Wφ, because Wφ means that W,wφ for all w∈ W. Analogously, Wφ is not in general equivalent to (Wφ or W). We note that, by Proposition 2.3, we have Wχ iff Wχ for all formulae of propositional logic in negation normal form, so D and L_D are similar with respect to formulae of propositional logic PL.
To give an example of how the semantics of works in D and L_D in the context of formulae of PL, let p and q denote the assertions “John has a cat” and “John is married,” respectively. Assume a scenario where it is agreed that the possible worlds are w₁={p} and w₂=∅, i.e., John may or may not have a cat, but he is definitely not married. Let W={w₁,w₂}. The assertion “It is not the case that John is married” seems correct, and indeed, we have W q. Note, however, that even though W p, the claim “It is not the case that John has a cat” would seem odd. To make the claim W p, one would have to assert, e.g., that it is possible that John does not have a cat, or that it is not necessarily the case that John has a cat.
We have earlier observed (Proposition 4.3) that L_D embeds into L_ I, and also that D embeds into I. In this section we will complete our discussion concerning the expressive powers of the logics L_D,L_ I ,D and I.
Let φ,∈FOR( D )∪FOR( I ). We write φ≡ₜₑₐₘ ψ if the equivalence Wφ W holds for all SD-models W. The first result we wish to point out is well-known; we prove it for the sake of completeness.
The logic I does not embed into D: there exists a formula φ of I such that for all formulae ψ of D, the equivalence φ≡ₜₑₐₘ ψ fails.
It is well-known, and easy to show, that D satisfies the following downwards closure property: if W_ D φ and U⊆ W, then we have U_ D φ.
Now, define an SD-model W={w₁,w₂,w₃,w₄} where the four states represent all truth assignments for propositions p and q. More precisely, let w₁(p)=w₁(q)=w₂(p)=w₃(q)=1 and w₂(q)=w₃(p)=w₄(p)=w₄(q)=0. Define U:={w₁,w₄}. Consider the formula φ:=p I q. It is clear that Wφ and Uφ. Therefore, due to the downwards closure property of D, no formula ψ of D can satisfy the equivalence φ≡ₜₑₐₘ ψ. ∎
While D embeds into I but not vice versa, the situation is different for L_D and L_ I. In Section 2.6 we established that L_D embeds into L_ I. We now define a translation showing that L_ I embeds into L_D, too. While it is straightforward to observe, based on Propositions 3.7 and 3.9, that L_ I indeed embeds into L_D, the concrete translation below will be of interest later on when we discuss compositional translations (to be defined) between the logics under investigation. We define the following translation s:FOR( L _ I )→FOR( L _ D ):
For the special case where m=0, recall that Conj(∅)= → p. Now, let
s((φ₁,…,φₖ) I_(θ₁,…,θₘ)(ψ₁,…,ψₙ)):=
It is easy to see that the translation of the operator I given by the formula above describes the meaning of I quite directly in terms of ⟨u⟩.
The proof of the next claim is straightforward, using the translation s defined above.
L_ I embeds into L_D i.e., for each formula φ of L_ I, there exists an equivalent formula ψ of L_D in the sense that for all W and all w∈ W, we have W,wφ iff W,w.
Next we will show that the team-semantics-based logic I is strictly contained in the Kripke-style logic L_D in the following sense.
The claim 1 above is essentially obvious, since all classes of models definable in I are closed under finite propositional equivalence, and due to Proposition 3.7, L_D can define all such model classes. However, we will provide an explicit and effective translation of I into L_D which is interesting in its own right and also elucidates the semantics of I. Furthermore, despite the simplicity of our translation, we will show in Section 6.4 that there does not exist a compositional translation from I into L_D.
Recall once again the notion of a type normal form formula and related notions from Section 2. Let Φ be a finite nonempty set of proposition symbols and χ= χ_1,…,χ_k a formula in DNF(). We let SPLIT(χ) denote the set of pairs (α,β) of type normal form formulae in DNF() such that if α= α_1,…,α_m and β= β_1,…,β_n, then we have
Let χ∈DNF(). We define the following translation t_χ from I into L_D:
We then define t_χ((p₁,…,pₖ) I_(q₁,…,qₘ) (r₁,…,rₙ)) :=
If φ is a formula of I and Φ the set of proposition symbols in φ, we let χ(φ) denote the formula in DNF() that contains as disjuncts all types over Φ. Note that the formula χ(φ) is a tautology.
We then prove that our translation of I into L_D preserves truth.
W_ I φ iff W_ L _ D t_χ(φ)(φ).
Let φ be a formula of I and W a model. Let Φ be the set of proposition symbols that occur in the formula φ. If χ∈DNF(), we let W_χ denote the set of worlds in W that satisfy χ. We will show that for every χ∈DNF() and every subformula ψ of φ, we have
The claim of the Lemma will then follow, as W_χ(φ)=W.
The proof proceeds by induction on the structure of ψ. The cases for proposition symbols, negated proposition symbols and conjunctions are straightforward. The argument for I is easy, as our translation in that case captures quite directly the semantics of I.
We now proceed to the case ψ=ψ′ ∨ψ^′′. When going through the argument below, it helps to keep in mind the trivial technicality that for an SD-model U and a proper subset S of PROP, there may exist several assignments in U that are equivalent with respect to S, i.e., assignments that satisfy exactly the same propositions in S (but differ elsewhere).
Assume that W_χ_ I ^′^′′. Thus there exist sets S′,S^′′ ⊆ W_χ such that S^′_ I ^′ and S^′′_ I ^′′, and furthermore, S′ ∪ S^′′=W_χ. Therefore there exists a pair (α,β)∈SPLIT(χ) such that S′ ⊆ W_α and S^′′ ⊆ Wᵦ, and furthermore, W_α≡Φ S′ and Wᵦ≡Φ S^′′ (recall Definition 3.5). Therefore clearly W_α^′ and W_β^′′. Hence, by the induction hypothesis, we have W L _ D t_α(^′) and W L _ D t_β(^′′). Thus W_ L _ D t_α(^′) t_β(^′′), whence we conclude that W_ L _ D t_χ(^′^′′).
For the converse, assume that W_ L _ D t_χ(^′^′′). Therefore there exist type normal form formulae α,β such that (α,β)∈SPLIT(χ), and furthermore, W_ L _ D t_α(^′) and W_ L _ D t_β(^′′). By the induction hypothesis, we have W_α_ I ^′ and W_β_ I ^′′. Since (α,β)∈SPLIT(χ), we have W_α ∪ Wᵦ=W_χ, and therefore W_χ_ I ^′^′′. ∎
We are now ready to prove the following theorem.
The logic I is strictly contained in L_D, i.e.:
By Lemma 6.3 there exists an effective translation from I into L_D. Hence we only need to prove the second claim of the theorem. In fact the claim follows relatively easily from Proposition 3.7 and the proof of Theorem 4.2 of [KMSV15], but we will establish the claim here explicitly.
We will show that the L_D-formula C p is not expressible in I, i.e., there is no formula ψ of I such that W_ I iff W_ L _ D C p. We first define two models U and U′, where U consists of two worlds, one satisfying p and the other one not, and U′ consists of single world that does not satisfy p. Furthermore, for all other proposition symbols q, we define q to be false in each world of the models U, U′.
We then show by induction on the structure of formulae that for all φ∈FOR( I ), we have
For the literals p and p this is immediate, as U_ I p and U_ I p. For other literals q, q, etc., the implication holds because U_ I q and U^′_ I q. In order to deal with the operator I, notice that U′ satisfies all formulae of the type (p₁,…,pₖ) I_(q₁,…,qₘ)(r₁,…,rₙ), since the model U′ contains only a single world.
The case for ∧ follows immediately by the induction hypothesis.
We then consider the case for ∨. Assume that U_ I ^′. Therefore there exist sets S,S′ ⊆ U such that S_ I and S^′_ I ^′, and furthermore, S∪ S′=U. We may assume, by symmetry, that S contains the assignment in U that does not satisfy p. We consider two cases.
holds. Therefore U^′_ I ^′.
holds again, and we hence conclude that U^′_ I ^′.
Finally, note that U_ L _ D C p, while U^′_ L _ D C p. Therefore C p cannot be expressible by a formula of I. ∎
The logics D and I are both strictly contained in both L_D and L_ I.
In summary, we have shown that D<I<L_D≡L_ I, where < denotes strict containment and ≡ equi-expressivity. We have also observed that L_D and L_ I are expressively complete in the sense that they can define exactly all classes of SD-models closed under finite propositional equivalence. (See Definition 3.6 for the exact specification of finite propositional equivalence.)
Let t∗ denote the translation from I into L_D we defined above. Recall that in addition to t∗, we have also defined the translations t:FOR( L _ D )→FOR( L _ I ) and s:FOR( L _ I )→FOR( L _ D ). Furthermore, in the proof of Proposition 4.3, we described a translation from D into I; let us denote that translation by t′.
In this section we will take a closer look at the four translations t∗,t,s and t′. We will establish that, in a certain sense, the translation t∗ is essentially different from the other three.
We begin by defining a notion of a syntactically regular logic suitable for our purposes. To this end, we first need some auxiliary definitions. Let ℕ∗ be the set of all finite sequences of numbers in ℕ (including the empty sequence). Let C be a finite or countably infinite set of operator symbols. Let d be a function that associates with each symbol in C a nonempty subset of ℕ∗; the set d(c) is called the arity type set of c. For example, in L_ I, the operator I always operates on three tuples of formulae, with the middle tuple being the only one allowed to be the empty tuple, and thus the arity type set associated with I is ℕ₊ × ℕ × ℕ₊.
The set C together with the function d give rise to a set FOR(C,d) of formulae, which is defined to be the smallest set S such that the following conditions hold:
We call FOR(C,d) the syntactically regular set of formulae defined by C and d. We call a logic syntactically regular if the set of formulae of the logic is a syntactically regular set of formulae for some set C and a related function d. Any logic whose set of formulae is a subformula closed subset of some syntactically regular set of formulae, is called a syntactically subregular logic. Closure of a formula set F under subformulae obviously means that if c((φ₁,₁,…,φ_1,n₁),…,(φₖ,₁,…,φ_k,nₖ)) ∈ F, then each of the formulae φᵢ,ⱼ is in F. For the sake of simplicity, we will below mainly talk about regular and subregular (rather than syntactically regular and syntactically subregular) logics.
It is easy to see that L_D and L_ I are essentially regular logics. Similarly, D and I are essentially subregular logics.¹²
We acknowledge that strictly speaking L_D and L_ I are not syntactically regular because—to give one reason—the connective → uses infix rather than prefix notation. However, it would be a trivial exercise to redefine the syntax of these logics in the required way, and therefore we consider them syntactically regular. Similarly, D and I are considered syntactically subregular.
Let L be a subregular logic and c an operator symbol of L. Let d be the function that associates the operators of L with the related arity type set, and let x∈ d(c). The pair (c,x) is called a base operator of L. For example, the operator D of L_D can act on tuples of formulae of all positive finite lengths, so each pair (D,i), where i is a (singleton tuple containing a) positive integer, is a base operator. In contrast, the operators and → of L_D are both associated with only a single arity type, and thus we can directly regard and → as base operators.
We now define the notion of a compositional translation from one subregular logic to another. Intuitively, a compositional translation from a logic L to a logic L′ has the property that each base operator of L is described in L′ in a uniform way. Therefore the translation in some sense acts only on the base operators of L rather than directly on individual formulae. Thus a compositional translation can be considered to be, in a sense, simple and direct. For further discussion on compositional translations, see [Jan97].
Assume φ₁,…,φₖ, where k∈ℕ, are distinct formulae of a subregular logic L. Assume ψ(φ₁,…,φₖ) is a formula of L obtained from φ₁,…,φₖ by composing these formulae with some collection of base operators. Let X₁,…,Xₖ be novel symbols. Then ψ(X₁,…,Xₖ) is called an operator term of L; the operator term is obtained by replacing the original ground instances of the formulae φ₁,…,φₖ in ψ(φ₁,…,φₖ) by X₁,…,Xₖ, respectively. (For example, if φ₁:=p and φ₂:=q, and if ψ(φ₁,φ₂):=(p→ q)∨ p I q, then we obtain the operator term (X₁ → X₂)∨ X₁ I X₂ by replacing φ₁ with X₁ and φ₂ with X₂.)
Let L and L′ be subregular logics. We identify L and L′ with their respective sets of formulae. A translation T:L→ L′ is compositional, if for each base operator (c,(n₁,…,nₖ)) of L, there exists an operator term
of L′ such that for all tuples (φ₁,₁,…,φ_1,n₁),…,(φₖ,₁,…,φ_k,nₖ) of formulae of L such that c((φ₁,₁,…,φ_1,n₁),…,(φₖ,₁,…,φ_k,nₖ)) ∈ L, we have
i.e., the translated formula is obtained by substituting each symbol Xᵢ,ⱼ in ψ by T(φᵢ,ⱼ). Furthermore, it is required that for each proposition symbol p in the syntax of L, the translation T(p) contains no other proposition symbols except for p. This ensures that the translation T(φ) of any formula φ contains no other proposition symbols except for those in φ itself. This is a natural requirement and can be essential for example when considering SD-models with a finite propositional signature, i.e, models that interpret only a finite number of proposition symbols. We note that in the team semantics literature, SD-models are in most cases indeed defined to interpret only finitely many proposition symbols.
The symbols Xᵢ,ⱼ in the above definition should be regarded as placeholders in the operator term ψ(X₁,₁,…,X_k,nₖ). Intuitively, the operator term ψ(X₁,₁,…,X_k,nₖ) provides a “uniform description” of the base operator (c,(n₁,…,nₖ)) of L in L′. The above definition of a compositional translation is suitable for the purposes of the current paper and follows standard principles of compositional translations.
Note that our translations t:FOR( L _ D )→FOR( L _ I ) and s:FOR( L _ I )→FOR( L _ D ) are indeed compositional, as is the translation t^′:FOR( D )→FOR( I ) from the proof of Proposition 4.3. However, the translation t^ :FOR( I )→FOR( L _ D ) is not compositional, despite being relatively simple. In fact, it will turn out that a sound compositional translation from I into L_D or L_ I is not possible. To see this, it is sufficient (due to the existence of the translations t′ and s) to show that D does not translate compositionally into L_D. The following theorem does exactly that.
There exists no compositional translation T from D into L_D which is sound with respect to SD-models in the sense that for any SD-model W and any formula φ of D, we have Wφ iff W T(φ).
Let S be an SD-model and χ₁,χ₂ formulae of L_D. We say that χ₁ and χ₂ are locally equivalent in S, if for all w∈ S, it holds that S,wχ_1 iff S,wχ_2.
Suppose, for the sake of contradiction, that a compositional translation T from D into L_D exists. Consider an SD-model V consisting of exactly two assignments, one satisfying p and the other one not. Then fix a proposition symbol q so that for each w∈ V, the assignment w satisfies q if and only if w does not satisfy p. For all other proposition symbols r∈PROP∖ p,q, we assume that neither of the worlds in V satisfies r. We then define an SD-model U which is the same as V but with the interpretation of q redefined so that q is satisfied by u∈ U if and only if u satisfies p. Let W∈{U,V}. We will prove the following claims about W.
We begin with the first claim. If T(r) was satisfied by both points of W, we would have W T(r) and thus W r, which is a contradiction. If T(r) was satisfied by exactly one point of W, we would obtain a contradiction due to the fact that T(r) is required by definition to contain no other proposition symbols except for r, and since w(r)=0 for both points w∈ W, the situation where only one of the points in W satisfies T(r) is impossible by symmetry. Therefore the first claim holds.
Concerning the second claim, we first observe that T(q) cannot be satisfied by both points of W, because if it was, then we would have W T(q) and thus W q, which is a contradiction. Now assume that neither of the points of W satisfies T(q). Then, using the first claim established above (claim 1.), the formulae T(q) and T(r), for r∈PROP∖ p,q, are locally equivalent in W. Therefore we can now infer, by the following argument, that the formulae T (Cq) and T (Cr) must also be locally equivalent in W.
Since the translation T is compositional, there exists an operator term ψ(X) that describes the translation of the operator C, and thus we have T (Cq)=ψ(T(q)) and T (Cr)=ψ(T(r)). Since we know that T(q) and T(r) are locally equivalent in W, we immediately observe that ψ(T(q)) and ψ(T(r)) are also locally equivalent in W. Thus T (Cq) and T (Cr) are locally equivalent in W.
Hence, as W C q and thus W T( C q), we infer that W T( C r). Therefore W C r. This is a contradiction, and thus the second claim holds.
Concerning the third claim, assume first that T (Cp) is satisfied by both points of W. Then W T( C p), whence W C p, which is a contradiction. Assume then that neither of the points in W satisfies T (Cp). Therefore, using the first claim (claim 1. above), T (Cp) and T(r) are locally equivalent in W. As W C p C p, we have W T( C p C p) and thus W^′(T( C p),T( C p)), where ψ′(X,Y) is the operator term for ∨ which demonstrates that T is indeed a compositional translation. Since T (Cp) and T(r) are locally equivalent in W, we infer that W^′(T(r),T(r)). Thus W r r, which is a contradiction. Therefore we conclude that T (Cp) is satisfied by exactly one point of the model W, and hence the third claim holds.
We have now proved each of the above three claims. By the last two of the three claims, recalling that T (Cp) can only use the proposition symbol p and T(q) the symbol q, we now observe that exactly one of the following conditions hold.
We first assume that the first one of these conditions holds. Therefore, since U C p C p and thus U T( C p C p), we may now conclude that U T(q q) as follows.
We know that T (Cp) and T(q) are satisfied by exactly the same single point in U. We know also that U T (Cp Cp). Thus U^′(T (Cp),T (Cp)), where ψ′(X,Y) is the operator term for ∨. Since T (Cp) and T(q) are locally equivalent in U, we therefore have U^′(T(q),T(q)). Since ψ′(T(q),T(q))=T(q∨ q), we have U T(q q).
Since U T(q q), we have U q q, which is a contradiction. Thus we turn to the case where T (Cp) and T(q) are locally equivalent in V. Similarly to the above, since V C p C p and thus V T( C p C p), we infer using the formula ψ′(X,Y) that V T(q q). Therefore V q q, which is a contradiction. ∎
We finish this section by mentioning some relevant related results in the literature on compositional translations and uniform definability of operators. Section 3.5 of [Cia09] establishes that in the propositional inquisitive logic InqL, which is a team-based logic equi-expressive with D, none of the primitive operators is definable in terms of the others. In [Yan16], it is shown that the implication and disjunction connectives of InqL are not uniformly definable in D, and thus no compositional translation from InqL into D is possible. In [Gal13], it is shown that the so-called weak universal quantifier ∀¹ is not uniformly definable in first-order dependence logic.
In this section we provide sound and complete axiomatizations for L_D and L_ I. We begin by axiomatizing L_C, the fragment of L_D with only operators C instead of general determinacy operators D.
Recall that Cφ stands for D(ε;φ), where ε is the empty sequence of formulae. Recall also the abbreviation [u]φ:=φ∧Cφ and the equivalence C [ u ][ u ] that intuitively demonstrate that the universal modality [U] and C are expressible in terms of each other.
We denote the fragment of L_D that extends propositional logic PL with C by L_C. The operator C has been studied previously and in a more general setting as a “non-contingency” operator, and also—in epistemic logic—as a “knowing whether” operator, see [FWvD15] and the references therein.
We next present a sound and complete axiomatic system AX( L _ C ) that captures the validities of L_C. Several proofs of completeness of equivalent axiomatizations have already been provided in the literature, starting with [MR66] and considered again in, e.g., [Dem97]. For historical references and recent related work on axiomatizations of C, see the above mentioned reference [FWvD15]. Nevertheless, we will present here yet another, simple and intuitive axiomatization with a purely syntactic proof of completeness by means of reduction to the completeness of S5 (or L_U). We will then use the completeness of AX( L _ C ) to obtain complete axiomatizations for L_D and L_ I.
The axiomatic system AX( L _ C ) is defined as follows.
Axiom schemes:
Inference rules:
We will denote derivability in AX( L _ C ) by _ C.
The axiomatic system above is not minimal. For instance, Ax4(C) can be left out¹³, as it is derivable (though, not quite trivially) from the others. Nevertheless, rather than providing a derivation of the axiom (which would not be in the focus of this paper), we prefer to keep it in the system.
Thanks to Jie Fan for noting that.
The following inference rule, which preserves SD-validity, can be used in AX( L _ C ):
NECC: If _ C φ then _ C C φ.
If _ C φ, then _ C φ→ p by PL (propositional logic). Thus _ C C φ C → p by EQC, whence _ C C φ by using Ax1(C) and PL. ∎
Now, recall the following well-known complete S5 axiomatization for L_U.
Axiom schemata:
Inference rules:
We will denote derivability in L_U by _S5.
To show completeness of AX( L _ C ), we first extend the intuitive interdefinability of C and the universal modality to a translation φφ^+ from L_C into L_U and a translation φφ^ from L_U into L_C.
The translation φφ^+ from L_C into L_U is defined as follows.
The translation φφ^ from L_U into L_C goes as follows.
For every formula φ of L_C, φ iff φ^+, where the validity statement in each case refers to the semantics of the language in question. Moreover, the translation ()⁺ preserves, both ways, truth in states and therefore validity in models.
The proof of the lemma is straightforward.
The composition of the two translations, first ()⁺ and then ()^, defines the following translation φφ^ from L_C into L_C:
The following lemma shows that we can derive equivalence of φ and its translation φ∗ in AX( L _ C ).
We have _ C φφ^ for every formula φ∈L_C.
The proof proceeds by induction on the structure of φ. The case for atoms is trivial and the cases for the Boolean connectives follow easily from the induction hypothesis using the fact that AX( L _ C ) is complete with respect to PL. We thus discuss the case involving Cφ.
By the induction hypothesis, we have _ C φφ^. By the inference rule EQC, we obtain
On the other hand, by PL, we have
Then, again using PL together with the induction hypothesis and the equivalences above, we derive
Finally, using the axiom C θ C θ with θ:=φ∗ and PL, we get
This concludes the proof. ∎
Next we will show that every derivation in L_U can be simulated by a derivation in AX( L _ C ).
For every formula φ∈L_U, if _ S5 φ then _ C φ^.
The proof proceeds by induction on derivations in L_U. We will first prove that _ C φ^ for each axiom φ for L_U. For propositional tautologies this is trivial.
To deal with Ax1(U), we must show that
for arbitrary θ and ψ. The following derivation does exactly this. (The steps after the first one use PL and the preceding steps.)
To cover axiom Ax2(U), we must show that _ C (θ C θ)→θ, which is a propositional tautology.
To deal with axiom Ax3(U), we must show that
Here is the derivation.
Now it remains to establish that NECU preserves the claim, that is, we will show that if _ S5 φ and thus _ C φ^ by the induction hypothesis, then we also have _ C ([ U ]φ)^. Thus we assume that _ C φ^. Using NEC_C (see Proposition 7.1), we infer that _ C C φ^, and using PL, we get _ C φ^ C φ^. As ([ U ]φ)^=φ^ C φ^, we are done. ∎
We are now ready to prove the soundness and completeness of AX( L _ C ).
The axiomatic system AX( L _ C ) is sound and complete for the validities of L_C.
The soundness follows by an easy verification of the validity of all the axioms and the fact that EQC preserves validity.
To prove completeness, assume that φ for some formula φ of L_C. Then φ^+ by Lemma 7.2. By completeness of L_U, we have _S5φ^+. By Lemma 7.4, we thus have _ C (φ^+)^, i.e., _ C φ^. Therefore _ C φ by Lemma 7.3. ∎
We now define sound and complete axiomatic systems AX( L _ D ) and AX( L _ I ) for L_D and L_ I by introducing new axiom schemata.
The axiomatic system AX( L _ D ) for L_D is obtained by extending AX( L _ C ). The idea is simply to define D in terms of C. A suitable definition is obtained from the equivalence established in Proposition 3.3.
Recall that [u]φ is an abbreviation of φ∧Cφ. We define, for each positive integer k, the following axiom schema:
The system AX( L _ D ) consists of the axiom schemata and rules of L_C together with the above axiom schemata for each k∈ℤ₊.
We obtain an axiomatic system AX( L _ I ) for L_ I similarly by essentially extending AX( L _ C ) by schemata that define by Proposition 4.4 the operator I in terms of C. The language L_ I does not contain C as a primitive, but the translation t given before Proposition 4.3 shows that the operator C can be expressed as φ I φ. Thus we first define AX_0( L _ I ) to be the following system¹⁴ obtained from AX( L _ C ) by the substitution C θθ I θ.
Provided here for readers’ convenience.
Axiom schemes:
Inference rules:
Recalling the abbreviation ⟨u′⟩ from Section 4, we define AX( L _ I ) to be the extension of AX_0( L _ I ) by the following axiom schemata for all m∈ℕ and k,n∈ℤ₊:
where B is as in Proposition 4.4.
We denote derivability in AX( L _ D ) by _ D and derivability in AX( L _ I ) by _ I.
The proofs of the two claims are very similar, so we will first present the argument for AX( L _ D ) and then briefly comment the claim for AX( L _ I ).
Soundness follows from the soundness of AX( L _ C ) and Proposition 3.3. To prove completeness, we will use a similar argument as the one applied in the proof of Proposition 7.5. We will reduce the completeness of AX( L _ D ) to the already proved completeness of AX( L _ C ).
We first define the obvious translation tr of L_D into L_C which leaves all atoms and Boolean connectives intact and likewise translates Cφ to C tr(φ), but treats formulae D(φ₁,…,φₖ;ψ) with k=0 as follows. Using the equivalence established by Proposition 3.3, we put
We then prove by induction on the structure of formulae θ of L_D that
The cases for proposition symbols and Boolean connectives are trivial. To cover the case for C, assume we have shown that _ D φ tr(φ). We then conclude that _ D C φ C tr(φ) directly by the rule EQ_C.
To deal with the case for D, let θ=D(φ₁,…,φₖ;ψ), and let the induction hypothesis be that _ D φ_i tr(φ_i) for each i≤k and _ D tr(). From here it is easy to conclude, using completeness with respect to propositional logic, that we also have _ D χ tr(χ) for each χ∈DNF(φ_1,...,φ_k). Therefore, using PL, we have
whence we infer by the rule EQ_C that we have
Using this equivalence and the already established fact that _ D χ^′ tr(χ^′) for all χ^′∈ ∪DNF(φ_1,...,φ_k), we then infer by PL that
From here we conclude, using propositional logic and Ax(Dₖ), that
In other words, we have _ D D (φ_1,…,φ_k,) tr( D (φ_1,…,φ_k,)), whence we have now established that _ D θ tr(θ) for all θ of L_D.
To conclude the proof, assume that θ for some θ of L_D. Then tr(θ) by soundness of the translation tr. Hence, recalling that tr(θ) is a formula of L_C, we have _ C tr(θ) by completeness of AX( L _ C ). Using the fact that _ D θ tr(θ), we extend the derivation of tr(θ) in AX( L _ C ) to a derivation of θ in AX( L _ D ). Therefore _ D θ.
The completeness proof of AX( L _ I ) is similar. We first prove that AX_0( L _ I ) is complete for the notational variant of L_C that replaces Cφ with f(φ) I f(φ), where f is a translation that keeps proposition variables and Boolean connectives intact but treats C as given here. This proof of completeness is virtually identical to the corresponding argument for AX( L _ C ) given above. Then the completeness of AX( L _ I ) is proved similarly to the way AX( L _ D ) was treated above, the only significant (but uncomplicated) difference being that the axioms Ax( I _k,m,n) instead of axioms Ax( D _k) are used. ∎
Our axiomatizations for L_D and L_ I are not finite because we have the schemata Ax(Dₖ) and Ax(Iₖ,ₘ,ₙ) for infinitely many values of k,m,n.¹⁵ We will next show that, in fact, neither L_D nor L_ I has a finite axiomatization. To this end, we will first define formally what we mean by a finite axiomatization.
Indeed, bounding these values by some small constant would result in more elegant axiomatizations that then would, however, only work for bounded versions of D and I with bounded arities.
An axiom schema for L_D (respectively, L_ I) is an object obtained from a formula χ of L_D (L_ I) by substituting schema letters φ₁,…,φₙ for all proposition symbols in χ. A proof rule for L_D (L_ I) is an implication of the form 1, … , k ⇒ χ, where ψ₁,…,ψₖ,χ are axiom schemata for L_D (L I) and k a positive integer. A finite axiomatization for L_D (L I) is a pair (Φ,Ψ), where Φ is a finite set of axiom schemata and Ψ a finite set of proof rules for L_D (L_ I).
Neither L_D nor L_ I has a sound and complete finite axiomatization.
We discuss L_D only. The argument for L_ I is similar.
Assume (Φ,Ψ) is a sound and complete finite axiomatization for L_D. Let k be the maximum number such that some schema in Φ∪Ψ contains a subschema of the type D(ψ₁,…,ψₖ ; φ). For each formula χ of L_D, let χ() denote the formula obtained from χ by replacing (in any order) each subformula of the type D(α₁,…,αₖ₊₁;β) by . We will show by induction on deductions that for all formulae χ of L_D, if χ is a theorem of (Φ,Ψ), then also χ() is a theorem of (Φ,Ψ). This will conclude the proof for the following reason. Consider the formula D(p,…,p ;p), where p is simply repeated k+2 times. This formula is a theorem of L_D, while is not.
The inductive argument is based on the following observation: if α is a formula obtained from a schema φ by substitution, then also the formula α() can be obtained from φ by substitution, because the schema φ does not involve any subschemata of the type D(χ₁,…,χₖ₊₁;χ′). Therefore the basis of the induction, which deals with the direct use of axiom schemata as a first step of a deduction, is clear. The induction step is based on similar reasoning. For consider a proof rule φ_1,…,φ_m⇒ and assume that we have deduced some formula β by applying an instance α_1,…,α_m⇒ β of this rule to some formulae α₁,…,αₘ such that . Since the schemata φ₁,…,φₘ,ψ do not contain subschemata of the type D(χ₁,…,χₖ₊₁,χ′), we observe that the implication is also an instance of the rule . Since , we have by the induction hypothesis. Thus , as required. ∎
In this paper we have defined the logics L_D and L_ I as alternatives for D and I. We have comprehensively studied the expressive powers of these four logics and argued for the naturalness of L_D and L_ I in relation to D and I. We have also provided sound and complete axiomatizations for L_D and L_ I. Here we discuss briefly a range of natural future developments of the present work.
The determinacy of a formula by a set of formulae can be relativised to a set of possible worlds. Let [θ]_W denote the set and define the relativised determinacy operator Dᶿ(φ₁,…,φₖ;ψ) such that iff for all u,v∈[θ]_W, if the equivalence
holds for each i≤k, then we have
In particular, we define Cᶿ φ=Dᶿ(∅,φ). Using [u], we notice that
We also notice that D(θ,φ) is definable in terms of Cᶿ as follows.
Furthermore, Dᶿ is inductively definable in terms of Cᶿ as follows.
We provide a simple example illustrating the use of relativised determinacy in natural language. Consider a scenario with the following propositions.
Assume the set of possible worlds in the scenario is W={w₁,w₂,w₃,w₄,w₅}, where
Consider the following claim.
If there are road blocks, then, whether it is rush hour determines whether John will be on time.
Perhaps the most natural interpretation for this sentence is given by Dᵖ(q,r), which is true in each world of the model W={w₁,…,w₅}, and thus we have . Interestingly, however, there is at least one sensible alternative interpretation, p→D(q,r), which is true in the worlds w₁,w₂,w₃, and false in w₄,w₅, whence we have .
As already mentioned in the introduction section, the determinacy operator D can be naturally generalised to the general modal setting. Given a Kripke model M=(W,R,V) and a possible world w∈ W, we define the semantics of D as follows: iff for all u,v∈ W such that wRu and wRv, if the equivalence holds for each i≤k, then .
It is easy to see that in a propositional language extended with both D and the standard box modality , we have the equivalence
i.e., for all Kripke models M and points w in the domain of M, the pointed model M,w satisfies either both or neither of the above formulae. On the other hand, on all models with a reflexive accessibility relation (but not in general), the box modality is definable in terms of D by , where Cφ of course denotes D(∅;φ).
Studying D over different classes of Kripke models provides an interesting research direction. In fact, the recent study [Fan16] has already taken up that direction.
It is possible to extend the scope of D to cover arbitrary sets of formulae as follows. Let Γ denote a possibly infinite set of formulae of L_D. Define if for all assignments u,v∈ W it holds that if the equivalence holds for all φ∈Γ, then .
The determinacy operator D now parallels in a natural way Tarski’s notion of a logical consequence operator C defined so that C(Γ,ψ) holds if and only if for every state description model W and assignment w such that for all φ∈Γ. The parallel is in the sense that D satisfies the same defining properties (Reflexivity, Monotonicity and Cut) which Tarski postulated for C (while D has some interesting extra properties that C lacks). Indeed, this is not accidental, because D and C bear technically similar ideas: C preserves truth, whereas D preserves invariance of truth values. For a further discussion of this and related issues, see [Hum92, Hum93, Hum98], as well as [Cia16a, Cia16b] for an argument presenting dependence as a case of logical consequence applied to questions instead of propositions. Thus, an interesting research direction extending the present work involves relating determinacy and logical consequence in the more general modal setting outlined here.
The determinacy operator D has a natural epistemic reading: the determinacy formula D(φ₁,…,φₖ,ψ) can be interpreted to mean that an agent knows the truth value of ψ relative to the truth values of the formulae φ₁,…,φₖ in the sense that the agent can always deduce the truth value of ψ if she learns the truth values of φ₁,…,φₖ. This interpretation of D leads to yet another open research direction. It is worth noting that a uniform analysis of various kinds of knowledge, including knowledge of questions and knowledge of dependencies of this kind has already been given in the work [CR15] on inquisitive epistemic logic (IEL). Indeed, conditional knowledge can be regarded as knowledge obtained by answering questions: the formula D(φ;ψ) with the meaning “agent a knows whether ψ holds conditionally on the knowledge whether φ holds” can be expressed in IEL as Kₐ(?φ→?ψ).
Acknowledgements. Valentin Goranko was partly supported by a research grant 2015-04388 of the Swedish Research Council. Antti Kuusisto was supported by Jenny and Antti Wihuri Foundation and the ERC grant 647289 (CODA). The results of this paper were presented at the Dagstuhl seminar Logics for Dependence and Independence in June 2015, where an earlier manuscript of the present paper was circulated; we thank the participants for their interest. After submitting the arXiv preprint [GK16], we have also been in correspondence with Jie Fan and Lloyd Humberstone. We thank them for their comments and discussion. In particular, Humberstone subsequently commented in depth some aspects of our work in [Hum17] and Jie Fan produced the manuscript [Fan16].
[Alo16]
Maria Aloni. Disjunction. In Edvard N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Stanford University, Stanford, 2016.
[Arm74]
William Armstrong. Dependency structures of database relationships. In IFIP’74, pages 580–583, 1974.
[Cia09]
Ivano Ciardelli. Inquisitive semantics and intermediate logics. Master’s thesis, Institute of Logic, Language and Computation, University of Amsterdam, 2009.
[Cia16a]
Ivano Ciardelli. Dependency as question entailment. In Jouko Väänänen Samson Abramsky, Juha Kontinen and Heribert Vollmer, editors, Dependence Logic: theory and applications, pages 129–181. Springer International Publishing, Switzerland, 2016.
[Cia16b]
Ivano Ciardelli. Questions in Logic. PhD thesis, Institute of Logic, Language and Computation, University of Amsterdam, 2016.
[CR11]
Ivano Ciardelli and Floris Roelofsen. Inquisitive logic. Journal of Philosophical Logic, 40(1):55–94, 2011.
[CR15]
Ivano Ciardelli and Floris Roelofsen. Inquisitive dynamic epistemic logic. Synthese, 192(6):1643–1687, 2015.
[Dem97]
Stéphane Demri. A completeness proof for a logic with an alternative necessity operator. Studia Logica, 58(1):99–112, 1997.
[Fan16]
Jie Fan. A modal logic of supervenience. Manuscript, arXiv:1611.04740v1, 2016.
[FWvD15]
Jie Fan, Yanjing Wang, and Hans van Ditmarsch. Contingency and knowing whether. Review of Symbolic Logic, 8(1):75 –107, 2015.
[Gal12]
Pietro Galliani. Inclusion and exclusion dependencies in team semantics - on some logics of imperfect information. Annals of Pure and Applied Logic, 163(1):68–84, 2012.
[Gal13]
Pietro Galliani. Epistemic operators in dependence logic. Studia Logica, 101(2):367–397, 2013.
[GK16]
Valentin Goranko and Antti Kuusisto. Logics for propositional determinacy and independence. Manuscript, arXiv:1609.07398, 2016.
[GP92]
Valentin Goranko and Solomon Passy. Using the universal modality: Gains and questions. Journal of Logic and Computation, 2(1):5–30, 1992.
[Gre39]
Kurt Grelling. A logical theory of dependence. In Proceedings of the 5th International Congress for the Unity of Science, 1939.
[GV13]
Erich Grädel and Jouko Väänänen. Dependence and independence. Studia Logica, 101(2):399–410, 2013.
[GV14]
Pietro Galliani and Jouko Väänänen. On dependence logic. In A. Baltag and S. Smets, editors, Johan F. A. K. van Benthem on Logical and Informational Dynamics, pages 101–119. Springer, 2014.
[Hin96]
Jaakko Hintikka. The Principles of Mathematics Revisited. Cambridge UP, 1996.
[HKMV15]
Lauri Hella, Antti Kuusisto, Arne Meier, and Heribert Vollmer. Modal inclusion logic: Being lax is simpler than being strict. In MFCS 2015, Proceedings, Part I, pages 281–292, 2015.
[HKVV15]
Miika Hannula, Juha Kontinen, Jonni Virtema, and Heribert Vollmer. Complexity of propositional independence and inclusion logic. In MFCS 2015, Proceedings, Part I, pages 269–280, 2015.
[HLSV14]
Lauri Hella, Kerkko Luosto, Katsuhiko Sano, and Jonni Virtema. The expressive power of modal dependence logic. In R. Goré, B. Kooi, and A. Kurucz, editors, Advances in Modal Logic 10, pages 294–312. College Publications, 2014.
[Hod97]
Wilfrid Hodges. Compositional semantics for a language of imperfect information. Logic Journal of the IGPL, 5(4):539–563, 1997.
[HS89]
Jaakko Hintikka and Gabriel Sandu. Informational independence as a semantical phenomenon. In J. E. Fenstad, I. T. Frolov, and R. Hilpinen, editors, Logic, Methodology and Philosophy of Science, volume 8, pages 571–589. Elsevier, Amsterdam, 1989.
[Hum92]
Lloyd Humberstone. Some structural and logical aspects of the notion of supervenience. Logique et Analyse, 35:101–137, 1992.
[Hum93]
Lloyd Humberstone. Functional dependencies, supervenience, and consequence relations. Journal of Logic, Language and Information, 2(4):309–336, 1993.
[Hum95]
Lloyd Humberstone. The logic of non-contingency. Notre Dame Journal of Formal Logic, 36(2):214–229, 1995.
[Hum98]
Lloyd Humberstone. Note on supervenience and definability. Notre Dame Journal of Formal Logic, 39(2):243–252, 1998.
[Hum02]
Lloyd Humberstone. The modal logic of agreement and noncontingency. Notre Dame Journal of Formal Logic, 43(2):95–127, 2002.
[Hum17]
Lloyd Humberstone. Supervenience, dependence, disjunction. Manuscript, June 2017.
[Jan97]
Theo Janssen. An overview of compositional translations. In Compositionality: The Significant Difference, International Symposium, COMPOS’97, Bad Malente, Germany, September 8-12, 1997. Revised Lectures, pages 327–349, 1997.
[KMSV14]
Juha Kontinen, Julian-Steffen Müller, Henning Schnoor, and Heribert Vollmer. Modal independence logic. In Advances in Modal Logic 10, pages 353–372, 2014.
[KMSV15]
Juha Kontinen, Julian-Steffen Müller, Henning Schnoor, and Heribert Vollmer. A van benthem theorem for modal team semantics. In CSL 2015, Proceedings, pages 277–291, 2015.
[Kon13]
Juha Kontinen. Dependence logic: A survey of some recent work. Philosophy Compass, 8(10):950–963, 2013.
[Kuu14]
Antti Kuusisto. A double team semantics for generalized quantifiers. CoRR, abs/1310.3032v5, 2014.
[Kuu15]
Antti Kuusisto. A double team semantics for generalized quantifiers. CoRR, abs/1310.3032v8, 2015.
[LV13]
Peter Lohmann and Heribert Vollmer. Complexity results for modal dependence logic. Studia Logica, 101(2):343–366, 2013.
[MB14]
Brian McLaughlin and Karen Bennett. Supervenience. In Edward N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Stanford, 2014.
[MR66]
Hugh Montgomery and Richard Routley. Contingency and non-contingency bases for normal modal logics. Logique et Analyse, 9(35):318–328, 1966.
[Piz07]
Claudio Pizzi. Necessity and relative contingency. Studia Logica, 85(3):395–410, 2007.
[Piz13]
Claudio Pizzi. Relative contingency and bimodality. Logica Universalis, 7(1):113–123, 2013.
[Roe13]
Floris Roelofsen. Algebraic foundations for the semantic treatment of inquisitive content. Synthese, 190(1):79–102, 2013.
[SvE88]
Barry Smith and Christina von Ehrenfels. Foundations of Gestalt Theory. Philosophia resources library. Philosophia Verlag, 1988.
[Vää07]
Jouko Väänänen. Dependence Logic - A New Approach to Independence Friendly Logic, volume 70 of London Mathematical Society student texts. Cambridge University Press, 2007.
[Vää08]
Jouko Väänänen. Modal dependence logic. In K. R. Apt and R. van Rooij, editors, New Perspectives on Games and Interaction, pages 237–254. Amsterdam University Press, 2008.
[Yan14]
Fan Yang. Extensions and Variants of Dependence Logic. PhD thesis, University of Helsinki, 2014.
[Yan16]
Fan Yang. Uniform definability in propositional dependence logic. arXiv:1501.00155, 2016.
[YV16]
Fan Yang and Jouko Väänänen. Propositional logics of dependence. Annals of Pure and Applied Logic, 167(7):557–589, 2016.