Dependency atoms

The atoms of team semantics are team properties, alongside the connectives of Team/Operations.lean. Each atom compares values read off the points of a team through two maps f and g. Väänänen's dependence atom Team.dep f g says that on the team g is a function of f; the inclusion atom Team.incl f g, which Anttila, Häggblom and Yang study in modal team logic, says that every value of f on the team is a value of g there.

A team of assignments reads a tuple of variables through f, and a team of Kripke worlds reads a tuple of propositional atoms through the valuation. Väänänen's first-order atom =(Z, u), here Team.Dep, and the modal atoms of Team/ModalDependence.lean and Team/ModalInclusion.lean are therefore instances of the same properties, and their closure behaviour is proved once. Widening the parameters of Team.Dep weakens dependence and strengthens variation, which is how Degano and Aloni compose the atoms into constancy and variation conditions.

Main definitions

• Team.dep, Team.incl: the atoms as team properties.
• Team.Dep, Team.Var: the first-order dependence atom over a team of assignments, and the variation atom, its failure witnessed by two assignments.

Main results

• Team.isLowerSet_dep, Team.supClosed_incl, Team.isUpperSet_var: closure of the atoms.
• Team.not_supClosed_dep, Team.not_isLowerSet_incl: the closure properties they break.
• Team.dep_iff_exists: the dependent variable is a function of the parameters on the team.
• Team.Dep.trans: dependence composes.

References

• [Hod97] Hodges, Compositional semantics for a language of imperfect information
• [Vaa07] Väänänen, Dependence Logic: A New Approach to Independence Friendly Logic
• [AHY25] Anttila, Häggblom and Yang, Axiomatizing modal inclusion logic and its variants
• [DA25] Degano and Aloni, How to be (non-)specific

The atoms as team properties

def Team.dep {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : α → γ) : TeamProperty α

The dependence atom holds of a team on which g is a function of f.

Equations

• Team.dep f g = {T : Finset α | Function.FactorsThrough ((↑T).domRestrict g) ((↑T).domRestrict f)}

def Team.incl {α : Type u_1} {β : Type u_2} (f g : α → β) : TeamProperty α

The inclusion atom holds of a team on which every value of f is a value of g.

Equations

• Team.incl f g = {T : Finset α | ∀ a ∈ T, ∃ b ∈ T, f a = g b}

theorem Team.mem_dep {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : α → γ} {T : Finset α} : T ∈ dep f g ↔ ∀ a ∈ T, ∀ b ∈ T, f a = f b → g a = g b

@[simp]

theorem Team.mem_incl {α : Type u_1} {β : Type u_2} {T : Finset α} {f g : α → β} : T ∈ incl f g ↔ ∀ a ∈ T, ∃ b ∈ T, f a = g b

@[instance_reducible]

instance Team.instDecidableMemFinsetTeamPropertyDepOfDecidableEq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : α → γ} [DecidableEq β] [DecidableEq γ] (T : Finset α) : Decidable (T ∈ dep f g)

Equations

• Team.instDecidableMemFinsetTeamPropertyDepOfDecidableEq T = decidable_of_iff (∀ a ∈ T, ∀ b ∈ T, f a = f b → g a = g b) ⋯

@[instance_reducible]

instance Team.instDecidableMemFinsetTeamPropertyInclOfDecidableEq {α : Type u_1} {β : Type u_2} [DecidableEq β] (f g : α → β) (T : Finset α) : Decidable (T ∈ incl f g)

Equations

• Team.instDecidableMemFinsetTeamPropertyInclOfDecidableEq f g T = { decide := decide (∀ a ∈ T.val.attach, (fun (a : α) (a_2 : a ∈ T) => ∃ b ∈ T, f a = g b) ↑a ⋯), reflects_decide := ⋯ }

theorem Team.isLowerSet_dep {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : α → γ) : IsLowerSet (dep f g)

theorem Team.singleton_mem_dep {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : α → γ} (a : α) : {a} ∈ dep f g

theorem Team.empty_mem_dep {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : α → γ} : ∅ ∈ dep f g

theorem Team.empty_mem_incl {α : Type u_1} {β : Type u_2} (f g : α → β) : ∅ ∈ incl f g

theorem Team.supClosed_incl {α : Type u_1} {β : Type u_2} [DecidableEq α] (f g : α → β) : SupClosed (incl f g)

theorem Team.not_supClosed_dep {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : α → γ} [DecidableEq α] {a b : α} (hf : f a = f b) (hg : g a ≠ g b) : ¬SupClosed (dep f g)

Dependence is not union-closed. Two points agreeing on f and differing on g each form a team satisfying the atom, but their union does not.

theorem Team.not_isLowerSet_incl {α : Type u_1} {β : Type u_2} [DecidableEq α] {f g : α → β} {a b : α} (hab : f a = g b) (hb : f b = g b) (ha : f a ≠ g a) : ¬IsLowerSet (incl f g)

Inclusion is not downward-closed. If b supplies the g-value both of its own f-value and of a's, but a does not supply its own, then {a, b} satisfies the atom and {a} does not.

The first-order atoms

def Team.Dep {V : Type u_4} {E : Type u_5} (T : Finset (V → E)) (Z : Finset V) (u : V) : Prop

The first-order dependence atom =(Z, u) holds of a team of assignments on which the value of u is a function of the values of the variables of Z. With Z empty, u is constant across the team.

Equations

