We prove a dichotomy theorem for the rank of the uniformly generated (i.e. expressible in First-Order (FO) Logic) propositional tautologies in both the Lovasz-Schrijver (LS) and Sherali-Adams (SA) proof systems. More precisely, we first show that the propositional translations of FO formulae that are universally true, i.e. hold in all finite and infinite models, have LS proofs whose rank is constant, independently from the size of the (finite) universe. In contrast to that, we prove that the propositional formulae that hold in all finite models but fail in some infinite structure require proofs whose SA rank grows poly-logarithmically with the size of the universe.

Up to now, this kind of so-called 'Complexity Gap' theorems have been known for Tree-like Resolution and, in somehow restricted forms, for the Resolution and Nullstellensatz proof systems. As far as we are aware, this is the first time the Sherali-Adams lift-and-project method has been considered as a propositional proof system. An interesting feature of the SA proof system is that it is static and rank-preserving simulates LS, the Lovasz-Schrijver proof system without semidefinite cuts.