Herbrandización - Herbrandization

La Herbrandización de una fórmula lógica (llamada así por Jacques Herbrand ) es una construcción que es dual a la Skolemización de una fórmula. Thoralf Skolem había considerado las Skolemizaciones de fórmulas en forma de prenexos como parte de su demostración del teorema de Löwenheim-Skolem (Skolem 1920). Herbrand trabajó con esta noción dual de Herbrandización, generalizada para aplicarse también a fórmulas no prenexas, con el fin de probar el teorema de Herbrand (Herbrand 1930).

La fórmula resultante no es necesariamente equivalente a la original. Al igual que con Skolemization, que solo conserva la satisfacibilidad , Herbrandization siendo el dual de Skolemization conserva la validez : la fórmula resultante es válida si y solo si la original lo es.

Definición y ejemplos

Sea una fórmula en el lenguaje de la lógica de primer orden . Podemos suponer que no contiene ninguna variable que esté vinculada por dos ocurrencias de cuantificador diferentes, y que ninguna variable ocurre tanto ligada como libre. (Es decir, se podría volver a redactar para asegurar estas condiciones, de tal manera que el resultado sea una fórmula equivalente). ${\ Displaystyle F}$${\ Displaystyle F}$${\ Displaystyle F}$

La Herbrandización de se obtiene de la siguiente manera: ${\ Displaystyle F}$

• Primero, reemplace las variables libres por símbolos constantes. ${\ Displaystyle F}$
• En segundo lugar, elimine todos los cuantificadores de variables que estén (1) cuantificadas universalmente y dentro de un número par de signos de negación, o (2) cuantificadas existencialmente y dentro de un número impar de signos de negación.
• Finalmente, reemplace cada una de estas variables con un símbolo de función , donde están las variables que aún están cuantificadas y cuyos cuantificadores gobiernan . ${\ Displaystyle v}$${\ Displaystyle f_ {v} (x_ {1}, \ dots, x_ {k})}$${\ Displaystyle x_ {1}, \ dots, x_ {k}}$${\ Displaystyle v}$

Por ejemplo, considere la fórmula . No hay variables gratuitas para reemplazar. Las variables son del tipo que consideramos para el segundo paso, por lo que eliminamos los cuantificadores y . Finalmente, luego reemplazamos con una constante (ya que no había otros cuantificadores que rijan ), y reemplazamos con un símbolo de función : ${\ Displaystyle F: = \ para todo y \ existe x [R (y, x) \ cuña \ neg \ existe zS (x, z)]}$${\ Displaystyle y, z}$${\ Displaystyle \ forall y}$${\ Displaystyle \ existe z}$${\ Displaystyle y}$${\ Displaystyle c_ {y}}$${\ Displaystyle y}$${\ Displaystyle z}$${\ Displaystyle f_ {z} (x)}$

${\ Displaystyle F ^ {H} = \ existe x [R (c_ {y}, x) \ wedge \ neg S (x, f_ {z} (x))].}$

La Skolemización de una fórmula se obtiene de manera similar, excepto que en el segundo paso anterior, eliminaríamos los cuantificadores de las variables que están (1) cuantificadas existencialmente y dentro de un número par de negaciones, o (2) cuantificadas universalmente y dentro de un número impar. de negaciones. Así, considerando lo mismo de arriba, su Skolemización sería: ${\ Displaystyle F}$

${\ Displaystyle F ^ {S} = \ forall y [R (y, f_ {x} (y)) \ wedge \ neg \ existe zS (f_ {x} (y), z)].}$

Para comprender el significado de estas construcciones, consulte el teorema de Herbrand o el teorema de Löwenheim-Skolem .

Ver también

• Lógica del functor de predicados

Referencias

• Skolem, T. "Investigaciones lógico-combinatorias en la satisfacibilidad o demostrabilidad de proposiciones matemáticas: una demostración simplificada de un teorema de L. Löwenheim y generalizaciones del teorema". (En van Heijenoort 1967, 252-63.)
• Herbrand, J. "Investigaciones en teoría de la prueba: Las propiedades de las proposiciones verdaderas". (En van Heijenoort 1967, 525-81.)
• van Heijenoort, J. From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931 . Prensa de la Universidad de Harvard, 1967.