FORMA NORMAL PRENEXA, FORMA NORMAL DE SKOLEM, VALIDEZ, TAUTOLOGÍA, EL TEOREMA DE HERBRAND, EL TEOREMA DE COMPLETITUD DE GÖDEL, EL TEOREMA DE INDECIBILIDAD DE CHURCH, y COMPUTABILIDAD.

(Noviembre 2017)

                                     THORALF ALBERT SKOLEM (1887–1963)

                                       JACQUES HERBRAND (1908-1931)

KURT GÖDEL (1906-1978)

                                       

                                                           ALONZO CHURCH (1903-1995)

Un resultado clásico de LÓGICA MATEMÁTICA es el Teorema que relaciona la VALIDEZ de la Lógica de Primer Orden con la TAUTOLOGICIDAD de la Lógica proposicional en el sentido de que permite caracterizar la "validez" en la Lógica de Predicados Poliádicos usando "tautologicidad" en la Lógica Proposicional. Un enunciado de dicho teorema puede leerse en la imagen (escaneada) que se anexa al final de este párrafo, y una prueba del mismo puede hacerse usando resultados sobre FORMA NORMAL PRENEXA, FORMA NORMAL DE SKOLEM y EL TEOREMA DE HERBRAND (1930), así lo demuestran los Profesores Anil Nerode y Richard Shore en su texto LOGIC FOR APPLICATIONS, Springer-Verlag, 1993, libro que se puede encontrar y bajar en la biblioteca digital de este blog.

Observación: Hay otras pruebas  de este resultado, por ejemplo el mismo se puede obtener como un colorario de Teorema de completitud original de Gödel (1930), el cual usa Forma normal de Skolem (definida de otra manera), ver texto de Church "Introduction to mathematical logic" de 1956. También puede probarse un resultado análogo (algo distinto, pero que recoge la misma idea a mi parecer) usando el Sistema Axiomático para la Lógica de Primer Orden ofrecido por Enderton en su texto "Una Introducción Matemática a la Lógica". Etc. He realizado una vesión propia de esta demostración siguiendo a Church (1956), se puede leer en mi artículo "Dos tópicos de lógica matemática y sus fundamentos" (Episteme NS, 34, N° 1, 2014, pp. 41-65) el cual está en la web y se puede bajar, uno de los enlaces donde se encuentra es en la web de "saber ucv": http://saber.ucv.ve/ojs/index.php/rev_ens/article/view/7742 . También se puede leer dicha demostración,  de manera mucho más detallada,  en mis notas llamadas:  "El Teorema de completitud de Gödel, el Teorema del Colapso Transitivo de Mostowski y el Principio de Reflexión".   Tales notas se pueden conseguir y bajar en el siguiente enlace de "Saber UCV":  http://saber.ucv.ve/handle/123456789/17426 . Y también  se pueden conseguir (y bajar)  en la biblioteca digital de este blog.

¿Y el resultado mencionado arriba no contradice al Teorema de indecibilidad de Alonzo Church ("La Lógica de primer Orden es indecidible", 1936), ya que la lógica proposicional es decidible?: La respuesta es que NO, porque a los n términos mencionados no hay cómo elegirlos de manera efectiva, es decir, se sabe que existen pero no hay un procedimiento mecánico y efectivo que permita determinarlos.

En el siguiente enlace se puede leer (y bajar) un interesante artículo del Profesor Jesús Mosterín sobre el problema de la decisión (un resumen general de su estado actual), en el mismo se presentan varios problemas abiertos sobre fragmentos decidibles o indecidibles de la Lógica de Primer Orden, dicho artículo también se puede encontrar y bajar en la biblioteca digital de este blog, se llama "El Problema de la decisión en la lógica de predicados" (Convivium, Núm. 39, 1973):

http://www.google.com/url?sa=t&rct=j&q=&esrc=s&source=web&cd=2&ved=0CDUQFjAB&url=http%3A%2F%2Fwww.raco.cat%2Findex.php%2FConvivium%2Farticle%2Fdownload%2F76430%2F98646&ei=Jh4YUsrNGIi92gXO0YHYDQ&usg=AFQjCNExXuJfr4QclWzcHD8zHf_DY0UlTQ&sig2=4mhHkOkEgGSi0gfjI1RWlg&bvm=bv.51156542,d.b2I&cad=rja"

