Table of Contents
Fetching ...

Compactness in Team Semantics

Joni Puljujärvi, Davide Emilio Quadrellaro

TL;DR

This paper advances the model theory of team semantics by proving general compactness results for independence logic and related logics in two ways: via an ultraproduct construction with a Łoś' theorem analogue, and via saturation plus an ESO-translation framework inspired by Kontinen and Yang. The ultraproduct approach extends Lück's method to cover weak team-based logics and both lax and strict semantics, yielding a standard-style compactness theorem for sets of formulas. The second, translation-based approach reduces satisfiability for sets of formulas to existential second-order logic, using a carefully designed auxiliary theory $\Delta_\Gamma$ and saturated models to merge finite approximants into a single team. Together, these results establish satisfiability compactness for a broad family of logics over team semantics with arbitrarily many free variables, and they pave the way for further study of infinite-team model theory, including notions of type and monster models in this setting.

Abstract

We provide two proofs of the compactness theorem for extensions of first-order logic based on team semantics. First, we build upon Lück's ultraproduct construction for team semantics and prove a suitable version of Łoś' Theorem. Second, we show that by working with suitably saturated models, we can generalize the proof of Kontinen and Yang to sets of formulas with arbitrarily many variables.

Compactness in Team Semantics

TL;DR

This paper advances the model theory of team semantics by proving general compactness results for independence logic and related logics in two ways: via an ultraproduct construction with a Łoś' theorem analogue, and via saturation plus an ESO-translation framework inspired by Kontinen and Yang. The ultraproduct approach extends Lück's method to cover weak team-based logics and both lax and strict semantics, yielding a standard-style compactness theorem for sets of formulas. The second, translation-based approach reduces satisfiability for sets of formulas to existential second-order logic, using a carefully designed auxiliary theory and saturated models to merge finite approximants into a single team. Together, these results establish satisfiability compactness for a broad family of logics over team semantics with arbitrarily many free variables, and they pave the way for further study of infinite-team model theory, including notions of type and monster models in this setting.

Abstract

We provide two proofs of the compactness theorem for extensions of first-order logic based on team semantics. First, we build upon Lück's ultraproduct construction for team semantics and prove a suitable version of Łoś' Theorem. Second, we show that by working with suitably saturated models, we can generalize the proof of Kontinen and Yang to sets of formulas with arbitrarily many variables.
Paper Structure (13 sections, 16 theorems, 19 equations)

This paper contains 13 sections, 16 theorems, 19 equations.

Key Result

Theorem 1

Let $\Gamma$ be a set of formulas of independence logic. If every finite subset $\Gamma_0$ of $\Gamma$ is satisfiable, then $\Gamma$ is satisfiable.

Theorems & Definitions (38)

  • Theorem
  • Definition 2.1: Satisfiability
  • Definition 2.2: Team Property
  • Theorem 2.3: Translation to $\mathsf{ESO}$
  • Theorem 2.4: Väänänen
  • Example 2.5
  • Theorem 2.6
  • proof
  • Definition 3.1: Ultraproduct of structures
  • Definition 3.2: Ultraproduct of teams
  • ...and 28 more