The Expressive Power of Two-Variable Least Fixed-Point Logics

Symmetric Circuits for Rank Logic

ACM Transactions on Computational Logic ◽

10.1145/3476227 ◽

2022 ◽

Vol 23 (1) ◽

pp. 1-35

Author(s):

Anuj Dawar ◽

Gregory Wilsenach

Keyword(s):

Fixed Point ◽

Expressive Power ◽

Broad Framework ◽

The Individual ◽

Rank Of A Matrix

Fixed-point logic with rank (FPR) is an extension of fixed-point logic with counting (FPC) with operators for computing the rank of a matrix over a finit field. The expressive power of FPR properly extends that of FPC and is contained in P, but it is not known if that containment is proper. We give a circuit characterization for FPR in terms of families of symmetric circuits with rank gates, along the lines of that for FPC given by Anderson and Dawar in 2017. This requires the development of a broad framework of circuits in which the individual gates compute functions that are not symmetric (i.e., invariant under all permutations of their inputs). This framework also necessitates the development of novel techniques to prove the equivalence of circuits and logic. Both the framework and the techniques are of greater generality than the main result.

Download Full-text

On fixed-point logic with counting

Journal of Symbolic Logic ◽

10.2307/2586569 ◽

2000 ◽

Vol 65 (2) ◽

pp. 777-787 ◽

Cited By ~ 3

Author(s):

Jörg Flum ◽

Martin Grohe

Keyword(s):

Fixed Point ◽

Complexity Theory ◽

Polynomial Time ◽

Planar Graphs ◽

Expressive Power ◽

Descriptive Complexity ◽

Main Motivation ◽

First Order ◽

Finite Structures ◽

Tree Width

One of the fundamental results of descriptive complexity theory, due to Immerman [13] and Vardi [18], says that a class of ordered finite structures is definable in fixed-point logic if, and only if, it is computable in polynomial time. Much effort has been spent on the problem of capturing polynomial time, that is, describing all polynomial time computable classes of not necessarily ordered finite structures by a logic in a similar way.The most obvious shortcoming of fixed-point logic itself on unordered structures is that it cannot count. Immerman [14] responded to this by adding counting constructs to fixed-point logic. Although it has been proved by Cai, Fürer, and Immerman [1] that the resulting fixed-point logic with counting, denoted by IFP+C, still does not capture all of polynomial time, it does capture polynomial time on several important classes of structures (on trees, planar graphs, structures of bounded tree-width [15, 9, 10]).The main motivation for such capturing results is that they may give a better understanding of polynomial time. But of course this requires that the logical side is well understood. We hope that our analysis of IFP+C-formulas will help to clarify the expressive power of IFP+C; in particular, we derive a normal form. Moreover, we obtain a problem complete for IFP+C under first-order reductions.

Download Full-text

On the expressive power of monadic least fixed point logic

Theoretical Computer Science ◽

10.1016/j.tcs.2005.10.025 ◽

2006 ◽

Vol 350 (2-3) ◽

pp. 325-344 ◽

Cited By ~ 6

Author(s):

Nicole Schweikardt

Keyword(s):

Fixed Point ◽

Expressive Power

Download Full-text

On the Expressive Power of Monadic Least Fixed Point Logic

Automata, Languages and Programming - Lecture Notes in Computer Science ◽

10.1007/978-3-540-27836-8_93 ◽

2004 ◽

pp. 1123-1135 ◽

Cited By ~ 2

Author(s):

Nicole Schweikardt

Keyword(s):

Fixed Point ◽

Expressive Power

Download Full-text

Martin Otto. The expressive power of fixed-point logic with counting. The journal of symbolic logic, vol. 61 (1996), pp. 147–176. - Martin Otto. Bounded variable logics and counting. A study infinite models. Lecture notes in logic, no. 9. Springer, Berlin, Heidelberg, New York, etc., 1997, ix + 183 pp.

Journal of Symbolic Logic ◽

10.2307/2586606 ◽

1998 ◽

Vol 63 (1) ◽

pp. 329-331

Author(s):

Anuj Dawar

Keyword(s):

New York ◽

Fixed Point ◽

Expressive Power ◽

Symbolic Logic ◽

Lecture Notes

Download Full-text

The expressive power of fixed-point logic with counting

Journal of Symbolic Logic ◽

10.2307/2275602 ◽

1996 ◽

Vol 61 (1) ◽

pp. 147-176 ◽

Cited By ~ 24

Author(s):

Martin Otto

Keyword(s):

Fixed Point ◽

Polynomial Time ◽

Natural Extension ◽

Expressive Power ◽

Generic Model ◽

Point Counting ◽

Ordered Structures ◽

Relational Structures ◽

Positive Assessment

