On the expressive power of inquisitive team logic and inquisitive first-order logic

This paper demonstrates that while inquisitive team logic is expressively equivalent to first-order logic for sentences, its open formulas possess strictly greater expressive power, a finding that extends to standard inquisitive first-order logic where certain sentences can express non-first-order properties.

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 whole group of clues at once. This is the world of Team Semantics.

In traditional logic (the kind you might learn in school), a sentence is like a detective looking at one single suspect at a time to see if they are guilty. But in "Team Logic," the detective looks at a team of suspects (a group of assignments) simultaneously. The question isn't just "Is this person guilty?" but "Does this whole group behave in a specific way?"

This paper by Juha Kontinen and Ivano Ciardelli explores a special type of detective work called Inquisitive Logic. These detectives don't just make statements ("The butler did it"); they also ask questions ("Who did it?").

Here is the breakdown of their big discovery, explained through a simple story.

1. The Two Types of Detectives

The authors are studying two versions of these question-asking detectives:

• InqBT (The Team Detective): This detective works with a fixed group of suspects (a "team") in a single world. They can ask, "What is the value of variable $x$?" and check if the whole team agrees on the answer.
• InqBQ (The Multiverse Detective): This detective is even more powerful. They don't just look at one group; they look at multiple possible worlds (like parallel universes) at the same time. They can ask, "In all possible worlds, is the butler guilty?"

2. The Big Question: Can They Be Replaced by Simple Logic?

For a long time, logicians wondered: "Can these fancy detectives be replaced by a standard, simple logic (First-Order Logic)?"

