pith. sign in

arxiv: 2210.07869 · v8 · submitted 2022-10-14 · 💻 cs.LO · math.LO

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

Moritz Lichter This is my paper

Pith reviewed 2026-05-24 11:14 UTC · model grok-4.3

classification 💻 cs.LO math.LO
keywords witnessed symmetric choicefixed-point logic with countingfirst-order interpretationsCFI graphsexpressiveness separationcanonizationlogic for PTime
0
0 comments X

The pith

Fixed-point logic with counting plus witnessed symmetric choice is not closed under first-order interpretations.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper investigates whether witnessed symmetric choice already gives fixed-point logic with counting enough flexibility, or whether an extra interpretation operator is still needed to reach higher expressiveness. It establishes a separation by proving that the logic without the interpretation operator fails to remain closed when first-order interpretations are applied. It also shows that allowing multiple nested witnessed symmetric choice operators adds strictly more power than a single level. A reader would care because these results clarify how choice mechanisms and structure reinterpretation interact in logics that try to capture polynomial-time properties without breaking isomorphism invariance.

Core claim

IFPC+WSC is not closed under FO-interpretations and is therefore properly weaker than IFPC+WSCI. Nesting WSC operators increases expressiveness, and if IFPC+WSC+I canonizes a class of base graphs then it also canonizes the corresponding CFI graphs, unlike the behavior in several other logics.

What carries the argument

The witnessed symmetric choice operator, which selects from definable orbits only when certified by definable witnessing automorphisms, together with the interpretation operator that evaluates formulas inside the structure produced by an FO-interpretation.

If this is right

  • IFPC+WSC cannot define every property that IFPC+WSCI can define.
  • A single level of WSC is strictly weaker than multiple nested levels.
  • Canonization of base graphs transfers to their CFI graphs inside IFPC+WSC+I.
  • The combination of WSC and interpretations behaves differently from the combination of WSC with pure fixed-point logic.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Similar non-closure results may hold for other choice operators once interpretations are allowed.
  • The separation suggests that any candidate logic for PTime may need a tightly integrated treatment of choice and reinterpretation rather than separate operators.
  • Further graph classes could be used to test whether the nesting benefit of WSC persists beyond CFI constructions.

Load-bearing premise

The CFI graph constructions and the definability of their witnessing automorphisms survive when the interpretation operator is applied.

What would settle it

An explicit FO-interpretation of a structure on which every IFPC+WSC formula fails to match the result of the corresponding IFPC+WSCI formula, or a CFI graph whose witnessing automorphisms cease to be definable after interpretation.

read the original abstract

At the core of the quest for a logic for PTime is a mismatch between algorithms making arbitrary choices and isomorphism-invariant logics. One approach to overcome this problem is witnessed symmetric choice. It allows for choices from definable orbits which are certified by definable witnessing automorphisms. We consider the extension of fixed-point logic with counting (IFPC) with witnessed symmetric choice (IFPC+WSC) and a further extension with an interpretation operator (IFPC+WSC+I). The latter operator evaluates a subformula in the structure defined by an interpretation. This structure possibly has other automorphisms exploitable by the WSC-operator. For similar extensions of pure fixed-point logic (IFP) it is known that IFP+WSCI simulates counting which IFP+WSC fails to do. For IFPC+WSC it is unknown whether the interpretation operator increases expressiveness and thus allows studying the relation between WSC and interpretations beyond counting. We separate IFPC+WSC from IFPC+WSCI by showing that IFPC+WSC is not closed under FO-interpretations. Additionally, we prove that nesting WSC-operators increases the expressiveness using the so-called CFI graphs. We show that if IFPC+WSC+I canonizes a particular class of base graphs, then it also canonizes the corresponding CFI graphs. This differs from various other logics, where CFI graphs provide difficult instances.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper studies extensions of fixed-point logic with counting (IFPC) by witnessed symmetric choice (WSC) and an additional interpretation operator (I). It claims two main results: (1) IFPC+WSC is not closed under FO-interpretations, separating it from the stronger IFPC+WSCI; (2) nesting WSC operators strictly increases expressive power, established via CFI-graph constructions. It further shows that IFPC+WSC+I canonizes the CFI graphs whenever it canonizes the corresponding base graphs.

Significance. If the claims hold, the work provides the first separation between WSC and WSCI in the presence of counting, extending known results for pure IFP. The canonization transfer to CFI graphs is a positive result that contrasts with the behavior of many other logics on the same graphs and supplies concrete evidence that interpretations interact non-trivially with WSC. The explicit constructions and the nesting result are strengths that make the separation falsifiable and technically substantive.

major comments (1)
  1. [CFI-graph construction and interpretation application] The non-closure claim rests on the preservation of definable witnessing automorphisms when an FO-interpretation is applied to the CFI graphs. The manuscript must contain an explicit lemma (likely in the CFI section) showing that the witnessing functions and their orbits remain definable after interpretation; without this step the separation does not follow.
minor comments (2)
  1. [Preliminaries] Notation for the WSC and I operators should be introduced with a single consistent syntax diagram or table early in the paper.
  2. [Abstract] The abstract states that 'nesting WSC-operators increases the expressiveness'; the corresponding theorem number should be cited in the abstract for immediate reference.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading of the manuscript and the positive evaluation of its significance. We address the single major comment below.

read point-by-point responses

  1. Referee: [CFI-graph construction and interpretation application] The non-closure claim rests on the preservation of definable witnessing automorphisms when an FO-interpretation is applied to the CFI graphs. The manuscript must contain an explicit lemma (likely in the CFI section) showing that the witnessing functions and their orbits remain definable after interpretation; without this step the separation does not follow.

    Authors: We agree that the non-closure argument would benefit from an explicit lemma establishing that the witnessing automorphisms and their orbits remain definable after the FO-interpretation is applied to the CFI graphs. In the revised manuscript we will insert such a lemma (in the section treating the CFI construction) that spells out the preservation of the relevant definable functions and orbits under the interpretation. This addition will render the separation between IFPC+WSC and IFPC+WSCI fully self-contained. revision: yes

Circularity Check

0 steps flagged

No circularity: proof-based separation via explicit constructions

full rationale

The paper establishes separations between IFPC+WSC and IFPC+WSCI through explicit constructions on CFI graphs and FO-interpretations, showing non-closure and increased expressiveness from nesting WSC operators. These are standard proof techniques in descriptive complexity that rely on definability arguments and graph constructions rather than any self-definitional equivalence, fitted parameters renamed as predictions, or load-bearing self-citations that reduce the central claim to its own inputs. No equations or steps in the provided abstract or description reduce the result to a prior self-citation chain or ansatz smuggling; the derivation remains self-contained against external benchmarks of logical expressiveness.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The work relies on standard definitions of fixed-point logic, counting, and witnessed symmetric choice from prior literature; no new free parameters, ad-hoc axioms, or invented entities are introduced in the abstract.

axioms (2)
  • standard math Standard semantics of fixed-point logic with counting and witnessed symmetric choice operators as defined in prior work.
    Invoked throughout to define IFPC+WSC and IFPC+WSCI.
  • domain assumption FO-interpretations preserve the relevant automorphism structure in the manner required for the closure argument.
    Central to the non-closure proof.

pith-pipeline@v0.9.0 · 5775 in / 1371 out tokens · 22773 ms · 2026-05-24T11:14:22.816928+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.