A first-order formula is positive if it does not contain any negations. It is not so difficult to prove that such formulas are preserved under surjective homomorphism, meaning that if some model M satisfies it, and there is a surjective homomorphism from M onto M′, then M′ also satisfies the formula. Lyndon’s theorem states that all first-order formulae preserved in this way are equivalent to a positive formula. Hence, Lyndon’s theorem characterizes syntactically this preservation property. Statement of similar forms are usually called ‘preservation theorems’. This theorem, as it is often the case for preservation theorems for first-order is not true in the finite: this signifies that there are first-order formulae which are preserved under surjective homomorphism between finite models, but are not equivalent to any positive formula.

In this presentation, we will give a panorama of various classical preservation theorems for first-order logic. We will then present a proof of Lyndon’s theorem, and a proof that it does not hold in the finite case (this last construction is a joint work with Arnaud Durant, Amélie Gheerbrant and Cristina Sirangelo).