• The Good News: If the detective only makes statements (sentences), the answer is YES. A standard logic can do everything a sentence-based Inquisitive logic can do.
• The Bad News (The Paper's Discovery): If the detective asks open questions (formulas with variables, like "What is $x$?") or looks at multiple worlds, the answer is NO.

The authors proved that these Inquisitive detectives can see things that standard logic is blind to. They can express "Second-Order" properties—complex patterns that require looking at the entire structure of the world, not just individual parts.

3. The "Finiteness" Trick (The Magic Spell)

To prove this, the authors created a "magic spell" (a logical sentence) that can tell if a world is finite (has a limited number of items) or infinite (goes on forever).

• The Analogy: Imagine you have a bag of marbles.
  • Standard Logic is like a person who can only count one marble at a time. They can say "There is a red marble" or "There is a blue marble." But they cannot say "There are exactly 5 marbles" or "There are infinitely many marbles" without getting stuck in an endless loop. Standard logic is famously bad at counting to infinity.
  • Inquisitive Team Logic is like a person who can look at the entire bag and the relationships between all the marbles at once.

The authors showed that by using a specific type of "universal quantifier" (a tool that expands the team to include every possible value), their Inquisitive detective can write a sentence that says: "This team contains a pattern that is only possible if the world is finite."

Because standard logic cannot express "finiteness," this proves that Inquisitive Team Logic is strictly more powerful than standard logic.

4. Why This Matters (The Consequences)

Because these detectives can see "finiteness" and "infinity," they break two important rules that standard logic follows:

1. The Compactness Rule: In standard logic, if a huge list of clues is contradictory, there must be a small, finite part of that list that is already contradictory.
   • The Result: Inquisitive logic breaks this. You can have a list of clues that seems fine in small chunks but becomes impossible when you look at the whole infinite list.
2. The Axiomatization Rule: In standard logic, you can write down a finite set of rules (an axiom system) to prove every true statement.
   • The Result: Because Inquisitive logic can express "finiteness," it becomes too complex to be captured by any finite set of rules. It's like trying to write a rulebook for a game that includes "infinity" as a rule; you can never finish writing the book.

5. The "Multiverse" Detective (InqBQ)

Finally, the authors took this result and applied it to the "Multiverse Detective" (InqBQ). They showed that even when you try to translate these questions into a "Two-Sorted" logic (a fancy way of organizing worlds and individuals), you still can't do it.

There are questions about the multiverse that simply cannot be translated into standard mathematical sentences. They are genuinely new kinds of logical thoughts.

Summary

Think of Standard Logic as a flashlight that shines on one object at a time. It's great for simple tasks.

Inquisitive Team Logic is a floodlight that illuminates the whole room, showing how objects relate to each other and how the whole room changes if you move one piece.

The paper proves that the floodlight can see patterns (like "the room is finite") that the flashlight simply cannot detect. This means that to fully understand questions, dependencies, and information in complex systems (like databases or quantum physics), we need this more powerful "floodlight" logic, and we can't just rely on the old, simple flashlight.

Technical Summary

Here is a detailed technical summary of the paper "On the expressive power of inquisitive team logic and inquisitive first-order logic" by Juha Kontinen and Ivano Ciardelli.

1. Problem Statement

The paper addresses three central open questions regarding the meta-theoretic properties and expressive power of Inquisitive Team Logic (InqBT) and Inquisitive First-Order Logic (InqBQ). While it is known that the sentences of InqBT are expressively equivalent to standard First-Order Logic (FOL), the status of open formulas and the full power of InqBQ sentences remained unresolved.

The specific open questions are:

1. Open Question 1 (InqBT Open Formulas): Can every open formula $\phi(x_1, \dots, x_n)$ of InqBT be systematically translated into a standard FOL sentence $\psi(R)$ (where $R$ is a relation symbol representing the team) such that the formula holds for a team if and only if the sentence holds for the relation encoding that team?
2. Open Question 2 (InqBT+[x] Sentences): Is every sentence of the extended logic InqBT+[x] (which includes a "range-generating" universal quantifier $[x]$) equivalent to a standard FOL sentence?
3. Open Question 3 (InqBQ Sentences): Can every sentence of standard Inquisitive First-Order Logic (InqBQ) be translated into a two-sorted FOL sentence (encoding worlds and individuals) such that the satisfaction relation is preserved?

2. Methodology and Framework

Logical Systems

• InqBT: A team-based logic extending FOL with inquisitive disjunction ($\lor$) and inquisitive existential ($\exists\exists$). It interprets formulas over a model $M$ and a team $X$ (a set of assignments).
• InqBT+[x]: An extension of InqBT adding the quantifier $[x]$. Semantically, $[x]\phi$ expands the team by assigning $x$ all possible values from the domain $D$ simultaneously ($X[x \to D]$), contrasting with $\forall x$ (which tests constant assignments) and $\exists\exists x$ (which tests existence of a constant assignment).
• InqBQ: The standard intensional version of inquisitive logic, interpreted over information models $(W, D, I)$ where $W$ is a set of worlds. The authors utilize a relational encoding to map InqBQ models to two-sorted FOL structures (sorts: worlds and individuals).

Key Definitions

• Flatness: A formula is "flat" if its support on a team depends only on the support of singleton sub-teams. Classical FOL formulas are flat; inquisitive formulas generally are not.
• Value Questions ($\lambda t$): Defined as $\forall x ?(x=t)$, expressing "what is the value of $t$?".
• Dependence Atoms: Defined via implication of value questions: $=(\vec{x}, y) \equiv \lambda x_1 \land \dots \land \lambda x_n \to \lambda y$. This captures functional dependence within a team.

Proof Strategy

The authors employ a counter-example construction strategy:

1. They construct specific sentences in InqBT+[x] that express finiteness (or infiniteness) of the domain.
2. Since finiteness is not expressible in FOL (by the Compactness Theorem), this immediately proves that these logics exceed FOL expressiveness.
3. They leverage the sentence expressing finiteness to construct an open formula in InqBT that cannot be translated into FOL with a team relation.
4. They adapt these constructions to the intensional setting of InqBQ using the relational encoding of worlds.

3. Key Contributions and Results

Result 1: Expressing Finiteness in InqBT+[x] (Solving Open Question 2)

The authors prove that InqBT+[x] can express the property of a model being finite.

• Construction: They define a sentence $\psi = [x][y]\phi(x,y)$, where $\phi$ involves dependence atoms and inquisitive operators.
• Logic: The formula $\phi(x,y)$ essentially asserts: "If the relation between $x$ and $y$ is a bijection (injective function) but the range is not the whole domain, then the domain of $x$ is not the whole domain."
• Mechanism: The quantifiers $[x]$ and $[y]$ allow the logic to quantify over the entire set of assignments (the full relation $D^2$). The sentence is satisfied if and only if there is no injective, non-surjective function on the domain $D$. By the Cantor-Bernstein-Schroeder theorem logic, this holds iff $D$ is finite.
• Consequence: Since FOL cannot express finiteness, InqBT+[x] is strictly more expressive than FOL.
• Further Implications:
  • Non-Compactness: The logic is not satisfiability-compact (a set of formulas can be finitely satisfiable but not globally satisfiable).
  • Non-Axiomatizability: The set of validities is not even arithmetical (it is not recursively enumerable), implying no complete recursive axiomatization exists.

Result 2: Non-Translatability of Open Formulas in InqBT (Solving Open Question 1)

The authors show that open formulas in InqBT cannot always be translated to FOL sentences with a team relation.

• Construction: They take the open formula $\phi(x,y)$ used in the finiteness proof above.
• Argument: If $\phi(x,y)$ were equivalent to an FOL sentence $\psi(R)$, then the sentence $[x][y]\phi(x,y)$ (which expresses finiteness) would be equivalent to a sentence in FOL extended with quantification over relations (effectively Second-Order Logic, but restricted to the specific relation $R$). However, the authors use an Ehrenfeucht-Fraïssé (EF) game argument to show that for any quantifier rank $k$, there exist finite and infinite structures that are indistinguishable by FOL sentences of that rank, yet they distinguish the finiteness property.
• Conclusion: There exist open formulas in InqBT that express genuinely second-order properties of teams, answering Open Question 1 negatively.

Result 3: Non-Translatability in InqBQ (Solving Open Question 3)

The authors extend the results to standard Inquisitive First-Order Logic (InqBQ).

• Adaptation: They replace the variables $x, y$ in the previous formula with constant symbols $a, b$. In the intensional setting, a state $s$ (a set of worlds) defines a relation $R_s = \{(a^w, b^w) \mid w \in s\}$.
• Full Models: They restrict attention to "full models" where the set of worlds $W$ is large enough to represent every possible binary relation on the domain $D$.
• Result: In full models, the sentence $\phi(a,b)$ holds if and only if $D$ is finite.
• Conclusion: Since the translation to two-sorted FOL would require expressing finiteness in FOL (which is impossible), InqBQ sentences cannot generally be translated into two-sorted FOL. This settles Open Question 3 negatively.

Result 4: Complexity on Finite Structures

The paper also establishes that over finite structures, InqBT can express CoNP-complete problems (specifically, the unsatisfiability of 3SAT). This demonstrates that the logic is significantly more complex than FOL (which is in PTIME for data complexity) and highlights the computational cost of its expressive power.

4. Significance

1. Resolution of Open Problems: The paper definitively answers three major open questions in the field of inquisitive logic and team semantics, showing that the expressive power of these logics extends beyond First-Order Logic in multiple dimensions (sentences with new quantifiers, open formulas, and intensional sentences).
2. Characterization of Expressive Limits: It clarifies the boundary between FOL and these inquisitive logics. While sentences of basic InqBT are FOL-equivalent, the addition of the range-generating quantifier $[x]$ or the consideration of open formulas breaks this equivalence, introducing Second-Order capabilities.
3. Meta-Theoretic Consequences: The results imply that InqBT+[x] lacks desirable meta-theoretic properties like compactness and recursive axiomatizability, similar to full Second-Order Logic. This suggests that any complete proof system for these logics must be non-recursive.
4. Theoretical Insight: The work highlights the power of team semantics combined with inquisitive operators (specifically the interaction between dependence atoms and implication) to capture global structural properties (like finiteness) that are invisible to standard Tarskian semantics or standard FOL.
5. Practical Implications: For applications in database theory and natural language semantics (where these logics are used to model dependencies and questions), the results suggest that reasoning in these full systems is inherently undecidable and computationally hard, necessitating the use of restricted fragments (like the clant or rex fragments mentioned) for practical implementation.