Has it been proven that second order statements cannot be computed in polynomial time? Can some statements be proven to only be second order expresibl

Question

I have read about the Immerman Vardi theorem and I do not understand what the implications fully are. Does it say that second order logic cannot be expressible in polynomial time? Or merely that all first order logic least fixed point operator statements can be, but says nothing about SO? Has it been proven elsewhere that SO cannot be polynomial time?