• Team.Dep T Z u = (T ∈ Team.dep (↑Z).domRestrict fun (x : V → E) => x u)

def Team.Var {V : Type u_4} {E : Type u_5} (T : Finset (V → E)) (Z : Finset V) (u : V) : Prop

The variation atom var(Z, u) of [DA25] holds of a team in which two assignments agree on Z and differ on u. It is the failure of =(Z, u) (Team.not_dep), stated by its witnesses.

Equations

• Team.Var T Z u = ∃ i ∈ T, ∃ j ∈ T, (∀ z ∈ Z, i z = j z) ∧ i u ≠ j u

theorem Team.dep_iff {V : Type u_4} {E : Type u_5} {T : Finset (V → E)} {Z : Finset V} {u : V} : Dep T Z u ↔ ∀ i ∈ T, ∀ j ∈ T, (∀ z ∈ Z, i z = j z) → i u = j u

Assignments of the team agreeing on every variable of Z agree on u.

theorem Team.var_iff {V : Type u_4} {E : Type u_5} {T : Finset (V → E)} {Z : Finset V} {u : V} : Var T Z u ↔ ∃ i ∈ T, ∃ j ∈ T, (∀ z ∈ Z, i z = j z) ∧ i u ≠ j u

@[instance_reducible]

instance Team.instDecidableDepOfDecidableEq {V : Type u_4} {E : Type u_5} [DecidableEq E] (T : Finset (V → E)) (Z : Finset V) (u : V) : Decidable (Dep T Z u)

Equations

• Team.instDecidableDepOfDecidableEq T Z u = decidable_of_iff (∀ i ∈ T, ∀ j ∈ T, (∀ z ∈ Z, i z = j z) → i u = j u) ⋯

@[instance_reducible]

instance Team.instDecidableVarOfDecidableEq {V : Type u_4} {E : Type u_5} [DecidableEq E] (T : Finset (V → E)) (Z : Finset V) (u : V) : Decidable (Var T Z u)

Equations

• Team.instDecidableVarOfDecidableEq T Z u = { decide := decide (∃ (a : V → E) (_ : a ∈ T), (fun (i : V → E) => ∃ j ∈ T, (∀ z ∈ Z, i z = j z) ∧ i u ≠ j u) a), reflects_decide := ⋯ }

theorem Team.dep_iff_exists {V : Type u_4} {E : Type u_5} {T : Finset (V → E)} {Z : Finset V} {u : V} [Nonempty E] : Dep T Z u ↔ ∃ (h : (↥Z → E) → E), ∀ i ∈ T, i u = h ((↑Z).domRestrict i)

Dependence holds exactly when, on the team, some function takes the values of the variables of Z to the value of u.

@[simp]

theorem Team.not_dep {V : Type u_4} {E : Type u_5} {T : Finset (V → E)} {Z : Finset V} {u : V} : ¬Dep T Z u ↔ Var T Z u

Variation is the failure of dependence.

@[simp]

theorem Team.not_var {V : Type u_4} {E : Type u_5} {T : Finset (V → E)} {Z : Finset V} {u : V} : ¬Var T Z u ↔ Dep T Z u

theorem Team.Dep.not_var {V : Type u_4} {E : Type u_5} {T : Finset (V → E)} {Z : Finset V} {u : V} (h : Dep T Z u) : ¬Var T Z u

Dependence excludes variation on the same parameters.

theorem Team.dep_of_mem {V : Type u_4} {E : Type u_5} {T : Finset (V → E)} {Z : Finset V} {u : V} (h : u ∈ Z) : Dep T Z u

A parameter depends on the parameters.

theorem Team.dep_singleton {V : Type u_4} {E : Type u_5} {Z : Finset V} {u : V} (i : V → E) : Dep {i} Z u

Every dependence holds on a team of one assignment.

theorem Team.Dep.mono {V : Type u_4} {E : Type u_5} {T : Finset (V → E)} {Z Z' : Finset V} {u : V} (hZ : Z ⊆ Z') (h : Dep T Z u) : Dep T Z' u

Dependence on fewer parameters is dependence on more.

theorem Team.Var.anti {V : Type u_4} {E : Type u_5} {T : Finset (V → E)} {Z Z' : Finset V} {u : V} (hZ : Z ⊆ Z') (h : Var T Z' u) : Var T Z u

Variation on more parameters is variation on fewer.

theorem Team.Dep.trans {V : Type u_4} {E : Type u_5} {T : Finset (V → E)} {Z Z' : Finset V} {u : V} (hZ : ∀ z ∈ Z', Dep T Z z) (h : Dep T Z' u) : Dep T Z u

Dependence composes, so a variable depending on variables that all depend on Z depends on Z.

theorem Team.Dep.subset {V : Type u_4} {E : Type u_5} {T T' : Finset (V → E)} {Z : Finset V} {u : V} (hT : T' ⊆ T) (h : Dep T Z u) : Dep T' Z u

Dependence is inherited by subteams.

theorem Team.Var.superset {V : Type u_4} {E : Type u_5} {T T' : Finset (V → E)} {Z : Finset V} {u : V} (hT : T ⊆ T') (h : Var T Z u) : Var T' Z u

Variation is inherited by superteams.

theorem Team.isUpperSet_var {V : Type u_4} {E : Type u_5} (Z : Finset V) (u : V) : IsUpperSet {T : Finset (V → E) | Var T Z u}