Otras dos conocidas aplicaciones importantes del procedimiento efectivo de Forma Normal de Skolem son las siguientes: (a) Como se dijo anteriormente en la prueba original del Teorema de Completitud de Gödel para la lógica de primer orden (1930) se usó este procedimeto (Ver libro de Church antes mencionado, y texto "Obras completas" de Gödel el cual se encuentra en la biblioteca digital de este blog y se puede bajar), y (b) En el "Cálculo de Resolución" se usa este procedimiento, tal cálculo es muy importante en PROLOG (Programación con Lógica), es decir, en el campo de la Inteligencia Artificial, ver texto LOGIC FOR APPLICATIONS anteriormente mencionado, el texto "Lógica para principiantes" de María Manzano y Antonia Huertas y el libro "Inteligencia Artificial. Un enfoque moderno" de Stuart J. Russell y Peter Norvig. Los textos de Manzano-Huertas y Russell-Norvig están en la biblioteca digital de este blog  y se pueden bajar. En la biblioteca digital están dos  versiones del libro "Lógica para principiantes" (una por  María Manzano solamente, y otra por María Manzano y Antonia Huertas), la versión de María Manzano y Antonia Huertas es la que tiene el Cálculo por resolución, ambas versiones   tienen  una exposición sistemática del Cálculo por Tablas (árboles) semánticas, el cual también es de utilidad en computabilidad y para trabajar manualmente lógica elemental, por ejemplo para decidir la validez o no validez de razonamientos formalizables en primer orden hasta predicados monádicos. Vale la pena resaltar que para decidir la validez de razonamientos formalizables con predicados poliádicos-relacionales-tal método no siempre funciona pues hay tablas semánticas que no terminan, se van al infinito , y por lo tanto no se puede decidir en estos casos específicos sobre la validez o no del razonamiento evaluado, esta limitación del método de tablas (árboles) semánticas también está en conformidad plena con el Teorema de Indecibilidad de Church para la Lógica de primer orden mencionado al inicio de esta entrada tal como ocurre con el resultado que usa Forma normal de Skolem descrito en el Teorema 10.7 que se presentó anteriormente. Los fundamentos matemáticos del método de Cálculo lógico de Tablas (árboles) semánticas pueden encontrarse en el texto mencionado anteriormente, LOGIC FOR APPLICATIONS, también en dicho texto se extiende tal método (árboles semánticos) a la Lógica Modal y a la lógica intuicionista y se demuestra matemáticamente que todo funciona bien en ambos sistemas lógicos(las estructuras de Kripke juegan un papel fundamental allí para definir la semántica en ambos sistemas lógicos y probar el teorema de completitud del Cálculo referido). Vale la pena resaltar que un Teorema importante para fundamentar matemáticamente el Cálculo por Resolución es el TEOREMA DE HERBRAND (1930), también el "ALGORITMO DE UNIFICACIÓN" es fundamental en tal método de cálculo (y en Tablas-árboles-semáticos también). Por ejemplo los procedimientos efectivamente computables de "Forma normal prenexa", "Forma normal de Skolem", "Forma normal conjuntiva" y "Unificación" permiten pasar todo el lenguaje de la lógica de primer orden a "lenguaje clausular", y así poder aplicar la "Regla de Resolución", única regla del Cálculo por Resolución. Ver texto referido anteriormente "LOGIC FOR APPLICATIONS".(Vale la pena resaltar que otro resultado lógico-matemático muy descado de Herbrand que se conoce es su demostración del Teorema de la Deducción, 1930, la primera demostración publicada que se conoce de dicho teorema, aunque se cree que hacia 1921 ya Tarski lo había probado, ver el texto de "Metalógica" de Hunter. Dicha prueba usa inducción matemática y es la que aparece expuesta en la mayoría de los manuales contemporáneos de Lógica matemática).