This paper considers KLM-style preferential non-monotonic reasoning in the setting of propositional team semantics. We show that team-based propositional logics naturally give rise to cumulative non-monotonic entailment relations. Motivated by the non-classical interpretation of disjunction in team semantics, we give a precise characterization for preferential models for propositional dependence logic satisfying all of System P postulates. Furthermore, we show how classical entailment and dependence logic entailment can be expressed in terms of non-trivial preferential models.
We define non-monotonic versions of team-based logics and
study their axiomatics regarding System P. The logics are
defined with the aid of preferential models in the style of
Kraus, Lehmann and Magidor [
Team semantics is a logical framework for studying
concepts and phenomena that arise in the presence of plurality
of data. Prime examples of such concepts are, e.g., functional
dependence ubiquitous in database theory and conditional
independence of random variables in statistics. The
beginning of the field of team semantics can be traced back to
the introduction of (first-order) dependence logic in [
Non-monotonicity is one of the core phenomenons of
reasoning that are deeply studied in knowledge
representation and reasoning; see Gabbay et al. (1993) and Brewka
et al. (1997) for an overview, with, e.g., connections to
belief change [
Alternatively to the interpretation above, one can understand non-monotonic inferences from a team perspective. For example, =(, ) |∼¬ reads then as “a team that usually satisfies =(, ) also satisfies ¬”. For the latter kind of expression, there is no obvious way to formulate it in existing team-based logic, so injecting non-monotonicity is a valuable extension of team logics. Note that “=(, ) |∼¬ ” does not imply that = (, ) ∧ is inconsistent. The semantics of team logic is developed with emphasis on teams. Depended on the application context, one reads =(, ) |∼¬ , e.g., as follows: Database Interpretation: “When the value of determines the value of in a database, then usually the value of is 0.” Possible World Interpretation. “When the agent is convinced that whether holds in a world always depends on , then usually the agent believes that does not hold.”
There are several approaches to non-monotonic
reasoning, e.g., circumscription, autoepistemic logic, Reiters
default logic, see Gabbay (1993) for an overview. For a start,
one can rely on the basic systems of non-monotonic
reasoning. The very most basic denominator of non-monotonic
reasoning is often denoted cumulative reasoning, which is
given axiomatically by System C [
Because of (KLM.1), KLM-style reasoning is also denoted preferential reasoning. Common for both representations of KLM-style reasoning is, that they are parametric in the sense that they make use of some underlying classical logic L , e.g., propositional logic or first-order logic.
In this paper, we define preferential team logics via
preferential models (as in KLM.1). The rationale is that we think
that preferential models capture the original intention of
preferential logic best, and, as we demonstrate, it shows
standard non-monotonic behaviour. Furthermore, we study
the relationship of preferential teams logic to System P (as
in KLM.2). Our axiomatic studies show that for general
team-based logics, (KLM.1) and (KLM.2) do not induce the
same non-monotonic inference relations. This is of interest,
e.g., because it gives a negative answer to the question of
whether the relationship between (KLM.1) and (KLM.2) by
KLM (1990) generalize beyond the assumptions by KLM1.
We give a condition for preferential models that is suficient
to reestablish satisfaction of System P in all preferential team
logics. Specifically for preferential dependence logic, we also
show that this condition exactly characterizes those
preferential models such that System P is satisfied. Moreover,
when using specific (non-trivial) preferences, preferential
dependence logic becomes dependence logic, respectively,
it is equivalent to classical propositional entailment.
2. Background: Team-Based Logics
In this section we present the background on propositional
logics with team semantics, propositional dependence logic
and propositional inclusion logic (see [
Semantics We denote by Prop = { : ∈ N} the set of propositional variables. We will use letters , , , . . . (with or without subscripts) to stand for elements of Prop. In this article, we consider only formulas in negation normal form. Definition 1 (Classical propositional logic (PL)). Well formed PL-formulas are formed by the grammar: ::= | ¬ | ⊥ | ⊤ | ∧ | ∨
In team semantics, one usually considers a non-empty finite subset ⊆ Prop of propositional variables and defined for valuations : → {0, 1} over and PL-formulas :
J K := { : → {0, 1} | |= }.
We write |= in case () = 1, and ̸|= otherwise. The valuation function is extended to the set of all PL-formulas in the usual way.
Definition 2. For any set ∆ ∪ { } of PL-formulas, we write ∆ |= if for any valuation , |= for all ∈ ∆ implies |= . We write simply |= for { } |= and ≡ if both |= and |= .
Next we define team semantics for PL-formulas (cf. [
= ∪ , |= and |= .
The set of all teams with |= is written as J K. Logical entailment and equivalence are defined as usual. For any set ∆ ∪ of classical formulas, we write ∆ |= if for any team , |= for all ∈ ∆ implies |= . We write simply |= for { } |= . Write ≡ if both |= and |= .
Proposition 4. Let be a PL-formula. Then the following properties hold: Flatness: |=
⇐⇒ for all ∈ , {} |= .
Empty team property: ∅ |= .
Downwards closure: If |= and ⊆ , then |= . Union closure: If |= and |= , then ∪ |= .
For any PL-formula , it further holds that {} |=
⇐⇒ |= , and hence for classical formulas, ∆ |= ⇐⇒ ∆ |= . 2.2. Propositional Dependence and
Inclusion Logic A (propositional) dependence atom is a string =(1 . . . , ), and a (propositional) inclusion atom is a string 1 . . . ⊆ 1 . . . , in which 1, . . . , , , 1, . . . , are propositional variables from Prop. The team semantics of these two types of atoms is defined as follows, whereby ⃗ stands for 1, . . . , : • |= =(⃗, ) if for all , ′ ∈ , (⃗) = ′(⃗) implies () = ′(). • |= ⃗ ⊆ ⃗ if for all ∈ , there exists ′ ∈ such that (⃗) = ′(⃗).
We define propositional dependence logic (denoted as PL(=(,))) as the extension of PL-formulas with dependence atoms. Similarly, propositional inclusion logic (denoted as PL(⊆ )) is the extension of PL by inclusion atoms. In this paper, we use propositional team logic to refer to any of the logics PL, PL(=(,)) and PL(⊆ ).
It is straightforward to check that dependence atoms do not have the union closure property and inclusion atoms the downwards closure property. However, the following holds.
Proposition 5. Formulas of PL(=(,)) and PL(⊆ ) have the empty team property. Moreover, PL(=(,))-formulas have the downwards closure property, while PL(⊆ )-formulas have the union closure property.
A dependence atom with the empty sequence in the first component will be abbreviated as =() and called constancy atoms. The team semantics of constancy atoms is reduced to
• |= =() if for all , ′ ∈ , () = ′(). Example 6. Consider the team over {, , } defined by: 1 2 3 We have |= =(, ) and |= =(). Moreover, |= =() ∨ =() but ̸|= =(). It is worth noting that PL(⊆ ) ≡ ∨ because of the union closure property. that |= and that
We can define the flattening
of a PL(=(,))-formula
by replacing all dependence atoms by ⊤. It is easy to check
{} |= ⇔ |=
(1)
for all assignments using the fact that dependence atoms
are always satisfied by singletons.
3. Background: Preferential Logics
In this section, we present background on preferential logics
in style of Kraus, Lehmann and Magidor [
For a strict partial order ≺ ⊆ × on a set and a with respect to ≺
if for each ′ ∈ holds ′ ̸≺ subset ⊆ , an element ∈ is called minimal in . Then, min(, ≺ ) is the set of all ∈ that are minimal in with respect to ≺ .
([
Smoothness guarantees the existence of minimal elements.
Definition 8 ([
if for all ∈ min(( ), ≺ ) holds ℓ() |=
L × L is called preferential if there is a preferential model W for L such that |∼ = |∼ W .
Because there are many preferential models for a logic L , we may have for one logic L with multiple preferential logics that are based on L . More precisely, when one considers a logical language ℒ, an entailment relation |= over ℒ that is based on a model theory with interpretations Ω , then there are (infinitely) many diferent preferential models W1, W2, . . . for this logic. Many of these preferential models yield diferent entailment relations |∼ W1 , |∼ W2 , . . .. 1–7 (RW) (CM) (Or) 3.2. Axiomatic Characterization by System P We make use of the following rules for non-monotonic entailment |∼ :
≡ ∧ |∼
|∼ |∼ |∼ |∼ |∼ (Ref ) (LLE) (Cut) |= |∼ |∼
|∼
∧ |∼
∨ |∼
|∼
|∼
|∼
Note that |= is the entailment relation of the underlying
monotonic logic L . The rules (Ref), (RW), (LLE), (CM) and
(Cut) forming System C. The rule (CM) goes back to the
foundational paper on non-monotonic reasoning system
by Gabbay (1984) and is a basic wakening of monotonicity.
System P consists of all rules of System C and the rule (Or).
The rule of (Or) is motivated by reasoning by case [
Proposition 9 (Kraus et al. 1990). Let L be a compact Tarskian logic with all Boolean connectives. A entailment L ×
L satisfies System P if and only if |∼ is 4. Preferential Team Logics For propositional team-based logics, we restrict ourselves to preferential models that we call standard.
called standard if
A preferential model W = ⟨, ℓ, ≺⟩ is such that ℓ() = (S1) There is no state ∈ such that ℓ() = ∅ (S2) For all non-empty teams there is some state ∈
The rationale for (S1) and (S2) is to make the models concise and meaningful, i.e., containing explicit, yet necessary information for specifying reasoning. By (S1) we are excluding the empty team ∅ from , because team logics considered here have the empty-team property. Hence, ∅ is trivially a model of every formula and including it provides no extra information. Condition (S2) ensures that every "non-trivial" model is included, and thus, its preference status is explicitly given in the preferential model.
We define the family of preferential team logics as those that are induced by some standard preferential model.
sitional team logic is called (standard) preferential, if there is some standard preferential model W such that |∼ = |∼ W
. over some propo
The next example is the bird-penguin example, demonstrating that preferential team logics are indeed nonmonotonic. {, , } ⊆ Example 12. Fix the set of propositional variables =
Prop, with the following intended meanings: stands for “it is a bird”, stands for “it is a penguin”, and stands for “it is able to fly” . We construct a (standard) preferential model, by using the following teams: = 1 1 0 1 = 2 1 1 0 Let Wpeng = ⟨peng, ℓpeng, ≺ peng⟩ be the preferential model such that peng =
{ | is a non-empty team} and ℓpeng( ) = ; for all singleton teams diferent from and we define:
≺ peng ≺ peng for all non-empty teams and non-empty non-singleton teams we define:
≺ peng if ⊊
= |∼ Wpeng
we obtain the following inference: |∼ |∼¬ ∧ |̸∼ This is because we have: (“birds usually fly”) (“penguins usually do not fly”) (“penguin birds usually do not fly”) min(JK, ≺ peng) = { } ⊆ J K min(JK, ≺ peng) = min(J ∧ K, ≺ peng) = { } ⊆ J¬ K
Note that Example 12 is agnostic about the concrete team logic used, i.e., it applies to PL, PL(=(,)), and PL(⊆ ). 5. General Axiomatic Evaluation We will now present general results on whether System P holds for non-preferential and preferential team logics. 5.1. System P and Non-Preferential Team
Logics For the entailment |= of propositional team logics, we obtain that System P is not satisfied by PL(=(,)). For PL and PL(⊆ ), we obtain that they satisfy System P.
Proposition 13. The following statements hold for |=: (a) PL(=(,)) satisfies System C, but violates System P. (b) PL (under team semantics) and PL(⊆ ) satisfy System P. Proof. We show both statements.
(a) Satisfaction of System C is a corollary of Proposition 14 and (b) of Proposition 23. The violation of (Or) is witnessed by choosing , and to be the formula =() in Example 6. (b) We start with satisfaction of System C. Note that one if and only if can reconstruct non-preferential entailment |= of PL by using a preferential model where all teams are incomparable. In such a preferential model W one has min(J K, ≺ ) = J K. Hence, we have |∼ W
if and only if |
= . By J
K ⊆ J
K using this, satisfaction of System C is a corollary of Proposition 14.
It remains to show that (Or) is satisfied. Let , and be PL-formulas such that |= and |= . If 1–7 same. is a model of ∨ , then there are teams , with = ∪ such that | = and |= .
Because , are models of and because PL has the union closure property (see Proposition 5), we obtain that is also a model of . Hence, ∨ |= . The proof of statement (b) for PL(⊆ ) is the Note that Example 6 is a witness for the second part of the statement (a) of Proposition 13, i.e., PL(=(,)) violates (Or). 5.2. System P and Preferential Team Logics Generally, System C is satisfied by preferential team logics. Proposition 14. Let W = ⟨, ℓ, ≺⟩ for a propositional team logic. The preferential entailment
if for all minimal ∈ ( ) holds ℓ() |= . ℓ() |= . Consequently, we have |∼ W .
By the definition of ( ), we have ∈ ( ) if [LLE.] Suppose that ≡ and |∼ W holds. From ≡ , we obtain that ( ) = ( ) holds. By using this last observation and the definition of |∼ W , we obtain |∼ W
from |∼ W . [RW.] Suppose that |= and |∼ by definition of |= we have W J
K ⊆ holds. Clearly,
J K. From ℓ() ∈ J
K the definition of |∼
W
, we obtain that ℓ() |= holds for each minimal ∈ ( ). The condition ℓ() |= in the last statement is equivalent to stating ℓ() ∈ J K. Because of J
K ⊆ J
K, we also have ; and hence, ℓ() |= for each minimal ∈ ( ). This shows that |∼ W holds. [Cut.] Suppose that ∧ |∼
W and |∼ W holds.
By unfolding the definition of
( ) from min(( ogously, |∼ ∧ ), ≺ )
⊆ W unfolds to min(( ), ≺ ) ⊆ ( ).
Moreover, employing basic set theory yields that ( ∧ ) = ( )∩( )
⊆ ) ⊆ ( ) and min(( ), ≺ ) ⊆ ( ) holds. From ( ∧ ( ), we obtain min(( ), ≺ )
( ∧ ). Consequently, we also have that min(( ), ≺ ) = min(( ∧ ), ≺ ) holds. Using the last observation and min(( ∧ ), ≺ ) ( ), we obtain min(( ), ≺ ) ⊆ ( ). Hence also
⊆ |∼ W
, we obtain ∧ |∼ W . Anal |∼ W
holds. [CM.] Suppose that |∼
W
By unfolding the definition of and |∼ W
|∼
W
holds. , we obtain ∧ |∼ W . contradicts the minimality of in ( sequently, we have that ∈ min(( ), ≺ ) holds. Because we have min(( ), ≺ ) ⊆ ( ), we obtain ∧ ). Con
The following Example 15 witnesses that, in general, (Or), and hence, System P, is violated by preferential team logics. Example 15. Assume that = {, } ⊆ following valuations 1, 2, 3 will be important: Prop holds. The 1() = 1() = 2() = 1 2() = 3() = 3() = 0 ential model such that We consider the teams = {1}, = {2}, and ↔ = {1, 3}. Let Wpq = ⟨pq, ℓpq, ≺ pq⟩ be the preferpq = { | is a non-empty team} ℓpq( ) = holds, and such that ≺ pq is the strict partial order given by2 ↔ ≺ pq ↔ ≺ pq ≺ pq ≺ pq where stands for every team diferent from and ↔. We obtain the following preferential entailments: |∼ Wpq ¬ |∼ Wpq ∨ ¬ |̸∼ Wpq Proposition 16. The entailment relation |∼ Wpq for PL, respectively PL(=(,)) and PL(⊆ ), violates (Or).
We can reestablish satisfaction of System P, by demanding the (⋆)-property, which we define below in Proposition 17. In the following we abuse notation and mean by min(JK, ≺ ) the set of ≺ -minimal states in (), as well as the set of al models ℓ() of for which a ≺ minimal states in () exists. More technically correct would be to write min((), ≺ ) for the former, and writing {ℓ() | ∈ min((), ≺ )} for the latter.
Proposition 17. Let W be a preferential model for some preferential team logic. If (⋆) is satisfied for all formulas , , then |∼ W satisfies System P, whereby 3: min(J ∨ K, ≺ ) ⊆
min(JK, ≺ ) ∪ min(JK, ≺ ) (⋆) J K cause (⋆) holds, this also means that min(J ∨ K, ⪯ ) ⊆ 6. Results for Preferential
For preferential dependence logic, we provide additional results to those of Section 5. 6.1. System P and Preferential Dependence
Logic The main contribution is a characterization of exactly those preferential entailment relations that satisfy all rules of System P. Central to this result is the following property for 2For the sake of readability we abuse notation and identify with . 3Abbreviation: min(JK, ≺ ) = {ℓ() | ∈ min((), ≺ )} 1–7 (△) states: a preferential model W = ⟨, ℓ, ≺⟩ , where , ′ ∈ are for all , |ℓ()| > 1, exists ′ with ℓ(′) ⊊ ℓ() and ′ ≺ The (△)-property demands (when understanding states as teams) that for each non-singleton team exists a proper subteam of that is preferred over . For this property, we can show the following theorem.
Theorem 18. Let W = ⟨, ℓ, ≺⟩ PL(=(,)). The following statements are equivalent: be a preferential model for (i) |∼ W satisfies System P. (ii) W satisfies the
△-property. (iii) The (⋆)-property holds for all , ∈ PL(=(,)).
We will obtain the proof of the theorem via the following lemmata. let a team over . We define the following formula: For the first lemma, assume that = {1, . . . , }, and Θ := ⋁︁ (1 ∧ · · · ∧
), ∈ whereby stands for if (1) = 1 holds and for ¬ if () = 0 holds. This formula is of crucial importance for proving Theorem 18. It is straightforward to check the following lemma. we have Lemma 19. Θ defines the family of subteams of , i.e., |= Θ ⇐⇒ ⊆ .
The next lemma guarantees that for a suficient large enough teams exist formulas , such that is a model of the disjunction ∨ , but is not a model of and . We make use of the following notions: define down() = { | ⊆ down({1, . . . , }) = ⋃︀
=1 down() } and down(1, . . . , ) = mulas and such that Lemma 20 (†). For each team with || > 1 exists for |= ∨ , ̸|= , and ̸|= and = Θ . , ⊆ Proof. Since we have || > 1, there exists non-empty teams such that = ∪ and ̸= and ̸= . Moreover, there are formulas and such that JK = down( ) and JK = down(), namely = Θ property describe the same preferential models.
We will now show that the (△)-property and the (⋆)
= ⟨, ℓ, ≺⟩ PL(=(,)) satisfies (△) if and only if (⋆) is satisfied. over PL(=(,)). The preferential entailment relation |∼ W over minimal elements of the order ≺ Proof. Assume (△) holds. Then it is easy to see that the are states that are mapped, via ℓ, to singleton teams. Furthermore, by the downward closure property, for any ∨ the minimal teams satisfying the formula are all singletons. Since for singleton teams the interpretation of ∨ is equivalent with that of the Boolean disjunction the property (⋆) follows.
For the converse, assume that (⋆) holds and let be a team with || > 1. We will show that then there is some team with ⊊ , ̸= ∅ , and ≺ Because contains at least two valuations, there exist , ⊆ such that = ∪ and ̸= and ̸= . By (the proof of) Lemma 20 there are formulas = Θ and = Θ such that |= ∨ , yet ̸|= and ̸|= . Using this and (⋆), we obtain that ∈/ min( ∨ , ≺ ) holds. However, by smoothness of ≺ , the set ( ∨ ) = () contains a team ′ such that ′ ≺ . Now ′ is a witness for the (△)-Property.
Now we are ready to give the proof of Theorem 18. Proof of Theorem 18. By Lemma 21, it sufices to show (⋆) ⇒ (Or) and (Or) ⇒ (△). We show each direction independently: (⋆) ⇒ (Or). This is given by Proposition 17. (Or) ⇒ (△). Assume, for a contradiction, that (△) fails.
Then there exists a team of size ≥ 2 such that for all ⊆ , ̸≺ . Let = + (, ≥ 1 and ≤ ) and define := Θ ∧ ( ∨ · · · ∨ ), where := ⋀︀1≤ ≤ =() and has many copies of . It is easy to check that is satisfied by subteams of of cardinality at most . The formula is defined similarly with copies of in the disjuncts. Now it holds that |= , |= but ̸|= , . Using reflexivity and right weakening, it follows that |∼ W and |∼ W . On the other hand, since is now a minimal model of ∨ that does not satisfy we have shown ∨ |̸∼ W and that (Or) fails for |∼ W. 6.2. Relation to Dependence Logic and
Classical Entailment Theorem 18 and the △-property imply that preferential dependence logics that satisfy System P are quintessentially the same as their flattening 4 counterpart in (preferential) propositional logic with classical (non-team) semantics. Theorem 22. Let W = ⟨, ℓ, ≺⟩ be a preferential model over PL(=(,)) that satisfies System P. Then |∼ W if |∼ W′ , where W′ = ⟨′, ℓ′, ≺ ′⟩ denotes the preferential model for classical propositional logic induced by W, i.e., over |= for PL formulas and valuations induced by the singleton teams in .
Proof. Note first that by the assumption for all valuations , ′ it holds that ≺ ′ ′ if {} ≺ { ′}. By theorem 18, satisfies the (△)-property and hence the minimal elements of ≺ are singleton teams. Hence |∼ , if, for all minimal {} ∈ JK : {} |= , if, for all ≺ ′-minimal ∈ J K : |= . The last equivalence holds due to (1). 4Note that the flatting of a formula is defined at the end of Section 2. 1–7
As a last result, we consider preferential models that characterize the |= entailment relation, as well as the entailment relation for classical formulas |=. Let Wsub = ⟨sub, ℓsub, ≺ sub⟩ and Wsup = ⟨sup, ℓsup, ≺ sup⟩ be the preferential models such that the following holds: sub = sup = { | is a non-empty team} ℓsub( ) = ℓsup( ) = ≺ sub if ⊊ ≺ sup if ⊊ In Wsub and Wsup, for each team there is exactly one state that is labelled by . In ≺ sub, subsets of a team are preferred, whereas in ≺ sup superset teams are preferred.
The preferential model Wsup gives rise to the PL(=(,)) entailment relation |=, and the preferential model Wsup gives rise to classical entailment of the flattening |=. Proposition 23. For all PL(=(,))-formulas , we have: (1) |∼ Wsub if and only if |= (2) |∼ Wsup if and only if |= Proof. We show statements (1) and (2).
. (1) Observe at first that we have |∼ Wsub exactly when we also have min(JK, ≺ sub) ⊆ JK. Because PL(=(,)) has the downwards closure property, we also have that stating min(JK, ≺ sub) ⊆ JK is equivalent to stating that for all singleton teams {} holds that {} |= implies {} |= . The latter statement is equivalent to stating that for the flattening and holds that for all valuations holds that |= implies |= (see also Section 2).
Hence, we have |∼ Wsub if and only if |= (2) We obtain |= ⊆ |∼ Wsup immediately by the definition of |∼ Wsup . We consider the other direction. The statement |= is equivalent to JK ⊆ JK. Because JK is downward-closed, there are (pairwise ⊆ -incomparable) teams 1, . . . , such that JK = down(1, . . . , ). Because of the last property, we have that |= holds exactly when {1, . . . , } ⊆ JK holds. By construction of Wsup we have min(JK, ≺ sup) = {1, . . . , } for . Consequently, we also have that |∼ Wsup holds and consequently, we also have |∼ Wsup ⊆ | =.
Note that, in conformance with Theorem 18 and Proposition 13, Wsup violates the (△)-property and (⋆)-property.
We considered preferential propositional team logics, which are non-monotonic logics in the style of Kraus et al.. Our results are a primer for further investigations on nonmonotonic team logics. We want to highlight that Theorem 22 indicates that (Or) of System P is too restrictive for non-monotonic team logics. In future work, the authors plan to identify further results on preferential models, especially with respect to axiomatic systems diferent from System P. Connected with that is to study the meaning of conditionals and related complexity issues in the setting of team logics.