¿Qué sentido tiene permitir sólo la cuantificación de las variables en la lógica de primer orden.

Question

En los idiomas de primer orden, ${ \forall }$ se permite cuantificar sólo sobre las variables, de modo que ${ \forall }v(P)$ donde $v$ es alguna variable y $P$ es una WFF es el único tipo de WFF que concierne a los cuantificadores universales permitidos en tales idiomas.

¿Por qué? No hay textos que lea sobre este tema (que debido a las limitaciones que tengo por el lugar donde vivo sólo han sido sitios como Wikipedia, Proofwiki o Wolfram MathWorld) proporcionó una explicación de por qué no se permite cuantificar sobre WFF. No veo ninguna ventaja en esto y lleva a problemas molestos como que el ZFC es una lista infinita de axiomas, que no evitan el concepto de ${ \forall }P(Q)$ , $P$ y $Q$ siendo WFFs, sólo tienes que decirlo de otra manera.

Entonces, ¿cuál es la justificación de no cuantificar sobre los WFF? ¿Cuáles son las ventajas de ese enfoque?

Answer 1

Es porque cuando nosotros hacer permiten alcances más amplios de cuantificación, las cosas se ponen extremadamente feas.

Un hecho extremadamente importante sobre la lógica de primer orden es que tiene una noción razonable de prueba si quiero saber si $ \varphi $ es verdadera siempre que cada frase en $ \Gamma $ es cierto, es decir, si $ \Gamma\models\varphi $ - Sólo busco un prueba de $ \varphi $ de $ \Gamma $ . Los hechos cruciales sobre las pruebas son:

• Una prueba es finito (en particular, puede ser representado por un único número natural).

• Puedo identificar pruebas (así que el conjunto de números correspondientes a pruebas válidas es computable ).

Pasar a una lógica más fuerte tiende a matar esta propiedad: en particular, la lógica de segundo orden - que creo que es el escenario natural de lo que estás describiendo - Se ha demostrado que no tiene un buen sistema de pruebas! De hecho, puedo escribir una frase de segundo orden que es válida (=verdadera en cada modelo) si la Hipótesis del Continuo es verdadera. Por lo tanto, determinar lo que constituye una prueba en la lógica de segundo orden requiere que primero hagamos fuertes compromisos teóricos, lo cual es poner el carro delante del caballo un poco.

Esto no quiere decir que la lógica más fuerte sea sin interés (ver el libro de Barwise y Feferman Modelo - Lógica Teórica ), simplemente que carecen de buenas propiedades que hacen manejable la lógica de primer orden (la otra propiedad principal es la La propiedad de Lowenheim-Skolem que es un poco más técnico). De hecho, podemos caracterizar la lógica de primer orden como la lógica más fuerte que satisface un par de buenas propiedades (esto es El teorema de Lindstrom ). Así que hay que hacer un intercambio, al elegir qué lógica usar.

Answer 2

Porque cuando permites la cuantificación sobre otros elementos del lenguaje en el que ya no estás primero -lógica de segundo orden, sino más bien lógica de segundo orden o superior, donde se puede cuantificar sobre variables predicadas y relacionales, variables predicadas de predicado, etc.

Ten en cuenta que lo que propones no es mejor pensado como una cuantificación sobre las WFF: no es típico permitir que el lenguaje hable de sus propias WFF y su sintaxis de esa manera. En la lógica de segundo orden, se introduce un nuevo conjunto de variables, $P^n_m$ (= el $m$ -la variable más importante para un $n$ -relación secundaria-), interpretadas como subconjuntos y más generalmente relaciones de individuos que las variables $v_i$ se extiende por todo el rango.

Así como puedes sustituir términos para las variables gratuitas de 1er orden, en la lógica de 2º orden puedes sustituir fórmulas para las variables gratuitas de 2º orden. Las reglas para hacerlo son un tanto complicadas; se explican en Introducción a la lógica matemática por Alonzo Church (publicado por primera vez en 1944, revisado en 1956).

Hay muy buenas razones para aislar la lógica de primer orden como una cosa en sí misma, digna de atención y estudio. Una es que es suficiente para formalizar la lógica tradicional, a la Aristóteles, e incluso la lógica de las relaciones desarrollada en el siglo XIX por Schroder y otros. Otra razón es que la lógica de primer orden tiene muchas propiedades "agradables" (completitud, compacidad) que ninguna de las lógicas de orden superior disfruta.

Las lógicas de segundo y tercer orden son de hecho útiles y muy expresivas pueden capturar distinciones en el lenguaje natural que la lógica de primer orden no puede. Pero las lógicas de alto orden son bestias muy diferentes: carecen de las agradables propiedades matemáticas que posee la lógica de primer orden. Por ejemplo, no hay un sistema deductivo completo. En realidad son una forma de teoría de conjuntos - "teoría de conjuntos en ropa de oveja", como dijo Quine. De hecho, la "teoría de tipos", el sistema de Russell & Whitehead que proporcionó una base para las matemáticas en una lógica de orden superior, precede a la teoría de conjuntos de Zermelo por una década más o menos. Russell mantuvo que esto establecía que las matemáticas es lógica, una filosofía de las matemáticas conocida posteriormente como logicismo pero el consenso actual es que Russell y Whitehead lograron una reducción de las matemáticas a la teoría de conjuntos, y no a lo que comúnmente se acepta como "lógica".

Answer 3

No hay nada intrínsecamente malo en cuantificar sobre las proposiciones, como en su $ \forall P$ cuantificadores.

Sin embargo, una lógica es, por definición, de "primer orden" si la cuantificación se restringe a variables que se extienden por el universo del discurso, solamente. Cuantificar sobre subconjuntos de dicho universo, sobre predicados, sobre proposiciones, etc. hace que la lógica sea de "orden superior" en su lugar.

En la lógica de primer orden, obtenemos algunos resultados metateóricos que fallan en la lógica de orden superior. Por ejemplo, obtenemos la solidez y la integridad: las fórmulas comprobables son exactamente las que se mantienen en todos los modelos posibles. En la lógica de orden superior, normalmente sólo la solidez se mantiene: las fórmulas comprobables son verdaderas en todos los modelos, pero hay algunas fórmulas que se mantienen en todos los modelos pero que no pueden ser probadas por la lógica.

---

También tenga en cuenta que, si tiene una fórmula $ \phi (P)$ que depende de $P$ de una forma extensiva, es decir. $$ (P_1 \iff P_2) \implies ( \phi (P_1) \iff \phi (P_2)) $$ entonces la cuantificación $ \forall P.\ \phi (P)$ puede expresarse en FOL como $$ \phi ({ \sf true}) \land \phi ({ \sf false}) $$ La "codificación" anterior del cuantificador universal se basa en la tautología clásica $$ (P \iff { \sf true}) \lor (P \iff { \sf false}) $$ Por lo tanto, al menos para este caso, obtenemos una formalización de primer orden equivalente.

Answer 4

En realidad puedes tener fórmulas como $ \forall P. \textbf {Apply}(P,x)$ (donde $ \textbf {Apply}$ es su símbolo de predicado que quiere denotar la aplicación del predicado $P$ a $x$ ) en una lógica de primer orden con dos tipos de variables. El problema es que no puede haber nada en las reglas que implique que la variable $P$ debe variar en fbf's, cuerdas, conjuntos o números: dependerá de su modelo.