Fixed-point logic with counting

Definitions and mathematical statement

Shared notation.

$\mathbb N=\{1,2,\ldots\}$, and $\mathbb Z,\mathbb Q,\mathbb R,\mathbb C$ denote the integers, rationals, reals and complex numbers. Any other conventions are specified locally.

Fixed-point logic with counting (FPC) extends first-order logic on finite structures by inflationary fixed-point operators and counting terms on an ordered numerical sort; no order on the graph's vertices or matrix indices is assumed. A perfect matching in a finite graph is a set of edges incident exactly once with each vertex. For the matrix question, follow the original BGS representation: the input contains a finite field $K$ with its field operations and a linear order on $K$, a separate unordered finite index set $I$, and a function $M:I\times I\to K$. Rows and columns have the same index set; their common reordering does not change $\det(M)$. The order on $K$ need not be compatible with its field operations.

Statement recorded in the supplied source.

(1) Is there an FPC sentence defining the existence of a perfect matching in every finite graph? (2) Is there a uniform FPC formula $\theta(a)$ in the stated matrix vocabulary which, for every such finite-field matrix and $a\in K$, holds exactly when $a=\det(M)$? Both parts ask for uniform definitions independent of graph order, matrix dimension and index ordering. [S2] [S3]

Short English statement

Can fixed-point logic with counting recognize perfect matchings, and can it compute the determinant of a square matrix with unordered indices over a finite field?

Sources

• S1 ULAM.AI and the UnsolvedMath Contributors, UnsolvedMath: A Curated Collection of Open Mathematics Problems, record 3337 (OPG-37424). CC BY 4.0. https://huggingface.co/datasets/ulamai/UnsolvedMath.
• S2 Open Problem Garden, Fixed-point logic with counting, node 37424, original problem page. Original question and full discussion. https://www.openproblemgarden.org/op/fixed_point_logic_with_counting.
• S3 Andreas Blass, Yuri Gurevich and Saharon Shelah, On polynomial time computation over unordered structures (2001; Journal of Symbolic Logic 67 (2002)), Section 6.3, Proposition 31 and Question 32, pp.39–40. https://arxiv.org/pdf/math/0102059.