Investigaciones sobre el Cálculo de Predicados

Título original:

Investigations into the Predicate Calculus

Contenido del libro:

Oiva Ketonen (1913-2000) fue el alumno más cercano que tuvo el creador de la teoría moderna de la demostración Gerhard Gentzen. Su encuentro tuvo lugar en 1938-1939 en Gotinga, con Ketonen esperando recibir un tema adecuado para una tesis doctoral y Gentzen, en cambio, profundamente inmerso en los intentos de demostrar la consistencia del análisis.

La tesis de Ketonen de 1944, su único trabajo en lógica, introdujo lo que hoy se denomina el cálculo secuencial G3. Se trata de su descubrimiento más conocido, un cálculo secuencial para la lógica proposicional clásica cuyas reglas lógicas son todas invertibles. Pocos leyeron su tesis, cuyos resultados se dieron a conocer a través de una larga reseña de Paul Bernays.

El cálculo de Ketonen es la base del método tableau de Evert Beth y de los cálculos secuenciales del influyente {it Introduction to Metamathematics} de Stephen Kleene. Un segundo resultado fue una agudización del teorema del secuente medio, mediante el cual se podía minimizar el número de inferencias de cuantificadores con variables propias.

A esto siguió la existencia de un subsecuente medio más débil posible, en el sentido de que si cualquier subsecuente medio es derivable, el más débil también lo es. Convirtiendo esto en un contrapositivo, Ketonen encontró un método puramente sintáctico para las pruebas de infraivabilidad que aplicó a la geometría plana afín.

Su resultado, en términos modernos, fue una solución positiva al problema de la palabra para el fragmento universal de la geometría afín plana, con una prueba sintáctica de la infraivabilidad del postulado paralelo a partir del resto de los axiomas afines como corolario.