Herbrandización

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.

Sea una fórmula en el lenguaje de la lógica de primer orden . Podemos suponer que no contiene ninguna variable que esté limitada por dos ocurrencias de cuantificadores diferentes, y que ninguna variable se produce tanto enlazada 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}$

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)}$

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}$