Convergence Laws for Extensions of First-Order Logic with Averaging

TL;DR

This work extends first-order logic with averaging operators to a real-valued aggregation framework, introducing Agg{Mean,LMean,Sup} with Lipschitz connectives and real-valued node features. It proves two main convergence results across Erdős–Rényi regimes: in dense graphs, closed terms converge in probability to a limit described by per-type controllers, enabling aggregate-elimination in the limit; in linear-sparse graphs, closed terms converge in distribution to a controller evaluated on a random r-core, via a game-based similarity analysis and a robust axiomatization. The approach blends local neighborhood analysis via branching processes and cores with a model-theoretic axiom system (richness, FBP-approximation, homogeneity) to control aggregation in the limit. Together, these results extend classical FO convergence laws to expressive logics with aggregation, with potential implications for SQL-like queries and graph-learning models that rely on averaged real-valued features.

Abstract

For many standard models of random structure, first-order logic sentences exhibit a convergence phenomenon on random inputs. The most well-known example is for random graphs with constant edge probability, where the probabilities of first-order sentences converge to 0 or 1. In other cases, such as certain ``sparse random graph'' models, the probabilities of sentences converge, although not necessarily to 0 or 1. In this work we deal with extensions of first-order logic with aggregate operators, variations of averaging. These logics will consist of real-valued terms, and we allow arbitrary Lipschitz functions to be used as ``connectives''. We show that some of the well-known convergence laws extend to this setting.

Theorems & Definitions (41)

• definition 1: Averaging logic
• definition 2: Interpretation of terms
• definition 3
• Theorem 1
• Theorem 2: Aggregate elimination in the dense case
• lemma 1
• proof : Proof of \ref{['thm:denseaggelim']}
• Theorem 3
• Theorem 5: Preservation of controllers by games
• proof