Dependence logic and IF logic (team semantics)¶
Dependence logic (Väänänen, Dependence Logic, 2007) and independence-friendly (IF) logic extend first-order logic with statements about how values relate across many assignments at once: “the value of y is a function of the value of x”, or “a witness for y is chosen without seeing x”. No single assignment can make such a statement true or false — so satisfaction is defined for a team, a set of assignments, and this page is about exactly that shift.
The toolkit’s dependence parser mode (MSFLParser(dependence=True)) accepts literals, ∧, the splitting ∨, ∀/∃, the dependence atom =(t₁, …, tₙ), and the slashed existential ∃x/{y, …}. There is deliberately no →/↔ — they have no faithful team semantics in this fragment. Evaluation is Väänänen’s strict team semantics over the same finite Structure the Tarskian evaluator uses:
What |
Function(s) |
Module |
|---|---|---|
Team satisfaction |
|
|
Sentence evaluation (team |
|
|
Teams as information states¶
A team is a set of assignments — think of a database table whose columns are variables and whose rows are assignments. A team models an information state: the rows are the possibilities you cannot yet tell apart. First-order literals are flat: the team satisfies a literal iff every row does.
from unicode_fol_kit import MSFLParser, Structure, team_satisfies
p = MSFLParser(dependence=True).parse
S = Structure(domain=[0, 1], predicates={("P", 1): {(0,)}})
team = [{"x": 0}, {"x": 1}] # two rows: x is undetermined
team_satisfies(S, team, p("P(x)")) # → False the row x=1 fails P
team_satisfies(S, team, p("¬P(x)")) # → False the row x=0 fails ¬P
team_satisfies(S, team, p("P(x) ∨ ¬P(x)")) # → True see "splitting ∨" below
Note the first two lines: on a mixed team, neither P(x) nor ¬P(x) holds — team satisfaction is not two-valued, because a team can be genuinely undecided. Two boundary facts to keep in mind:
team_satisfies(S, [], p("x ≠ x")) # → True the EMPTY team satisfies everything
team_satisfies(S, [{"x": 0}, {"x": 0}], p("=(x)")) # → True a team is a SET: duplicates collapse
The empty team is the information state with no remaining possibilities — every formula holds vacuously (the empty-team property). And every formula of dependence logic is downward closed: if X ⊨ φ then every subteam Y ⊆ X satisfies φ (Väänänen 2007, Prop. 3.10) — learning more never breaks what you knew.
Dependence atoms are functional dependencies¶
The dependence atom =(x, y) says: within this team, the value of y is a function of the value of x — exactly a database functional dependency x → y on the table. With one argument, =(x) is the constancy atom: the x column holds a single value.
# x determines y: the rows encode the function {0 ↦ 1, 1 ↦ 1}
team_satisfies(S, [{"x": 0, "y": 1}, {"x": 1, "y": 1}], p("=(x, y)")) # → True
# x = 0 maps to two different y values — the dependency fails
team_satisfies(S, [{"x": 0, "y": 0}, {"x": 0, "y": 1}], p("=(x, y)")) # → False
# constancy: =(x) fails when the column varies, holds when it does not
team_satisfies(S, [{"x": 0}, {"x": 1}], p("=(x)")) # → False
team_satisfies(S, [{"x": 1, "y": 0}, {"x": 1, "y": 1}], p("=(x)")) # → True
Functional dependencies compose, just as in Armstrong’s axioms: any team satisfying =(x, y) and =(y, z) satisfies =(x, z) (the test suite checks this exhaustively over all 256 teams on a two-element domain).
The splitting disjunction¶
Team disjunction is not “one disjunct holds”: X ⊨ φ ∨ ψ iff the team can be split into X = Y ∪ Z with Y ⊨ φ and Z ⊨ ψ. This is what made P(x) ∨ ¬P(x) true above — the team splits by P-membership. It also makes ∨ non-idempotent on dependence atoms:
team = [{"x": 0}, {"x": 1}]
team_satisfies(S, team, p("=(x)")) # → False
team_satisfies(S, team, p("=(x) ∨ =(x)")) # → True split into two constant halves!
=(x) ∨ =(x) says “the team is a union of two constant teams”, i.e. the x column takes at most two values — a strictly weaker claim than =(x). Counting continues by pigeonhole:
S3 = Structure(domain=[0, 1, 2])
team3 = [{"x": 0}, {"x": 1}, {"x": 2}]
team_satisfies(S3, team3, p("=(x) ∨ =(x)")) # → False 3 values, 2 constant parts
team_satisfies(S3, team3, p("=(x) ∨ =(x) ∨ =(x)")) # → True
Quantifiers, sentences, and the |dom| = 1 example¶
A sentence is evaluated with team_models, starting from the team {∅} containing just the empty assignment (not the empty team — that one satisfies everything). ∀x duplicates the team, extending every row with every domain element for x; ∃x supplements it, choosing one witness per row (a function F : X → dom). Watch the dependence atom interact with ∃:
from unicode_fol_kit import team_models
S1 = Structure(domain=[0])
S2 = Structure(domain=[0, 1])
team_models(S2, p("∀x ∃y (y = x)")) # → True choose F(s) = s(x)
team_models(S2, p("∀x ∃y (=(y) ∧ y = x)")) # → False
team_models(S1, p("∀x ∃y (=(y) ∧ y = x)")) # → True nothing left to vary
Worked through on S2: after ∀x the team is {{x↦0}, {x↦1}}. Now ∃y must pick a witness per row, but =(y) forces the same witness c for both rows, and y = x then demands c = 0 and c = 1. So ∀x ∃y (=(y) ∧ y = x) is true iff the domain has exactly one element — the dependence atom turned an always-true sentence into a domain-size probe.
Slashed quantifiers and imperfect information¶
IF logic reaches the same effect through imperfect information: ∃y/{x} φ chooses the witness for y uniformly in x — rows that agree on everything outside {x, y} must receive the same witness. Game-theoretically, the verifier picks y without being shown x:
team_models(S2, p("∀x ∃y (y = x)")) # → True
team_models(S2, p("∀x ∃y/{x} (y = x)")) # → False y may not look at x
team_models(S1, p("∀x ∃y/{x} (y = x)")) # → True with one element there is nothing to know
Uniformity forces a constant witness here: after ∀x, the rows {x↦0} and {x↦1} agree on every variable outside {x, y} (vacuously — there are none), so F must be constant, which is exactly the =(y) sentence above. ∀x ∃y/{x} (y = x) is true iff |dom| = 1.
The uniformity requirement is also exactly what makes signalling possible — an intermediate quantifier can leak the hidden variable back in:
team_models(S2, p("∀x ∃z (z = x ∧ ∃y/{x} (y = x))")) # → True z signals x
Because z = x, the rows now differ on z, which is outside {x, y} — so the slashed witness may vary with z, hence effectively with x. This is the classic signalling phenomenon of IF logic: hiding x is worthless if a visible variable carries the same information.
A genuine dependence sentence: the universal sink¶
On directed graphs (a binary Edge relation), the sentence
∀x ∃y (=(y) ∧ Edge(x, y))
says: every vertex has an outgoing edge, and the target is the same vertex for all of them — i.e. some single vertex receives an edge from every vertex (a universal sink). The constancy atom upgrades the row-by-row witness of ∃y into one global witness:
SINK = Structure(
domain=["a", "b", "c"],
predicates={("Edge", 2): {("a", "c"), ("b", "c"), ("c", "c"), ("a", "b")}},
)
CYCLE = Structure( # a → b → c → a: out-edges everywhere, no common target
domain=["a", "b", "c"],
predicates={("Edge", 2): {("a", "b"), ("b", "c"), ("c", "a")}},
)
sink = p("∀x ∃y (=(y) ∧ Edge(x, y))")
team_models(SINK, sink) # → True every vertex points at c
team_models(CYCLE, sink) # → False
team_models(CYCLE, p("∀x ∃y Edge(x, y)")) # → True without =(y) the witness may vary
This particular pattern is still first-order expressible — ∀x ∃y (=(y) ∧ ψ) says ∃y ∀x ψ — which gives a nice differential check against the independent Tarskian evaluator:
from unicode_fol_kit import models
fo = MSFLParser().parse("∃y ∀x Edge(x, y)")
(models(fo, SINK), models(fo, CYCLE)) # → (True, False) — agrees with team_models
In general, though, dependence atoms take you strictly beyond first-order logic: dependence logic has the full expressive power of existential second-order logic (Σ¹₁), so on finite structures it captures every NP graph property.
The honest boundary¶
Evaluation over finite structures only. That Σ¹₁ expressive power has a hard flip side: the set of valid dependence-logic sentences is not recursively enumerable — not even arithmetical (Väänänen 2007, Ch. 6). No prover, tableau, or SMT export can exist for it, so the toolkit offers exactly what is decidable: brute-force model checking over finite structures. The witness searches are exponential; above a documented bound (MAX_TEAM_SEARCH = 65536 candidates, i.e. domains up to 4 with teams up to 8 rows) they raise ValueError rather than hang.
The fragment boundaries are enforced with clear errors:
p("=(x, y)").to_z3() # raises NotImplementedError — no classical export exists
p("P ∧ Q → R") # raises (parse error) — no → in the dependence mode
team_satisfies likewise rejects nodes outside the team fragment (Implies/Iff built programmatically, ¬ applied to anything but an atom, dual negation of =(…) or ∃x/{…}, modal or fuzzy operators) with a TypeError naming the fragment. Contradictory-looking teams are not errors, though — they are information states, and the empty one satisfies everything.