LA TESIS Y EL TEOREMA DE CHURCH

1-INDECIDIBILIDAD DEL MÉTODO DE ÁRBOLES

Ya sabemos que el método de árboles no nos da siempre una respuesta correcta a

la pregunta por la validez de una inferencia o por la satisfacibilidad de un conjunto de

fbfs. A veces no da ninguna respuesta, por tanto, carece de la deseable propiedad de la

decidibilidad. En consecuencia, se nos plantea la cuestión de si puede haber alguna

mejora o alguna alternativa al método de árboles que siempre nos dé respuesta, y

respuesta correcta, a las preguntas sobre la validez y la satisfacibilidad de primer orden.

2-INDECIDIBILIDAD GENERAL

Toda rutina mecánica es inadecuada: no existe un procedimiento mecánico para

decidir sobre la validez o la satisfacibilidad de primer orden. De lo cual se sigue que no

puede existir una rutina mecánica para determinar si las inferencias tienen árboles

finitos o infinitos. Ante cualquier inferencia particular cuyo árbol sea infinito, tras un

número finito de pasos, puede que seamos capaces de darnos cuenta de que el árbol

nunca parará de crecer. Pero lo que no existe es un procedimiento mecánico uniforme

para hacer esto; un procedimiento que funcione para algunas inferencias, fallará para

otras.

3-EL PROBLEMA DE LA DECISIÓN

El problema de la decisión en lógica de primer orden es insoluble. Llamamos

“problema de la decisión” en lógica de primer orden a la cuestión de cómo construir una

rutina mecánica, aplicada por un ser humano o por una máquina a cualquier inferencia

de la lógica de primer orden, termine eventualmente clasificándola correctamente como

válida o inválida. Por tanto, siempre habrá lugar para el ingenio humano, e incluso para

la suerte, en la cuestión de reconocer la validez.

4-EL TEOREMA DE CHURCH

Se trata de un notable metateorema demostrado en 1936 por Alonzo Church, el

cual establece que la insolubilidad del problema de la decisión se sigue de una cierta

hipótesis acerca de la computabilidad. Esa hipótesis recibe el nombre de “Tesis de

Church”. En consecuencia, el teorema de Church es la siguiente afirmación:

“Si la tesis de Church es verdadera, el problema de la decisión en lógica de primer

orden es insoluble.

5-LA TESIS DE CHURCH

Es una hipótesis para cuya aceptación existen muy buenas razones, pero que no es

susceptible de demostración matemática. Para explicarlo presentamos n tipo de máquina

de computación muy simple perno notablemente potente: las llamadas máquinas de

registros o ábacos. Son máquinas que pueden programarse para que realicen cálculos

matemáticos, como sumas, multiplicaciones, y muchos otros más complicados. Pues

bien, la Tesis de Church dice que si una función es computable, es computable por un

programa de ábacos.

6-COMPUTABILIDAD Y MÁQUINAS

Ser computable significa que exista un algoritmo, un procedimiento mecánico, una

máquina que lo resuelva en un número finito de pasos. Pero el concepto de máquina es

ambiguo, pues no hay límites claros a la variedad de formas que podría adoptar una

rutina mecánica. Prescindimos aquí de limitaciones físicas, que pudieran ser superadas

con los años; supondremos que contamos con máquinas ideales, con tanta memoria y

tanta velocidad de proceso como pudiera ser necesaria (aunque siempre finita).

7-POTENCIA DE LAS MÁQUINAS DE REGISTROS

Las máquinas de registros que vamos a considerar son capaces de realizar notables

hazañas computacionales. Aunque representan sólo un tipo muy especial de rutinas

mecánicas para computar funciones, todos los indicios señalan que cualquier otro tipo

de rutina mecánica puede transcribirse en términos de ábacos. Al menos así ha ocurrido

con todos los casos en que de hecho se ha intentado; las rutinas escritas en diferentes

lenguajes de programación que funcionan en computadores comerciales, se pueden

reescribir y desarrollarse en ábacos, obteniendo el mismo efecto.

8-DISTINTAS MÁQUINAS IDEALES

Está matemáticamente demostrado que las máquinas de registros pueden computat

exactamente las mismas funciones que otras máquinas ideales que han sido propuestas,

como por ejemplo:

• Máquinas de Türing

• Algoritmos de Markov

• Cálculo landa de funciones recursivas

La tesis de Church puede formularse igualmente para cualquiera de ellas: Si una

función es computable, lo es por máquinas de Türing, o por algoritmos de Markov o por

el cálculo landa.

9-LA TESIS DE CHURCH NO ES DEMOSTRABLE

No es posible dar una definición general y precisa de lo que es una rutina

mecánica. En contraste, la noción de programar ábacos es muy clara, y puede ser

