Finitely monotone properties
Alexei P. Stolboushkin · 2002
A characterization of definability by positive first order formulas in terms of Fraisse-Ehrenfeucht-like games is developed. Using this characterization, an elementary, purely combinatorial, proof of the failure of Lyndon's Lemma (1959) (that every monotone first order property is expressible positively) for finite models is given. The proof implies that first order logic is a bad candidate for the role of a uniform version of positive Boolean circuits of constant depth and polynomial size. Although Lyndon's Lemma fails for finite models, same similar characterization may be established for finitely monotone properties, and we formulate a particular open problem in this direction.