este é um post muito antigo, portanto você já deve ter encontrado a resposta desejada. Desde que estudei FO (LFP) nos últimos meses. Eu tenho alguma compreensão das respostas que você precisa.
[σϕ(x⃗ ,X)|x⃗ |=ar(X)fϕP(Aar(X))↦P(Aar(x))σa estrutura A e P(Z) é o conjunto de potência do conjunto Z. E fϕ(Z)={ a⃗ ∈Aar(X) | A,a⃗ ,Z⊨ϕ }. Se esse operador for monótono, podemos capturar facilmente o ponto fixo na estrutura finita e infinita, seguindo o teorema do ponto fixo do knaster tarski mencionado nas respostas acima. Mas, o problema está testando se a fórmula escrita fora do formulário, como acima, codifica um operador monótono ou não, é indecidível; portanto, precisamos obter a melhor coisa a seguir. A positividade na variável livre de segunda ordem garante que o requisito de monotonicidade seja atendido, sendo uma indução estrutural padrão para provar esse fenômeno. A questão é, é suficiente?
Para isso, ainda não tenho uma resposta sólida, pois ainda estou lendo. Eu posso apontar para papéis nesta frente. Pelo menos as idéias explicativas que mencionei aqui são do artigo Monotone vs Positive - Ajtai, Gurevich. Ele também menciona outro artigo Extensões de ponto fixo da lógica de primeira ordem de Gurevich e Shelah, que afirmam que o operador de ponto fixo quando aplicado à fórmula positiva não perde poder expressivo quando comparado com o aplicativo sendo feito sobre fórmulas monótonas arbitrárias.