「‍」 Lingenic

Anonymity Logic

(⤓.md ≡ ◇.md); γ ≜ [2026-10-22T141515.691, 2026-10-22T161910.980] ∧ |γ| = 3

Anonymity Logic

Origin. Jouko Väänänen, "An atom's worth of anonymity" (Logic Journal of the IGPL 31, 2023, 1078–1083, written for John Crossley's birthday), which named the atom, read it as data anonymity, and axiomatized it. The atom itself is Pietro Galliani's non-dependence atom ("The dynamics of imperfect information", PhD thesis, Amsterdam 2012), and it is the afunctional dependency of database theory (Paredaens, De Bra, Gyssens and Van Gucht, The Structure of the Relational Database Model, 1989).

Models. The atom x̄ Υ ȳ says that publishing the team's x̄-columns reveals no row's ȳ-value: every assignment has another in the same team agreeing on x̄ and differing on ȳ. Väänänen reads it as "a strong (maximal) denial" of the dependence atom =(x̄, ȳ) — not a contradictory negation, which team logics lack, but the statement that for every single row the would-be function from x̄ to ȳ fails. Against its neighbours: independence x̄ ⊥ ȳ does not imply x̄ Υ ȳ, since ȳ may be constant; inclusion defines it, and over whole formulas the two logics coincide. The Team division's criteria name the anonymity atom alongside dependence, independence, inclusion and exclusion; this entry is that atom's record, and the record is short — one axiomatization paper and the thesis it builds on.

Formalism.

Teams: X ⊆ {s : s an assignment on dom}; satisfaction is M, X ⊨ φ. Variables read as database attributes; an assignment is a record.

The anonymity atom: M, X ⊨ x̄ Υ ȳ iff ∀s ∈ X ∃s′ ∈ X : s′(x̄) = s(x̄) ∧ s′(ȳ) ≠ s(ȳ) "x̄ leaves ȳ anonymous": no row's ȳ-value is derivable from its x̄-value.

Closure: Not downward closed, not upward closed. Closed under unions — the inclusion-logic side of the family, not the dependence side. The empty team and the full team (domain of at least two elements) always satisfy x̄ Υ ȳ. Each atom is a first-order property of the team.

Relation to the other atoms: Incompatible with =(x̄, ȳ) on nonempty teams, and stronger than its failure: dependence breaks at every row. Definable in inclusion logic: x̄ Υ ȳ ⟺ ∃ū(¬ū = ȳ ∧ x̄ū ⊆ x̄ȳ) First-order logic with Υ ≡ inclusion logic (Galliani 2012).

Axioms (Väänänen 2023): A1 Permutation: x̄ȳ Υ z̄ū gives ȳx̄ Υ z̄ū and x̄ȳ Υ ūz̄. A2 Monotonicity: x̄ȳ Υ z̄ gives x̄ Υ z̄ū. A3 Cancellation: x̄ȳ Υ z̄ȳ gives x̄ȳ Υ z̄. A4 x̄ Υ ⟨⟩ gives ⊥ (anonymity of the empty tuple fails on every nonempty team). Transitivity is invalid: a four-row team satisfies x Υ y and y Υ z while satisfying x = z.

The k-anonymity atom: M, X ⊨ x̄ Υₖ ȳ iff ∀s ∈ X : |{s′(ȳ) : s′ ∈ X, s′(x̄) = s(x̄)}| ≥ k Each published x̄-value is compatible with at least k values of ȳ. Υ₁ is trivially true; Υ₂ is Υ. Axioms A1–A4 adapted (monotonicity lowers k) plus chaining: x̄ Υₖ₁ y₁, x̄y₁ Υₖ₂ y₂, …, x̄y₁…yₙ₋₁ Υₖₙ yₙ give x̄ Υₖ₁·…·ₖₙ y₁…yₙ.

Symbols.

SymbolUnicodeNameMeaning
ΥU+03A5Greek capital upsilon / Anonymity atomx̄ Υ ȳ: every row has a mate agreeing on x̄ and differing on ȳ
Υₖ—k-anonymity atomAt least k values of ȳ behind each published x̄-value
=(x̄,ȳ)—Dependence atomThe atom Υ maximally denies
⊆U+2286Subset / Inclusion atomThe atom that defines Υ; also subteam
⊥U+22A5Up tack / FalsumThe inconsistency A4 derives
⊨U+22A8True / SatisfactionBetween a model-team pair and a formula
∀U+2200Universal quantifierRanges over members of the team
∃U+2203Existential quantifierThe witnessing mate in the same team
∈U+2208Element ofAssignment belonging to a team
≠U+2260Not equal toThe difference on ȳ that anonymity requires
X—TeamSet of assignments; the published table
s—AssignmentA row; an individual's record
GFP⁺—Positive greatest fixed pointThe class the logic captures, through inclusion logic

Metatheory. Väänänen (2023) proved the axioms A1–A4 complete for consequence among anonymity atoms: Σ ⊢ x̄ Υ ȳ iff every team satisfying Σ satisfies x̄ Υ ȳ. For k-anonymity atoms he proved completeness for the simple case (a single variable on the right) and conjectured it in general — the paper's open problem. The expressive theory transfers whole from inclusion logic, since Galliani (2012) proved first-order logic with non-dependence atoms equivalent to it: sentences capture positive greatest-fixed-point logic and hence PTIME over ordered finite structures (Galliani and Hella 2013), the logic is union closed and not downward closed, the empty team satisfies everything, and consequence for the full logic is, in Väänänen's words, badly non-axiomatizable. Hella, Luosto and Väänänen, "Dimension in team semantics" (Mathematical Structures in Computer Science 34, 2024) place the atom in the arity hierarchy: (k+1)-ary anonymity atoms, like the other four atom families, are not definable from atoms of smaller arity. Beyond the atomic axiomatizations, the inclusion-logic equivalence and the dimension bounds, little is settled; the fragment-complexity programme the paper points to has only early results (Durand, Kontinen and Väänänen, "Modular SAT-based techniques for reasoning tasks in team semantics", 2022).

Applies to. The logic of data publication: which attribute sets can be released while others stay underivable, and k-anonymity as a graded strengthening. Database dependency theory, where the atom is the afunctional dependency. Comparative team semantics, as the union-closed family's second native atom.

Limitations. The atom is, in Väänänen's words, "the most basic form of anonymity, not sufficient for practical applications" — one differing mate per row; Υₖ raises the count to k and no further. Anonymity does not survive passing to subteams: deleting rows can delete every witness, which read as a privacy fact says a published subset of an anonymous table need not be anonymous. Transitivity fails, so anonymity declarations do not compose along a chain of attributes. Expressively the atom adds nothing to inclusion logic, so its contribution is the axiomatization and the privacy reading, not new strength — and it inherits inclusion logic's ceilings, including the lack of a compositional contradictory negation. The general completeness question for k-anonymity atoms is open, and full first-order consequence with the atom has no recursive axiomatization. The empty team satisfies every formula, so the existence of any data at all cannot be stated inside the logic.

© 2026 Lingenic LLC