Capturing dual team properties with inclusion atoms

This paper introduces propositional team-based logics that expressively capture dual downward and upward closed properties through variants of inclusion atoms, establishes their normal forms reflecting this duality, and provides sound and complete natural deduction systems for each logic.

The Gist

Imagine you are a detective trying to solve a mystery, but instead of looking at a single clue, you are looking at a group of clues (a "team"). In this paper, the author, Matilda Haggblom, is building a new set of logical tools to describe how these groups of clues behave.

Here is the story of the paper, broken down into simple concepts and analogies.

The Big Picture: Two Ways to Grow a Group

In the world of logic, properties of these "teams" usually fall into two categories: Downward and Upward.

1. Downward Closed (The "Snowball" Effect):
   Imagine a snowball rolling down a hill. If a big snowball exists, then any smaller piece of that snowball also exists.

   • The Rule: If a team satisfies a condition, then any smaller group taken from that team also satisfies it.
   • Example: "Everyone in this room is wearing a hat." If this is true for the whole room, it's definitely true for just the people in the corner.

2. Upward Closed (The "Party" Effect):
   Imagine a party. If a small group of people is having a great time, adding more people to the party won't ruin the vibe; the "great time" property grows with the group.

   • The Rule: If a team satisfies a condition, then any larger group containing that team also satisfies it.
   • Example: "There is at least one person in this room who is wearing a hat." If this is true for a small group, it remains true if you invite the whole neighborhood over.

The Problem: The "Empty" and "Full" Traps

The author noticed a tricky problem with these rules.

• If a "Downward" group includes the Full Team (everyone in the universe), it forces the group to include every possible subset, making the rule useless (trivial).
• If an "Upward" group includes the Empty Team (no one at all), it forces the group to include everyone, also making it useless.

To fix this, the author created "Quasi" versions. Think of these as "Quasi-Downward" and "Quasi-Upward" rules that carefully exclude the "Full" or "Empty" teams to keep the logic interesting and useful.

The New Tools: Inclusion Atoms

To build these logics, the author invented special "atomic" tools called Inclusion Atoms.

• The Standard Atom ($a \subseteq b$): This is like saying, "For every person in group A, there is a matching person in group B who has the same characteristics."
• The New Variants: The author tweaked these atoms to fit the specific "Upward" or "Downward" needs.
  • Some atoms only work if the team isn't empty.
  • Some atoms only work if the team isn't full.

The Four Logics: A Symmetrical Dance

The paper introduces four distinct logical languages, each designed to capture one of the four scenarios:

1. Quasi-Upward: Handles groups that grow, but ignores the "Empty" team.
2. Upward: Handles groups that grow, but ignores the "Empty" team (strictly).
3. Quasi-Downward: Handles groups that shrink, but ignores the "Full" team.
4. Downward: Handles groups that shrink, but ignores the "Full" team (strictly).

The "Aha!" Moment:
The author discovered a beautiful symmetry (duality) between these four logics.

• In the Upward logics, the formulas look like a list of "AND" statements (conjunctions).
• In the Downward logics, the formulas look like a list of "OR" statements (split-disjunctions).
  It's like looking at a reflection in a mirror: the structure is identical, but the operations are flipped.

Connection to "Might" and "Must"

The paper makes a fascinating link to everyday language:

• Upward Logics are like saying "Might."
  • Example: "There might be a red car in the parking lot." If you find one, adding more cars doesn't change the fact that there might be one.
• Downward Logics are like saying "Must."
  • Example: "There must be a red car in the parking lot." If you take cars away, you might accidentally remove the only red one, breaking the rule.

The author shows that their new "Inclusion Atoms" are mathematically equivalent to these "Might" and "Must" concepts found in other areas of logic.

The Proof System: The Rulebook

Finally, the author didn't just invent the languages; they wrote the Rulebook (Natural Deduction Systems) for each one.

