Use of generating functions in logic

Question

Are there any uses of generating functions within logic, in particular to count how many models exists for a given theory $T$, say in FOL?

The concrete problem I'm hoping to apply this to involves counting the number of states witnessed by a given program. In this application some ad-hoc combinatorial arguments can be made for any instance, but it feels like there should exist a general construction scaffolded by the logic underlying our PL.

My far-reaching hope is that such functions not only exist, but are compositional in a reasonable sense. One way this could manifest: perhaps we build one such generating function for each axiom in our theory, and the generating function for the entire theory is just the product over each axiom.

Or perhaps they compose in a different manner, but the core idea remains that each connective in our logic induces an operation on these generating functions.

Regardless of my hope bearing fruit, I'd love to hear about any resources involving generating functions in logic

Answer 1

Not sure if the lambda calculus or 2-SAT counts for you as "logics" but here is a couple of recent papers presenting bijections between these formal structures of mathematical logic and "more classical" combinatorial objects. The bijections transfer certain properties of the former objects to the properties and patterns in graphs and maps, use the generating functions to enumerate them and study their asymptotic distribution.

Asymptotic Distribution of Parameters in Trivalent Maps and Linear Lambda Terms
by Olivier Bodini, Alexandros Singh, Noam Zeilberger

Exact enumeration of satisfiable 2-SAT formulae
by Sergey Dovgal, Élie de Panafieu, Vlady Ravelomanana.