Witnessed Symmetric Choice and Interpretations in Fixed-Point Logic with Counting

1. Problem Statement

The central open problem in finite model theory is the quest for a logic that captures Ptime (polynomial time). While Fagin's theorem established that existential second-order logic captures NP, finding a logic for Ptime remains unresolved. A fundamental obstacle is the mismatch between algorithms, which often rely on arbitrary choices (e.g., picking a neighbor in DFS or a pivot in Gaussian elimination), and logics, which must be isomorphism-invariant by design.

To bridge this gap, researchers have proposed Symmetric Choice (SC) and Witnessed Symmetric Choice (WSC).

• SC: Allows choosing from sets of elements that form an orbit under the automorphisms of the structure.
• WSC: A restricted form where the choice set must be an orbit, and this fact must be certified by a definable set of witnessing automorphisms. This ensures the choice is computable in Ptime.

While WSC has been studied in pure Fixed-Point Logic (IFP) and Choiceless Polynomial Time (CPT), its interaction with Logical Interpretations (reductions between structures) and Counting (as in IFPC) is not fully understood. Specifically:

1. Does adding an interpretation operator to IFPC+WSC increase its expressiveness?
2. How does the nesting depth of WSC and interpretation operators affect expressiveness?
3. Can these logics capture Ptime, or are there inherent limitations?

2. Methodology

The author introduces and analyzes two extensions of Fixed-Point Logic with Counting (IFPC):

• IFPC+WSC: IFPC extended with a fixed-point operator featuring witnessed symmetric choice.
• IFPC+WSC+I: IFPC+WSC further extended with an interpretation operator ($I$), which allows evaluating a subformula in a structure defined by an interpretation of the original structure.

The methodology relies on three main technical pillars:

1. Semantics of Reducts: The paper addresses the "reduct property" (whether a formula's truth depends only on the relations it uses). It distinguishes between subformula reduct semantics (evaluating subformulas on their specific reducts) and global reduct semantics (evaluating the whole formula on a single reduct). The paper shows these semantics have different expressive powers regarding interpretations.
2. CFI Construction (Cai-Fürer-Immerman): The paper utilizes CFI graphs, which are known to be indistinguishable by IFPC (and many other logics) but distinguishable by Ptime algorithms. The construction creates two non-isomorphic graphs (even and odd) from a base graph based on a parity function.
3. Graph Constructions:
   • Color Class Joins: A method to combine multiple graphs into a larger structure while preserving specific automorphism properties.
   • Multipedes: Asymmetric structures (no non-trivial automorphisms) based on CFI gadgets, used to force logics to fail at distinguishing isomorphism without specific operators.
   • Gluing: Combining Multipedes with CFI graphs to create structures that are asymmetric (making WSC useless) but whose isomorphism problem reduces to the CFI query via interpretation.

3. Key Contributions and Results

A. Hierarchy of Expressiveness

The paper establishes a strict hierarchy of expressiveness:
$$\text{IFPC} < \text{IFPC+WSC} < \text{IFPC+WSC+I} \leq \text{Ptime}$$

• IFPC < IFPC+WSC: Proven by showing that IFPC+WSC can define the CFI query for ordered base graphs (which IFPC cannot), while IFPC+WSC fails to distinguish certain asymmetric structures that IFPC+WSC+I can.
• IFPC+WSC < IFPC+WSC+I: This is the paper's primary separation result. The authors construct a class of asymmetric structures where isomorphism is not definable in IFPC+WSC (because there are no non-trivial orbits to choose from). However, an interpretation operator can reduce the isomorphism problem of these structures to the CFI query on ordered base graphs, which IS definable in IFPC+WSC+I.
• Implication: This proves that IFPC+WSC is not closed under FO-interpretations, a significant finding as previous logics capturing Ptime (like IFPC) are closed under interpretations.

B. Nesting Depth and Canonization

The paper investigates the cost of defining CFI graphs.

• Theorem: If IFPC+WSC+I can canonize a class of base graphs $K$, it can also canonize the CFI graphs over $K$ ($CFI(K)$).
• Necessity of Nesting: To canonize $CFI(K)$, the logic must nest one WSC-fixed-point operator and one interpretation operator more than required to canonize $K$.
• Lower Bound: The paper proves this increase in nesting depth is unavoidable. By constructing "double CFI graphs" (applying the CFI construction twice), they show that $WSC(I(IFPC))$ (one level of nesting) cannot define the CFI query for these double graphs, whereas $WSC(I(WSC(I(IFPC))))$ (two levels) can. This suggests an operator nesting hierarchy.

C. Semantics of Reducts

The paper clarifies the relationship between different semantic variants:

• Subformula Reduct Semantics ($IFPC+WSC_{sub\downharpoonright}$): More expressive; closed under one-dimensional interpretations.
• Global Reduct Semantics ($IFPC+WSC_{glob\downharpoonright}$): Less expressive; not closed under interpretations.
• Result: $IFPC+WSC_{glob\downharpoonright} < IFPC+WSC_{sub\downharpoonright}$. The interpretation operator can simulate the subformula reduct semantics, but not vice versa in the global variant.

4. Significance

1. Resolution of Open Questions: The paper definitively answers whether the interpretation operator increases the expressiveness of IFPC+WSC. The answer is yes, and it does so by enabling the logic to overcome the "orbit limitation" of WSC on asymmetric structures.
2. Limits of WSC: It demonstrates that WSC alone is insufficient for Ptime even when combined with counting, specifically because it cannot handle structures where the "choice" mechanism is rendered useless by asymmetry, unless an interpretation operator is used to transform the structure.
3. Hierarchy of Operators: The work provides the first concrete evidence of a hierarchy based on the nesting depth of WSC and interpretation operators, suggesting that deeper nesting yields strictly more expressive power.
4. Relation to Ptime: While IFPC+WSC+I is shown to be more powerful than IFPC+WSC, it is still unknown if it captures Ptime. However, the paper suggests that if an operator nesting hierarchy exists (via iterating CFI constructions), it could potentially separate IFPC+WSC+I from Ptime, as the construction does not change the signature of the structures.
5. Comparison with Other Logics: The results help position IFPC+WSC+I relative to other candidates like Rank Logic. The paper speculates that Rank Logic might define the CFI queries that IFPC+WSC+I struggles with (and vice versa), making them potentially incomparable.

Conclusion

Moritz Lichter's paper significantly advances the understanding of the interplay between symmetric choice and logical interpretations. By constructing specific graph families (asymmetric multipedes glued to CFI graphs) and analyzing the necessity of operator nesting, the author proves that interpretations strictly increase the power of witnessed symmetric choice in the presence of counting. This separation highlights the complexity of capturing Ptime and suggests that a logic for Ptime likely requires a sophisticated combination of choice, counting, and interpretation mechanisms, potentially organized in a hierarchy of nesting depths.