• They proved that these rulebooks are Sound (you can't prove something false).
• They proved they are Complete (you can prove everything that is actually true within that logic).

Summary

Matilda Haggblom has built a set of four perfectly balanced logical tools.

• Two tools describe how groups grow (Upward).
• Two tools describe how groups shrink (Downward).
• She fixed the edge cases (Empty/Full teams) to make them practical.
• She showed that these tools are the mathematical twins of "Might" and "Must" in language.
• She provided a complete instruction manual for using them.

It's a bit like discovering that there are four perfect keys to unlock four different types of doors, and realizing that the keys are made of the same metal, just shaped differently to fit the lock.

Technical Summary

Here is a detailed technical summary of the paper "Capturing dual team properties with inclusion atoms" by Matilda H¨aggblom.

1. Problem Statement

The paper addresses the challenge of defining propositional team-based logics that are expressively complete for specific classes of team properties, specifically focusing on the duality between downward closed and upward closed properties.

In team semantics, a "team" is a set of valuations (assignments of truth values to propositional variables). Team properties are collections of teams. The paper focuses on four specific closure properties:

1. Downward Closed: If a team $T$ is in the property, all subsets $S \subseteq T$ are also in the property.
2. Upward Closed: If a team $T$ is in the property, all supersets $S \supseteq T$ are also in the property.
3. Quasi-Downward Closed: The property contains the full team ($F = 2^P$) and is downward closed for all other teams (i.e., $C \setminus \{F\}$ is downward closed).
4. Quasi-Upward Closed: The property contains the empty team ($\emptyset$) and is upward closed for all other teams (i.e., $C \setminus \{\emptyset\}$ is upward closed).

The goal is to construct logics for each of these four settings that:

• Are expressively complete (can define any team property with the relevant closure property).
• Exhibit a syntactic duality between the upward and downward settings.
• Admit sound and complete natural deduction proof systems.

2. Methodology

The author employs a novel approach using variants of inclusion atoms as the primitive atomic formulas, rather than standard propositional variables or dependence atoms.

A. Atomic Definitions

The paper introduces four types of inclusion atoms to capture the different closure properties:

1. Primitive Inclusion Atom ($x \subseteq p$): Where $x$ is a sequence of constants ($\top, \bot$) and $p$ is a sequence of propositional variables.
   • Semantics: $T \models x \subseteq p$ iff $\forall v \in T, \exists v' \in T$ such that $v(x) = v'(p)$.
   • Property: Quasi-upward closed.
2. Nonempty Primitive Inclusion Atom ($x \mathbin{\text{\textopeno}} p$):
   • Semantics: $T \neq \emptyset$ and $T \models x \subseteq p$.
   • Property: Upward closed.
3. Dual Full Inclusion Atom ($p \mathbin{\text{\textc}} x$):
   • Semantics: $T = F$ or $T \models p \subseteq x$.
   • Property: Quasi-downward closed.
4. Dual Primitive Inclusion Atom ($p \subseteq x$):
   • Semantics: $T \models p \subseteq x$.
   • Property: Downward closed.

The paper establishes that these atoms are semantically equivalent to specific modalities:

• Upward closed atoms correspond to "might" modalities ($\Diamond$).
• Downward closed atoms correspond to "must" modalities ($\Box$).

B. Logic Construction

Four distinct logics are defined, each tailored to one of the closure properties:

• $L_{qu}$: Quasi-upward closed logic (uses $\bot$, $x \subseteq p$, $\land$, $\bigvee$).
• $L_u$: Upward closed logic (uses $\top$, $x \mathbin{\text{\textopeno}} p$, $\land$, $\bigvee$).
• $L_{qd}$: Quasi-downward closed logic (uses $\bullet$ (full team atom), $p \mathbin{\text{\textc}} x$, $\land$, $\lor$, $\bigvee$).
• $L_d$: Downward closed logic (uses $\bot$, $p \subseteq x$, $\land$, $\lor$, $\bigvee$).

C. Normal Forms and Proof Systems

To prove expressive completeness, the author constructs normal forms for each logic. These normal forms express any target team property as a global disjunction ($\bigvee$) of specific "characteristic formulas" ($\psi'_T$, $\psi^*_T$, $\theta'_T$, etc.) that isolate specific teams.

For each logic, a Natural Deduction system is defined. These systems include:

• Standard rules for conjunction and disjunction.
• Specific rules for the inclusion atoms (e.g., Projection, Permutation, and Extension rules).
• Special handling for the empty team ($\bot$) and full team ($\bullet$) atoms.

3. Key Contributions

1. Symmetric Logic Framework: The paper successfully defines four logics that form a symmetric picture. The syntax and semantics of the upward-closed logics are the exact duals of the downward-closed logics.

   • Duality: Upward closed logics use global disjunction ($\bigvee$) and inclusion atoms with constants on the left ($x \subseteq p$). Downward closed logics use split disjunction ($\lor$) and dual atoms with constants on the right ($p \subseteq x$).
   • Quasi-variants: The "quasi" variants specifically handle the inclusion of the empty team (for upward) or full team (for downward) without trivializing the logic (i.e., avoiding the case where the property becomes the set of all teams).

2. Expressive Completeness:

   • Theorem: Each of the four logics is expressively complete for the class of all team properties satisfying its respective closure condition.
   • Mechanism: This is achieved via the construction of normal forms (e.g., $\Psi'_C = \bigvee_{T \in C} \psi'_T$) which can define any non-trivial team property in that class.

3. Connection to Modal Logic:

   • The paper explicitly links the inclusion atoms to might modalities ($\Diamond$) in the upward-closed setting and must modalities ($\Box$) in the downward-closed setting.
   • For example, $\top \subseteq p$ is semantically equivalent to $\Diamond p$, and $p \subseteq \top$ is equivalent to $\Box p$. This provides a semantic bridge between team logic and modal logic.

4. Sound and Complete Proof Systems:

   • The author provides natural deduction systems for all four logics.
   • Completeness Theorems: Proven by showing that every formula is provably equivalent to its normal form, and that semantic entailment implies syntactic derivability within these systems.
   • Novel rules (like $\subseteq Ext$ and $\mathbin{\text{\textc}} Ext$) are introduced to handle the specific properties of the inclusion atoms.

4. Results

• Expressive Power: The logics $L_{qu}, L_u, L_{qd}, L_d$ precisely capture the classes of quasi-upward, upward, quasi-downward, and downward closed team properties, respectively.
• Normal Forms:
  • Upward/Quasi-upward: Normal forms are global disjunctions of conjunctions of inclusion atoms.
  • Downward/Quasi-downward: Normal forms are global disjunctions of split-disjunctions of dual inclusion atoms.
• Compactness: All four logics are shown to be compact, inheriting this property from inquisitive logic arguments.
• Duality in Disjunction: In the quasi-upward setting, global disjunction ($\bigvee$) and split disjunction ($\lor$) coincide. In the upward setting, split disjunction coincides with conjunction ($\lor \equiv \land$).

5. Significance

• Unification of Team Logics: This work unifies the study of team logics by demonstrating that upward and downward closed properties are not just semantic opposites but can be captured by syntactically dual logical systems using a unified atomic framework (inclusion atoms).
• New Atomic Primitives: By moving away from standard propositional variables as the primary atoms and using inclusion atoms with constants, the paper offers a more flexible tool for defining team properties that align naturally with modal concepts (possibility/necessity).
• Foundational for Future Research: The paper sets the stage for combining these logics (e.g., creating a logic that handles both empty and full teams simultaneously) and exploring their computational complexity, connections to natural language, and modal variants.
• Proof-Theoretic Rigor: Providing sound and complete natural deduction systems for these specific closure properties fills a gap in the literature, as many team logics previously lacked complete proof systems or relied on less symmetric axiomatizations.

In summary, the paper provides a rigorous, symmetric framework for propositional team logics, leveraging inclusion atoms to create a dualistic system that perfectly mirrors the semantic duality between upward and downward closure, while establishing robust proof-theoretic foundations for each variant.