¿Hay alguna razón para considerar fórmulas con múltiples cuantificadores en la misma variable?

Question

Estoy muy verde en la lógica matemática, por lo que me disculpo por lo que puede ser una pregunta estúpida.

Como yo lo entiendo, la definición de un primer orden de la fórmula permite monstruosidades como

$$\exists x \neg \exists x \varphi(x),$$

$$\forall x \forall x \forall x \exists x \psi(x),$$

etc. Hay una buena razón para definir fórmulas de tal manera que estos tipos de "fórmulas" están incluidos? Por ejemplo, yo estaba tratando de escribir una prueba de la Tarski-Vaught prueba, y parece que este caso requiere un tratamiento especial, aparte de que el argumento principal.

Mi instinto natural sería definir las fórmulas de tal manera que $\exists x \phi$ es una fórmula sólo si $x$ es una variable libre en $\phi$, pero este no parece ser el modo en que las cosas se hacen generalmente.

Answer 1

Tenga en cuenta que cuando una variable específica$x$ se cuantifica repetidamente, el cuantificador anidado más cercano a la declaración cuantificada es el único cuantificador de$x$ que se aplica: niega todos y cada uno de los cuantificadores anteriores en esa variable.

Asi que:

PS

PS

Answer 2

Aquí hay un par de lugares en los que la convención se utiliza:

• Si $x$ no es libre en $\psi$ $(\forall x)\phi \lor \psi$ es equivalente a $(\forall x)(\phi \lor \psi)$. Esto es usado para ayudar a poner las fórmulas en forma normal prenex. Si $\psi$ contiene $x$ como una variable ligada, en virtud de la propuesta en la pregunta, tendríamos que modificar el algoritmo para prenex forma, porque de lo contrario $(\forall x)(\phi \lor \psi)$ podría no ser una fórmula. En particular, el algoritmo no sería puramente recursiva de la misma manera.

• Si queremos reemplazar un símbolo en una fórmula con su definición en términos de otra fórmula, normalmente podemos ignorar cualquier obligado cuantificadores en la definición. Por ejemplo, el conjunto de la teoría de la fórmula $\emptyset \subseteq x$ puede volver a escribirse en el idioma $\{\in\}$ $$(\forall z)[(\forall w)[w \not \in z] \to (\forall p)[p \in z \to p \in x]]$ $ Si hiciéramos esta dentro de una fórmula mayor, normalmente se puede simplemente ignorar cualquier exterior cuantificadores más $z$, $w$, o $p$, debido a que estos no son libres en la fórmula que se muestra arriba. Agrega una pequeña cantidad de trabajo adicional para mantener el cambio de las variables para otros.