¿Por qué se cuantifica la lógica proposicional no forma parte de la lógica de primer orden?

Question

Si la lógica proposicional se extiende por cuantificadores ( $\forall$ $\exists$ ) sin la adición de funciones y relaciones (o incluso de los objetos y la igualdad, es decir, podemos cuantificar sobre proposicional-variables), el resultado podría ser llamado cuantificado lógica proposicional. Este sistema es más expresivo de la lógica proposicional (el verdadero cuantificado Booleano fórmulas son un PSPACE-completo idioma), pero menos expresiva de la lógica de primer orden. Porque la lógica de primer orden es considerado a veces como "la verdadera lógica", me parece interesante que no incluya este subsistema. (De segundo orden, lógica por otro lado lo incluye como un subsistema.)

Nota: Aún así esta pregunta es similar a otra pregunta acerca de la omisión de partes de primer orden de la lógica, de la motivación detrás de esta pregunta es diferente. Surgió por consideraciones acerca de la relación entre las constantes y variables (y por qué no son "sólo" countably de muchas variables diferentes), y que debe haber una similar relación entre las proposiciones y silogismos-variables. (Una relacionada con la pregunta sería "¿cómo muchas de las diferentes variables/proposicional-variables son necesarios para deducir todas las consecuencias de un determinado conjunto de axiomas".)

Answer 1

Este sistema de lógica proposicional cuantificada es fácil de interpretar en la lógica de primer orden. Hacemos una teoría de la $T$ que tiene un único unario relación símbolo, decir $P$, y ningún otro de los símbolos en la firma, ni siquiera la igualdad. Entonces, para cuantificar el exceso de "variables proposicionales", podemos cuantificar por los elementos, en primer orden de la lógica como de costumbre. Para cada elemento $x$ en un modelo de $T$, $Px$ es verdadero o falso, de modo que los elementos del modelo pueden ser tratados como si fueran variables proposicionales.

Así, la cuantificado frase proposicional $(\exists Q)(\forall R)[R \lor Q]$ se interpreta en $T$$(\exists q)(\forall r)[Pr \lor Pq]$. De esta manera, cada frase de cuantificados lógica proposicional se interpreta como una sentencia de $T$, y vice-versa.

Si queremos agregar constante de símbolos a $T$, que sería equivalente a la adición constante (es decir, no variable) proposicional variables cuantificadas lógica proposicional.

Yo diría que la razón principal por la que no molestan a tener cuantificados proposicional variables en la "costumbre" marco para la lógica de primer orden es que no son útiles para la formalización de las típicas teorías matemáticas (teoría de grupos, lineal órdenes, la teoría de conjuntos, la aritmética, etc.), y un objetivo central en la mayoría de las presentaciones de la lógica de primer orden es ser capaz de formalizar estas teorías. Lo mismo vale para los $\lambda$ términos para definir funciones. No hay ninguna razón por la que no pudo ser incluido en el primer fin de teorías, y de hecho a veces lo son, pero la mayoría de las presentaciones no tienen ningún uso para ellos.