AbstractWe study the expressive power in the finite of the logic Fixed-Point+Counting, the extension of first-order logic which is obtained through adding both the fixed-point constructor and the ability to count.To this end an isomorphism preserving (‘generic’) model of computation is introduced whose PTime restriction exactly corresponds to this level of expressive power, while its PSpace restriction corresponds to While+Counting. From this model we obtain a normal form which shows a rather clear separation of the relational vs. the arithmetical side of the algorithms involved.In parallel, we study the relations of Fixed-Point+Counting with the infinitary logics and the corresponding pebble games.The main result, however, involves the concept of an arithmetical invariant. By this we mean a functor taking every finite relational structure to an expansion of (an initial segment of) the standard arithmetical structure. In particular its values are linearly ordered structures. We establish the existence of a family of arithmetical invariants with the following properties:• The invariants themselves can be evaluated in polynomial time.• A class of finite relational structures is definable in Fixed-Point+Counting if and only if membership can be decided in polynomial time on the basis of the values of one of the invariants.• The invariant r classifies all finite relational structures exactly up to equivalence with respect to the logic We also give a characterization of Fixed-Point+Counting in terms of sequences of formulae in the : It corresponds exactly to the polynomial time computable families (φn)n ∈ ω in these logics.Towards a positive assessment of the expressive power of Fixed-Point+Counting, it is shown that the natural extension of fixed-point logic by Lindström quantifiers, which capture all the PTime computable properties of cardinalities of definable predicates, is strictly weaker than what we get here. This implies in particular that every extension of fixed-point logic by means of monadic Lindström quantifiers, which stays within PTime, must be strictly contained in Fixed-Point+Counting.

Download Full-text

Beyond first-order logic

A First Course in Logic ◽

10.1093/oso/9780198529804.003.0013 ◽

2004 ◽

Author(s):

Shawn Hedman

Keyword(s):

Fixed Point ◽

Expressive Power ◽

Second Order ◽

Order Logic ◽

Compactness Theorem ◽

First Order Logic ◽

First Order ◽

Skolem Theorem ◽

Additional Rule ◽

Second Order Logic

We consider various extensions of first-order logic. Informally, a logic 𝓛 is an extension of first-order logic if every sentence of first-order logic is also a sentence of 𝓛. We also require that 𝓛 is closed under conjunction and negation and has other basic properties of a logic. In Section 9.4, we list the properties that formally define the notion of an extension of first-order logic. Prior to Section 9.4, we provide various natural examples of such extensions. In Sections 9.1–9.3, we consider, respectively, second-order logic, infinitary logics, and logics with fixed-point operators. We do not provide a thorough treatment of any one of these logics. Indeed, we could easily devote an entire chapter to each. Rather, we define each logic and provide examples that demonstrate the expressive power of the logics. In particular, we show that none of these logics has compactness. In the final Section 9.4, we prove that if a proper extension of first-order logic has compactness, then the Downward Löwenhiem–Skolem theorem must fail for that logic. This is Lindstrom’s theorem. The Compactness theorem and Downward Löwenheim–Skolem theorem are two crucial results for model theory. Every property of first-order logic from Chapter 4 is a consequence of these two theorems. Lindström’s theorem implies that the only extension of first-order logic possessing these properties is first-order logic itself. Second-order logic is the extension of first-order logic that allows quantification of relations. The symbols of second-order logic are the same symbols used in first-order logic. The syntax of second-order logic is defined by adding one rule to the syntax of first-order logic. The additional rule makes second-order logic far more expressive than first-order logic. Specifically, the syntax of second-order logic is defined as follows. Any atomic first-order formula is a formula of second-order logic. Moreover, we have the following four rules: (R1) If φ is a formula then so is ￢φ. (R2) If φ and ψ are formulas then so is φ ∧ ψ. (R3) If φ is a formula, then so is ∃x φ for any variable x.

Download Full-text

Fixed Point Logics

Bulletin of Symbolic Logic ◽

10.2178/bsl/1182353853 ◽

2002 ◽

Vol 8 (1) ◽

pp. 65-88 ◽

Cited By ~ 22

Author(s):

Anuj Dawar ◽

Yuri Gurevich

Keyword(s):

Fixed Point ◽

Fixed Points ◽

Model Theory ◽

Predicate Logic ◽

Expressive Power ◽

Finite Model ◽

Finite Model Theory ◽

Inductive Definitions ◽

The Relationship ◽

Second Order Logic

AbstractWe consider fixed point logics, i.e., extensions of first order predicate logic with operators defining fixed points. A number of such operators, generalizing inductive definitions, have been studied in the context of finite model theory, including nondeterministic and alternating operators. We review results established in finite model theory, and also consider the expressive power of the resulting logics on infinite structures. In particular, we establish the relationship between inflationary and nondeterministic fixed point logics and second order logic, and we consider questions related to the determinacy of games associated with alternating fixed points.

Download Full-text