definida con completa precisión. Otro tanto cabe decir de cualquier otro tipo particular

de rutina mecánica. Es la noción de rutina mecánica en general la que es imposible de

definir con precisión. La equivalencia entre una cosa y otra es, por tanto, una hipótesis

no susceptible de demostración.

10-LA TESIS DE CHURCH ES REFUTABLE

Aunque no puede ser demostrada, la tesis de Church si que puede ser refutada si es

falsa. Si fuera falsa, existiría alguna rutina mecánica que podríamos especificar con total

precisión, la cual nos permitiría computar un cierto tipo de función que no pudiera

computar ningún ábaco. Puesto que lo que es un programa de ábacos es definible con

precisión, se podría demostrar que ningún programa tal es capaz de computar dicha

función.

11-LA TESIS NO TIENE RIVAL

La tesis de Church permanece hasta la fecha sin refutar. La confianza en esa tesis

se basa en el hecho de que la perversa intuición humana no ha sido capaz de inventar

una rutina mecánica que sea imposible transcribir en términos de ábacos. Puede, pues,

que la tesis de Church sea falsa, pero tal posibilidad para hoy enormemente vaga y

especulativa. Por el momento, esa tesis constituye nuestra única hipótesis de trabajo, y

por tanto, al no tener ningún competidor, demanda credibilidad. Pese a todo, siempre es

posible que, como sucedió con la mecánica newtoniana, esté destinada a ser sustituida

por una explicación más profunda. Pero por el momento no tenemos ni las más remota

noción acerca de las características que habría de tener esa nueva y más profunda

explicación.

12-ESTRATEGIA PARA PROBAR EL TEOREMA DE CHURCH

1. Definiremos las capacidades de las máquinas de registros, de forma que la

tesis de Church se haga inteligible y plausible.

2. Definiremos una función particular h y demostraremos que ningún

programa de ábacos puede computarla.

3. Mostraremos como la función h sería computable si existiese un

procedimiento de decisión para la validez de primer orden.

Como consecuencia de todo ello, y si las máquinas de registros son tan potentes como la

tesis de Church dice que son, entonces el problema de la decisión en lógica de primer

orden es insoluble.

MAQUINAS DE REGISTROS O ÁBACOS

1-REGISTROS Y CONTADORES

Una máquina de registros o ábaco se compone de un número finito de registros,

cada uno de los cuales puede contener un número finito de objetos llamados contadores.

En cada momento un registro puede contener una determinada cantidad de contadores.

Hablaremos del número que hay en el registro en un determinado momento,

entendiendo por ello simplemente el número de contadores que hay en él en ese

momento.

2-PROGRAMAS DE ÁBACOS

Un programa para un ábaco es un conjunto de instrucciones que indican cómo

poner contadores uno por uno en los registros y cómo quitar contadores uno por uno de

los registros. Hay sólo tres tipos de instrucciones en los programas de ábacos:

• Ir a un registro y añadir un contador

• Ir a un registro y quitar un contador

-Puede que esto sea posible, porque haya contadores en el registro

-Puede que no sea posible, porque el registro esté vacío

EL TEOREMA DE CORRECCIÓN

1-EL METATEOREMA DE CORRECCIÓN

Vamos a demostrar la corrección del método de árboles para la lógica de primer

orden: que siempre que se clasifica una inferencia como válida (o un conjunto de fbfs

como insatisfacible), al obtenerse un árbol cerrado, esa clasificación es semánticamente

correcta. Lo que hay que demostrar es que si todas las ramas de un árbol están cerradas,

entonces la lista inicial de fbfs es insatisfacible, o lo que viene a ser lo mismo: si la lista

de fbfs iniciales es satisfacible, habrá una rama abierta (finita o infinita) en cualquier

árbol que pueda obtenerse de ella.

2-EL LEMA DE LA CORRECCIÓN

Para demostrar el teorema enunciado basta probar que si la lista inicial es

satisfacible, también lo será alguna rama entera de cualquier árbol que puede obtenerse

a partir de esa lista (una rama satisfacible no puede estar cerrada). Para probarlo bastará

con el lema de corrección: siempre que se aplica una regla de inferencia a una fbf o a un

par de fbfs de una rama satisfacible, habrá al menos una lista de conclusiones que,

añadidas a esa rama, formarán una rama más larga y también satisfacible.

3-LA PRUEBA DEL LEMA

Para probar el lema (y con ello el teorema de corrección) basta verificar que

cuando las fbfs de una rama son verdaderas para una interpretación I con un dominio D,

y se aplica una regla, al menos una de las listas de conclusiones, añadida a la rama,

forma una nueva rama cuyas líneas son todas verdaderas para I.