La skolemización es un procedimiento especial cuando reduce alguna fórmula de primer orden a su forma normal de Skolem. Por lo general, se usa cuando uno quiere probar un teorema a través de algún programa de prueba.
Ahora comienza la explicación.
Aquí puedes ver qué es un lenguaje de primer orden. Como su definición es bastante grande, no la reproduciré una vez más.
- Si la caja de sugerencias contiene lo siguiente, ¿cuál es la contraseña: 4 uvas, 1 manzana, 7 plátanos, 7 mangos, 2 piñas, 1 naranja, 8 granadas?
- ¿Cuál es una buena manera de aprender y comprender la escritura dependiente en un idioma como Idris / Coq / Agda?
- ¿Cómo podría razonar matemáticamente sobre la corrección y solidez de un programa en programación funcional?
- ¿Por qué no funciona mi función de búsqueda binaria?
- ¿Para qué se usan las mónadas en ingeniería de software?
Para comprender correctamente qué son la Skolemización y la forma normal de Skolem, primero necesitamos una noción de una forma normal previa (PNF). Una fórmula está en su PNF si tiene una forma [matemática] Q_1 \ ldots Q_n A [/ matemática] con [matemática] Q_i [/ matemática] siendo algunos cuantificadores y [matemática] A [/ matemática] es una fórmula libre de cuantificador. Es importante mencionar que para cualquier fórmula existe tal fórmula en PNF que estos dos son equivalentes.
Wiki ofrece una buena explicación sobre cómo convertir una fórmula a su PNF.
Después de convertir una fórmula a su PNF, es posible que deseemos eliminar todos sus cuantificadores existenciales, que es Skolemisation. ¿Por qué queremos hacerlo? Bueno, una vez más, muchos probadores “prefieren” trabajar con fórmulas cuantificadas universalmente.
Entonces. ¿Cómo funciona la Skolemisation? Un poco poco intuitivo porque no es una equivalencia de primer orden. Es de segundo orden. ¿Qué es la lógica de segundo orden? Se puede leer aquí. En la lógica de segundo orden, lo siguiente contiene [math] \ exist x P (x) \ equiv \ exist \ mathbf {f} P (\ mathbf {f} (x)) [/ math]. Es por eso que eliminamos cada cuantificador existencial y sustituimos cada variable cuantificada existencialmente [math] y [/ math] con un “término de Skolem” [math] f (x_1, \ ldots, x_n) [/ math] con [math] f [ / math] es un nuevo símbolo funcional y [math] x_1, \ ldots, x_n [/ math] son variables cuantificadas por cuantificadores universales que preceden al cuantificador existencial [math] \ exist y [/ math].
Tenga en cuenta que una fórmula no es en general equivalente a su Skolem NF. Sin embargo, si la fórmula es verdadera (o demostrable) en algún modelo, su SNF también será verdadera. Por qué esto conserva la satisfacción se puede leer en wiki.
