Hanf normal form for first-order logic with unary counting quantifiers
Lucas Heimberg, Dietrich Kuske, Nicole Schweikardt · 2016
We study the existence of Hanf normal forms for extensions FO(Q) of first-order logic by sets Q ⊆ P(N) of unary counting quantifiers. A formula is in Hanf normal form if it is a Boolean combination of formulas ζ(x) describing the isomorphism type of a local neighbourhood around its free variables x and statements of the form "the number of witnesses y of ψ(y) belongs to (Q+k)" where Q ∈ Q, k ∈ N, and ψ describes the isomorphism type of a local neighbourhood around its unique free variable y.