¿Qué expresa el orden de los cuantificadores anidados en la lógica de predicados?

Una forma de interpretar el orden de los cuantificadores anidados es expresando relaciones de dependencia entre opciones de objetos seleccionados para satisfacer la fórmula cuantificada. Friedman en la Teoría de la geometría de Kant explica cómo la incapacidad de expresar tales dependencias en silogística (se necesitan tres cuantificadores anidados para definir límites, por ejemplo) obligó al cálculo y análisis tempranos a confiar en ideas intuitivas sobre el movimiento en lugar de construcciones formales. Y a su vez condujo a Kant a su teoría sintética a priori del razonamiento matemático.

Por ejemplo, ∀x∃yL(x,y) significa que existe ay para cada x, es decir, debemos seleccionar y dependiendo de x, o y=f(x). La fórmula descuantificada es L(x,f(x)) y x se puede elegir libremente, la función f entonces asegurará que se cumpla el predicado. En este ejemplo, f es una función "lovefinder", por cada x encuentra y a quien x ama. Pero ∃y∀xL(x,y) es diferente, significa que hay una y universal para todo x, una constante y=c, un amado universal, como Santa. Entonces la fórmula se reduce a L(x,c), un patrón de dependencia diferente.

El procedimiento descrito se llama Skolemización, y cualquier fórmula cuantificada se puede convertir en una forma descuantificada mediante el uso de funciones y constantes de Skolem , que revelan las dependencias explícitamente. Las variables cuantificadas universalmente se eligen libremente, y las cuantificadas existencialmente deben elegirse en función de todas las cuantificadas universalmente, cuyos ∀ preceden a sus ∃. Por ejemplo, ∀x∃y∀z∃tL(x,y,z,t) significa que x y z se eligen libremente, la elección de y nuevamente depende solo de x, entonces y=f(x), pero la elección de t depende tanto de x como de z, por lo que t=g(x,z). La fórmula de Skolemized es L(x,f(x),z,g(x,z)). Moviendo los cuantificadores y Skolemizing, verá cómo cambian las dependencias de satisfacción. Esto es lo que describe de manera equivalente el análisis de los árboles en la respuesta de Keelan.

La skolemización se puede utilizar para construir modelos de teorías formales a partir de sus propios símbolos, por así decirlo. Así es como Skolem descubrió originalmente que todas las teorías finitas de primer orden tienen modelos contables, después de todo, solo podemos generar un número contable de símbolos Skolemizados. También se utiliza para la demostración automatizada de teoremas, mediante la construcción de un modelo de Skolem donde se cumple la fórmula.

Puede ver la diferencia cuando crea un árbol de análisis para estas expresiones:

    ∀                 ∃
   / \               / \
  x   ∃             y   ∀
     / \               / \
    y   L             x   L
       / \               / \
      x   y             x   y

 ∀x∃y L(x,y)       ∃y∀x L(x,y)

_{Nota: hacer un árbol de análisis es similar a colocar paréntesis implícitos: ∀x(∃y(L(x,y))) y ∃y(∀x(L(x,y))).}

El primero significa:

• Para todo x se cumple que:
  • Existe algún y, tal que:
    • x ama a y.

O "todos aman a alguien".

El segundo significa:

• Existe ay, tal que:
  • Para todo x:
    • x ama a y.

O "hay alguien que ama a todos".