Mostrar código-fonte de Posto de quantificadores

Na [[lógica matemática]], o '''posto de quantificadores''' de uma [[Fórmula matemática|fórmula]] é a profundidade do aninhamento de seus quantificadores, desempenhando um papel essencial na teoria de modelos.<br />

Note que o posto de quantificadores é uma propriedade da própria fórmula (como a expressão em uma linguagem). Assim, duas fórmulas equivalentes podem ter diferentes postos, quando elas expressam duas coisas iguais porém de maneira diferente.

== Definição ==
'''Posto de Quantificadores em uma fórmula da [[Lógica de primeira ordem|Lógica de Primeira Ordem]] (FO, do inglês ''First-order language'').''' <br />

Suponha que φ seja uma fórmula da Lógica de Primeira Ordem. O posto do quantificador de φ, escrito por pq(φ) é definido como
* <math>pq(\varphi) = 0</math>, se φ for atómico.
* <math>pq(\varphi_1 \land \varphi_2) = pq(\varphi_1 \lor \varphi_2) = max(pq(\varphi_1), pq(\varphi_2))</math>.
* <math>pq(\lnot \varphi) = pq(\varphi)</math>.
* <math>pq(\exists_x \varphi) = pq(\varphi) + 1</math>.
<br />
'''Observação'''
* Escrevemos FO[n] para o conjunto de todas fórmulas φ da Lógica de Primeira Ordem com <math>pq(\varphi) \le n</math>.
* FO[n] relacionais (sem símbolos de função) são sempre de tamanho finito, isto é, contém um número finito de fórmulas.
* Note que na [[Forma Normal Prenex]] o posto do quantificador de φ é exatamente o número de quantificadores que aparecem em φ.

== Exemplos == 
* Uma sentença com posto de quantificador igual a 2:
: <big>&forall;x&exist;y R(x, y)</big> 
* Uma fórmula com posto de quantificador igual a 1:
: <big>&forall;x R(y, x) &and; &exist;x R(x, y)</big>
* Uma fórmula com posto de quantificador igual a 0:
: <big>R(x, y) &and; x &ne; y</big>
* Uma fómula na Forma Normal Prenex com posto de quantificador igual a 3:
: <math>\forall x\exists y\exists z ((\lnot x = y) \land x R y )  \land ( (\lnot x = z) \land z R x ) </math> 
* Uma fórmula com posto de quantificador igual a 2:
: <math>\forall x ( \exists y ((\lnot x = y) \land x R y ) ) \land ( \exists z ((\lnot x = z) \land z R x ) ) </math>


== Referências==
* Ebbinghaus, Heinz-Dieter; Flum, Jörg (1995), ''Finite Model Theory'', Springer,ISBN 978-3-540-60149-4.
* Grädel, Erich; Kolaitis, Phokion G.; Libkin, Leonid; Maarten, Marx; Spencer, Joel; Vardi, Moshe Y.; Venema, Yde; Weinstein, Scott (2007), ''Finite model theory and its applications'', Texts in Theoretical Computer Science. An EATCS Series, Berlin:Springer-Verlag, p. 133, ISBN 978-3-540-00428-8, Zbl 1133.03001.

[[Categoria:Teoria dos modelos]]