Relación entre demostraciones lógicas y programas: Isomorfismo Curry-Howard

UNIVERSIDAD CENTRAL DE VENEZUELA FACULTAD DE HUMANIDADES Y EDUCACIÓN INSTITUTO DE FILOSOFÍA MAESTRÍA DE LÓGICA Y FILOSOFÍA DE LAS CIENCIAS

Relación entre demostraciones lógicas y programas: Isomorfismo Curry-Howard

Alumno: Numa Tortolero Tutor: Jesús Baceta

0

Contenido I. Introducción II. Principios Generales de la Lógica 1.1 Constitución de un sistema lógico 1.2 .Propiedades de un sistema lógico 1.3. Teoría de la demostración 1.4. La lógica intuicionista III. Sistemas lógicos de Gentzen 3.1. Cálculos de deducción natural: 3.1.1. Lógica clásica 3.12. Lógica intuicionista 3.2. Cálculo de secuentes 3.2.1. Lógica clásica 3.2.2. Lógica intuicionista 3.3. Normalización IV. Computabilidad y Cálculos Lambda 4.1.- Relevancia lógico – matemática de la noción de computabilidad. 4.2.- El cálculo lambda de Alonso Church y la noción de computabilidad 4.3.- Maquinas de Turing y cálculo lambda 4.4.- Reglas del cálculo lambda Convenciones para variables y términos: Reglas de formación: Convenciones de asociación: Variables libres 1

Reglas de transformación: Regla de sustitución o regla alfa ‘=α’ Regla de reducción o regla beta ≥ β Regla de expansión o abstracción beta ‘≤ β’ Conversión lambda “λ” Forma Normal en el Cálculo Lambda Caracterización de la conversión lambda Combinadores Teoremas Church – Rosser Funciones lambda-definibles Numerales de Church Constructor y selector Constantes y operaciones booleanas 4.5.- El cálculo lambda con tipos: origen y reglas. V. Correspondencia Curry-Howard 5.1. Breve historia 5.2. Presentación 5.2.1. Isomorfismo 5.2.2. Presentación informal del Isomorfismo Curry-Howard 5.2.3. Presentación formal del isomorfismo Curry-Howard 5.3. Cálculo de deducción natural con términos lambda 5.4. Extracción de programas de demostraciones lógicas: aproximación 2

5.5. Isomorfismo Curry – Howard y el significado de las constantes lógicas VI. Conclusiones y Reflexiones I II III V Apéndice: Sistemas computacionales de demostración

3

Introducción El presente trabajo trata sobre la relación entre deducción en sistemas de lógica formal y computación. Esta relación podría ser precisada a través de una correspondencia entre los componentes del sistema lógico ―fórmulas y sus deducciones― y los componentes de un cálculo que define computación ―términos y programas.

Por un lado tenemos entonces sistemas lógicos, los cuales incluyen mecanismos para construir y derivar fórmulas nuevas a partir de otras. Al proceso que da lugar a tal derivación se le llama deducción. De las fórmulas obtenidas por deducción, que han sido obtenidas a partir de otras por la aplicación de reglas de deducción del sistema, decimos que están en relación de deducción con aquellas a partir de las cuales se obtuvieron. A las fórmulas obtenidas por deducción se les denomina teoremas. En general, las reglas de deducción de un sistema lógico deben permitir decidir si una fórmula es un teorema del sistema. El proceso de deducción constituye una demostración de que la formula obtenida es un teorema del sistema. En este sentido, podemos entender la deducción como una relación que se establece entre las fórmulas que se encuentran en la demostración de un teorema. Vista desde el punto de vista del álgebra, una lógica puede ser definida como un sistema, constituido por un conjunto de fórmulas cerrado bajo la relación de deducción que, como toda relación de un sistema algebraico, está caracterizada por una serie de propiedades.

Por otro lado tenemos sistemas formales de cómputo, pensados para caracterizar la noción de computación. Este concepto, computación, muy en boga por el creciente desarrollo de la industria informática y la robótica, comenzó a precisarse a mediados de la década de 1930, 4

como parte de la investigación acerca del problema de la decisión: ¿hay un método o procedimiento mecánico por el cual es posible decidir si cualquier problema matemático tiene solución? Para responder a esta cuestión, se intentaron aproximaciones diferentes a la definición de la noción de procedimiento efectivo, las cuales demostraron ser equivalentes en su capacidad para expresar computación, entendiendo informalmente esto como proceso mecánico de construcción o de definición de funciones —cierta correspondencia que proyecta objetos de un dominio, los argumentos, a otros objetos de otro o el mismo dominio— que pueden ejecutar de forma automatizada soluciones a problemas. Un proceso de cómputo o de cálculo de los valores de una función para ciertos valores de sus argumentos puede ser representado a través de una secuencia discreta de enunciados o términos y esta secuencia puede llamarse programa.

Partiendo de esta definición informal de computación y acercándonos al concepto de sistema lógico, podemos preguntarnos si las demostraciones en estos sistemas, vistas como procesos de deducción, tienen algún contenido computacional, en el sentido de que puedieran realizarse de forma automatizada, y que ese contenido pudiera ser aislado de forma precisa.

Una demostración supone el inicio de un proceso cognitivo que, para expresarlo en términos coloquiales, “pone la mente en movimiento”. Supongamos que, por ejemplo, se quiere demostrar algún teorema matemático o se desea comprender si un hecho es el caso: se inicia una actividad mental donde tiene lugar una serie de cogitaciones reguladas por principios implícitos de acuerdo a los cuales debería poder decidirse si una proposición es un teorema o si un hecho es el caso. El resultado de un proceso tal constituye una 5

verificación: la proposición es un teorema o el hecho es el caso, o una refutación la proposición no es un teorema o el hecho no es el caso. Si describimos el proceso de demostración a través de derivaciones en algún sistema lógico, obtendremos un reflejo sintáctico de procesos mentales. Entender esta diferencia entre el acto mental orientado por una finalidad verificadora y la derivación que lo describe a través de un lenguaje formal, es un rasgo que caracteriza el punto de vista sostenido por lógicos y matemáticos de la tendencia en filosofía de las ciencias formales conocida como intuicionismo. Esta consideración de los actos mentales, junto al principio de que sólo a través de estos actos pueden alcanzar existencia los objetos formales, ha llevado a los intuicionistas a hablar del carácter constructivo al razonamiento lógico y a las entidades matemáticas.

El presente trabajo investiga la posible identidad estructural entre los sistemas de deducción natural y los cálculos que definen algorítmicamente la noción de computabilidad. Se ha comprobado que tal identidad existe entre el cálculo de deducción natural para la lógica proposicional intuicionista y el cálculo lambda con asignación de tipos, que es un sistema en el cual es posible definir funciones computables estructural se le conoce como isomorfismo Curry – Howard. Esta investigación no sólo es ocasión para una presentación organizada de una serie de conceptos y nociones elementales relativos a la lógica y al propio concepto de computación, también plantea hechos que, por el lado de la lógica, abren nuevas perspectivas en el estudio teórico de la demostración y, por el lado de la computación práctica, brinda los fundamentos para el desarrollo de programas bajo una disciplina estricta de corrección.

El trabajo se divide en cuatro capítulos, el último de los cuales, el más breve, es 6

simplemente una reunión de conclusiones y reflexiones a propósito de los hechos puestos en evidencia en los tres primeros capítulos.

Comenzaremos, en el primer capítulo, tratando de entender en qué consiste un sistema lógico, lo cual nos dará un marco teórico adecuado para presentar los sistemas deducción natural para la lógica intuicionista proposicional. Esta presentación implica mostrar las propiedades de estos sistemas, en especial la llamada normalización, esencial para cumplir nuestro objetivo.

Luego, en el segundo capítulo, procederemos a indagar en la noción de computabilidad, tal como es expresada por los cálculos lambda. Primero haremos una presentación general e informal de la noción de computabilidad y de su relevancia en la investigación del problema de la decisión. Veremos cómo el cálculo lambda fue empleado a este respecto. Finalmente haremos una presentación formal del cálculo lambda puro y del cálculo lambda simple con tipos. Veremos en la presentación de este último sistema, como comienzan a hacerse evidentes sus relaciones, a nivel de su estructura formal, con el fragmento condicional positivo de la lógica proposicional.

En el tercer capítulo, mostraremos que es posible definir un isomorfismo o equivalencia estructural entre el cálculo proposicional de deducción natural intuicionista y el cálculo lambda con tipos. Este isomorfismo es conocido como correspondencia Curry – Howard o principio de fórmulas-como-tipos. El isomorfismo permite aislar con precisión el componente computacional o constructivo de las demostraciones lógicas. Como ya hemos asomado, esto tiene varias ventajas, algunas de tipo práctico, como la posibilidad de extraer 7

programas que computen soluciones de problemas a partir de la demostración lógica del enunciado que especifica el problema a resolver; desde el punto de vista teórico, el isomorfismo permite formalizar la noción de evidencia en sistemas formales constructivos y nos da elementos para justificar una presentación semántica del significado de las conectivas lógicas a través de reglas de inferencia. Otra ventaja teórica del isomorfismo es la posibilidad de trasladar teorías y demostraciones metateóricas válidas para un sistema de la lógica intuicionista a sistemas del cálculo lambda y viceversa. Por ejemplo, la teoría de la identidad entre términos del cálculo lambda, basada en la noción de reducción que define el proceso de normalización en el cálculo lambda, puede ser trasladada al fragmento condicional positivo del cálculo natural proposicional intuicionista. Esto nos da, al tener ambos sistemas idéntica estructura formal, que los corolarios que se siguen del teorema de la forma normal para el cálculo lambda, también se deben cumplir en el cálculo lógico.

8

I. Cálculos de deducción natural El objetivo del trabajo es mostrar la correspondencia entre el cálculo de deducción natural intuicionista y el cálculo lambda con tipos, conocida como isomorfismo Curry-Howard. En el presente capítulo vamos a hacer una presentación de los sistemas de deducción natural que nos servirá de base para cumplir nuestra tarea. Comenzaremos exponiendo cómo se constituye un sistema lógico, cuáles son las propiedades más importantes que debe satisfacer y en qué marco teórico se realiza el estudio de estas propiedades. Como ejemplos de sistemas lógicos damos primero una presentación axiomática para la lógica clásica y luego una, también axiomática, para la lógica intuicionista. Estas primeras exposiciones darán el entorno teórico propicio para presentar los cálculos lógicos de Gerhard Gentzen: el cálculo de deducción natural y el cálculo de secuentes, tanto para lógica clásica y la lógica intuicionista. Incluimos una exposición del cálculo de secuentes por estar este cálculo estrechamente vinculado al cálculo de deducción natural, como se verá especialmente en la última parte de este capítulo, donde presentaremos la noción de normalización para estos cálculos. Los cálculos de Gentzen se caracterizan por ofrecer una presentación formal de las reglas de derivación que facilita el razonamiento sobre las propiedades del sistema y su subsiguiente comparación con otros. En especial, la aproximación a los sistemas lógicos de deducción natural y la presentación de la noción de normalización es estos sistemas, ha de facilitarnos su comparación con el cálculo lambda con tipos, un sistema pensado para definir formalmente la noción de computabilidad. En esta comparación se determina la existencia de algún tipo de relación o morfismo entre el cálculo natural y el cálculo lambda con tipos.

9

1.1 Constitución de un sistema lógico En virtud de su carácter simbólico y formal, toda lógica Lincluye un lenguaje formal L, es decir, un vocabulario y una sintaxis. El vocabulario consta de un conjunto no vacío de símbolos que pueden combinarse para formar expresiones complejas. Las combinaciones permitidas en el lenguaje L, las fórmulas de este lenguaje, están determinadas por un conjunto de reglas: las reglas de formación de L. Un vocabulario y un conjunto de reglas de formación constituyen un lenguaje formal. Para que este lenguaje formal sea una lógica todavía es necesario agregar un conjunto de reglas de transformación o de inferencia, a través de las cuales podemos establecer cómo una fórmula puede inferirse a partir de otras, y una especificación del significado de las expresiones bien formadas. Las reglas de formación y de transformación del sistema constituyen la sintaxis del lenguaje L, la cual define cuáles son las expresiones gramaticalmente correctas del sistema y cómo derivar unas de otras, de manera tal que las derivadas siempre conserven ciertas propiedades que poseen aquellas de las cuales derivan. Además de la sintaxis, habría que establecer una semántica que asigne significado a las expresiones correctas y establezca cuáles propiedades deben conservar las fórmulas involucradas en una derivación o inferencia.

De acuerdo a Palau (2002) El vocabulario de un sistema lógico consta de (pag. 24): a) un conjunto de símbolos descriptivos o categoremáticos, que no son estrictamente lógicos, como letras para representar variables y constantes. Un conjunto de símbolos lógicos o sincategoremáticos, que representan constantes o conectivas lógicas1. 1

Corti (2002, pags. 10 – 11) explica que los símbolos categoremáticos son los que tienen de significación extralingüística. Los símbolos sincategoremáticos carecen significación extralingüística, sólo adquieren significación modificando a un símbolo categoremático. (Quine, 1977, pag. 59) aclara que la distinción entre términos categoremáticos y términos sincategoremáticos se atribuye a la filosofía escolástica, pero procede de la Antigüedad: se relaciona con las proposiciones categóricas del silogismo, pues se llaman categoremas a los términos de una proposición categórica. Una proposición categórica relaciona dos clases

10

b) Signos de puntuación o auxiliares, como paréntesis.

Formulemos ahora un lenguaje formal. El vocabulario para este lenguaje constará de: i)

El conjunto de símbolos descriptivos o categoremáticos está formado por letras mayúsculas A, B, …, Z.

ii)

 Los símbolos lógicos o sincategoremáticos son: ¬, \/, /\, →, ↔.

iii)

Los símbolos auxiliares son ( , ).

La sintaxis de un lenguaje consta de reglas de carácter combinatorio y constructivo: nos dicen cómo combinar o construir las expresiones del lenguaje usando los símbolos del vocabulario. Como mencionamos arriba, las reglas que conforman la sintaxis de un sistema lógico se pueden subdividir en dos grupos: reglas de formación, que nos permiten decidir si una fórmula está bien construida o bien formada, y reglas de transformación, que nos permiten transformar una fórmula en otra y decidir si la transformación es válida. Para nuestro sistema, podemos establecer las siguientes reglas de formación: i)

A, B, … , Z son variables del sistema que representan fórmulas no especificadas.

ii)

Si A y B son variables, entonces las siguientes construcciones son fórmulas del lenguaje L: i)

¬A

ii)  A \/ B iii)  A /\ B iv)  A → B v) A ↔ B. o categorías, cada una de las cuáles es designada por un término denominado término categórico.

11

iii)

Las construcciones (a) – (e) y las que resultan de combinar ellas para formar otras más complejas, son las formas bien formadas (fbf) del sistema.

Como A, B, …, Z representan fórmulas no especificadas, puede emplearse una de ellas para representar una fórmula bien formada. Quiere decir que, por ejemplo, podemos usar la letra C para representar una expresión como ‘A → B’ o ‘¬A’.

Como es usual, hemos usado las comillas simples - ' - para formar el nombre de una palabra u otra expresión. La expresión formada por las comillas simples designa la expresión que encierra la comilla. De aquí en adelante, a los fines de abreviar la notación, convenimos en usar las constantes lógicas y los símbolos auxiliares como nombres de sí mismos. En lo que sigue, utilizaremos A, B, C, etc. como metavariables que representan cualquier fórm,ula bien formada (f.b.f). Una expresión como '(A \/ B)' no debe entenderse como una mezcla de lenguaje objeto y metalenguaje; es una expresión propia del metalenguaje porque hemos convenido que los corchetes y las conectivas son nombres de sí mismos.

Para nuestro sistema, utilizamos una única regla de transformación, el modus ponens (MP): Si A → B y A, entonces B. Esta regla se corresponde con la idea intuitiva de que si sabemos que cuando A es el caso, B no puede no serlo, y si A es el caso, podemos concluir también que B lo es. Los sistemas de lógica formal elaborados entre finales del siglo XIX y principios del siglo XX son sistemas axiomáticos. Entre estos sistemas tenemos el de la Conceptografía de Frege (1879), el de los Principia Mathematica de Russell y Whitehead (1910) y el de Los Fundamentos de las Matemática de Hilbert (1928). En éstos, el proceso de deducción que 12

se realiza, el conjunto de fórmulas que los constituyen se dividen en axiomas y teoremas. Los axiomas son fórmulas dadas que no se infieren de otras, pero permiten inferir otros enunciados: los teoremas. Entonces, los teoremas serían fórmulas inferidas de los axiomas o de otros teoremas, aplicando reglas de inferencia. Se podría decir que un sistema axiomático está constituido por axiomas y teoremas.

Los axiomas del sistema pueden ser dados a través de esquemas como los siguientes: H1

A → (B → A)

Introducción de una suposición

H2

(A → (B → C)) → ((A →B) → (A → C))

Distribución

H3

(A /\ B) → A)

Simplificación (a)

H4

(A /\ B) → B)

Simplificación (b)

H5

(C → A) → ((C → B) →(C → (A /\ B)))

Producción

H6

A → (A \/ B)

Adición (a)

H7

B → (A \/ B)

Adición (b)

H8

((A → C) → (B → C)) → ((A \/ B) → C)

Prueba por casos

H9

(A → ¬B ) → (B → ¬A)

Contraposición

H10

¬(A → A) → B

H11

¬¬A → A

Doble negación

Hemos enumerado esta lista de esquemas usando el símbolo Hn, donde n es un número natural, porque este conjunto de esquemas es tomado de la obra de Hilbert y Bernays (1934), Fundamentos de la Aritmética, según Palau (2002, pags, 28 – 29). Las expresiones de esta lista no deben considerarse como enunciados saturados con un contenido específico: se trata de formas o esquemas, expresiones sin significado, donde las letras ‘A, 13

B, … , Z’ tienen como objeto representar fórmulas bien formadas del sistema o hasta expresiones con significado definido pertenecientes a otros sistemas o lenguajes [Kleene, 81]. El estatus de estos esquemas se aclarará cuando presentemos un ejemplo y se precisará más cuando hablemos del metalenguaje, en el apartado que le dedicamos a las propiedades de los sistemas lógicos y el metalenguaje.

Los esquemas de axiomas H1 – H2 caracterizan el condicional. El axioma H1 al permitir pasar de la afirmación de A a la afirmación de B → A, afirma la posibilidad de introducir suposiciones. El axioma H2, que distribuye un antecedente sobre dos consecuentes, lo hemos llamado principio de distribución.

H3 – H5 caracterizan la conjunción. Los axiomas H3 y H4 nos dicen intuitivamente que si conozco A y B, entonces puedo concluir que A o puedo también concluir que B. Permiten “eliminar” el cojuntor /\ y se les conoce como axiomas de simplificación o de eliminación de /\. El axioma H5 permite introducir el cojuntor /\, y se le conoce como axioma de producción.

H6 – H8 caracterizan la disyunción. H6 y H7 se permiten introducir el disyuntor \/ y se conocen como axiomas de adición. El axioma H8 se conoce como prueba por casos y manifiesta la idea intuitiva de que si de una fórmula A deduzco una fórmula C y de una fórmula B también deduzco la misma fórmula C, entonces puedo concluir que puedo deducir C de A o de B.

H9 – H11 caracterizan la negación. Al axioma H9 lo hemos llamado contraposición: 14

caracteriza la idea intuitiva de que si el conocimiento de A deduzco lo suficiente para saber que B no es el caso, entonces puedo afirmar que en un hecho donde B es el caso, A no puede serlo: los hechos A y B se contraponen. El axioma H11 es una forma semejante de la reducción al absurdo: intuitivamente, si no puedo aceptar que A es el caso sabiendo que A es el caso, entonces puedo deducir otra cosa, que puede ser B. H11, que elimina la negación, se conoce como axioma de la doble negación.

Los teoremas derivados de H1 – H2 constituyen el fragmento condicional de la lógica proposicional clásica; los derivados de H1 – H8 el fragmento positivo; y los derivados de H1 – H11 el conjunto de la lógica proposicional clásica.

Un teorema es una fórmula D que puede ser demostrada en un sistema. Según Kleene (1974, pag. 83) un teorema o fórmula demostrable se define inductivamente: 1. Si D es un axioma, es también un teorema 2. Si E es un teorema y D es inferido directamente de E, entonces D es un teorema. 3. Si E y F son teoremas y D es inferido directamente de E y F, entonces D es un teorema 4. Sólo son teoremas las fórmulas que cumplen con las condiciones 1 – 3. Una derivación de un teorema es una lista numerada de fórmulas donde cada una es un axioma o una fórmula inferida directamente de fórmulas precedentes de la lista. Como un ejemplo, demostremos un teorema de nuestro sistema. Derivaremos (A → A):

15

1. A → ((A → A) → A)

H1 con (A → A) por B

2. A → ((A → A) → A) → ((A → (A → A)) → (A → A))

H2

3. (A → (A → A)) → (A → A)

MP 1 y 2

4. A → (A → A)

H1 con A por A

5. (A → A)

MP 3 y 4

Hemos derivado en nuestro sistema el enunciado (A → A), el cual podemos considerar ahora un teorema de nuestro sistema. Se trata de una derivación que no depende para nada de lo que puedan significar la letra A, pues recuérdese que estas expresiones son esquemas formales sin contenido. Vemos que en esta derivación sólo hemos usado procedimientos sintácticos. Confirmamos que la sintaxis no nos dice nada de los significados de las fórmulas del sistema, así que no sabemos todavía si las fórmulas de tal sistema son verdaderas o falsas, pues no sabemos a qué se refieren. A un sistema de este tipo, que sólo posee un vocabulario y una sintaxis, lo llamamos cálculo. Un cálculo no es sino un sistema de relaciones entre signos donde lo importante no es su contenido sino su forma, “el conjunto de relaciones sintácticas que vincula entre sí a dichos signos independientemente de lo que designen” (Corti y Gianneschim 2002, pag. 24).

Como plantea Cuena (1985, pag. 83), la asignación de significados a las expresiones y símbolos de un sistema lógico se hace a través de una semántica, que establece una simbolización del significado de las proposiciones del sistema y, en consecuencia, una forma de valorar el contenido informativo de cada proposición. Para ello, primero especificamos a qué refieren los símbolos no lógicos o descriptivos del sistema. Necesitaremos luego una definición semántica de las conectivas para especificar cómo 16

atribuir significado a las proposiciones compuestas con

distintos tipos de conectivas

partiendo de los significados de sus componentes proposicionales. Finalmente, debemos dar una definición semántica de deducción correcta.

Para asignar significado a los símbolos no lógicos del sistema construimos una interpretación I, hacemos lo siguiente: 1. Elegimos un conjunto no vacío de entidades extra lógicas, que llamamos el dominio D de la interpretación. 2. Definimos una función que asocia o asigna un elemento del dominio D a cada signo descriptivo del sistema.

Por ejemplo, para nuestro sistema elegimos como dominio D de la interpretación I al conjunto formado por los valores de verdad: Verdad (representado por 1) y Falsedad (representado por 0). Así que: D = {1, 0}.

La definición semántica de las conectivas puede hacerse mediante las llamadas tablas de verdad o especificando las condiciones en que cada oración del lenguaje, que incluya conectivas lógicas, es verdad. Aquí usaremos la última opción: para especificar las condiciones de verdad para cada oración del lenguaje L, definimos una función de valoración V, que asigna un valor de verdad a cada fórmula de acuerdo a la valoración de sus componentes y según cierta condición: 1.

V (¬A) = 1 si y sólo si V(A) = 0 V (¬A) = 0 si y sólo si V(A) = 1

2.

V(A \/ B) = 1 si y sólo si V(A) = 1 y V(B) = 1 17

3.

V(A /\ B) = 1 si y sólo si V(A) = 1 o V(B) = 1

4.

V(A → B) = 0 si y sólo si V(A) = 1 y V(B) = 0

5.

V(A ↔ B) = 1 si y sólo si V(A) = 1 = V(B) = 1

Esta manera de dar significado a las conectivas, donde especificamos las condiciones de verdad en las que ellas aparecen, supone que el valor veritativo de las fórmulas en las que aparecen las conectivas lógicas depende del valor de verdad de sus componentes. Cuando el significado de las conectivas es determinado de esta forma, de manera que los valores de verdad de proposiciones compuestas dependen de los valores de verdad de sus constituyentes, decimos que son extensionales, de acuerdo a Ebbinghaus, Flum y Thomas (1996, pag. 31) o veritativos funcionales (funciones de verdad), según Palau (2002, pag. 27)2.

Nos queda ahora la caracterización semántica de la deducción lógica, es decir, dar una definición semántica de deducción correcta. La noción que hace esta caracterización la podemos llamar derivación semántica o consecuencia lógica. Para definirla comenzamos definiendo la noción de validez semántica, la cual puede ser relativa o absoluta. Una fórmula de un sistema es válida, en un sentido relativo, si es verdadera respecto a una interpretación. Si una fórmula de un sistema es verdad bajo cualquier interpretación, decimos que es una verdad universalmente o absolutamente válida o, también, una tautología o verdad lógica.

2

Generalmente, explica Ebbinghaus (1996, pag. 31), en el habla coloquial, las conectivas no son usadas extensionalmente. Por ejemplo, la verdad del enunciado ”José enfermó y el doctor le dio una prescripción” es valorada de una forma distinta al enunciado “El doctor le dio una prescripción a José y enfermó”. A diferencia del caso extensional, estos enunciados compuestos dependen de la relación temporal expresada por el orden de los dos componentes de cada enunciado. En este último caso estamos haciendo un uso intencional. de la conectiva.

18

Definida la noción de validez semántica, podemos definir consecuencia lógica o derivación semántica: dado un conjunto de fórmulas Γ, decimos que una fórmula A es consecuencia lógica de Γ sí y sólo si la fórmula A es verdadera en todas las interpretaciones donde son verdaderas las fórmulas del conjunto Γ. Como plantea Cuena (1985, pags. 87 – 88), la idea intuitiva de la consecuencia lógica es que una fórmula es consecuencia de otras si siempre que éstas son verdaderas lo es también aquella. ¿En qué sentido esta definición de consecuencia lógica caracteriza semánticamente la noción de deducción?

Aunque la sintaxis y la semántica de un sistema lógico refieran a diferentes aspectos, la sintaxis de un sistema lógico sería inútil si las fórmulas que derivamos a partir de nuestros axiomas y teoremas no fueran verdaderas respecto del mismo dominio de objetos extra lógicos de los que son verdaderos los mismos axiomas y fórmulas dadas. El sistema lógico no tendría utilidad si fuera deducible en él un teorema que no fuera verdadero en una interpretación donde sí son verdaderos los axiomas y teoremas a partir de los cuales fue derivado: el sistema no sería correcto. Por eso, en un sistema lógico las reglas de inferencia y los axiomas deben garantizar que su aplicación o uso en una deducción conserve la verdad de las fórmulas involucradas, como si el objetivo de las reglas de inferencia fuera transmitir la verdad de los axiomas a los enunciados que derivan de ellos por la aplicación de las reglas de inferencia. La sintaxis y la semántica de un sistema lógico pueden estar estrechamente relacionadas: todo teorema deducido siguiendo las reglas de inferencia no debería ser falso en ninguna de las interpretaciones donde los axiomas y otros teoremas del sistema, de los cuales deriva, son verdaderos. Lo deseable es que las tautologías de un sistema lógico sean deducibles en el sistema.

19

¿Cómo podemos caracterizar formalmente la relación entre sintaxis y semántica en un sistema lógico?

1.2 .Propiedades de un sistema lógico La relación entre sintaxis y semántica en un sistema lógico es un aspecto del sistema cuyo estudio trasciende los límites del sistema. Si, por un lado, un sistema lógico formalizado permite formar expresiones y concatenarlas de acuerdo a reglas precisas, por otro lado, el propio sistema puede ser considerado como un objeto cuyas propiedades pueden ser estudiadas. En esta última consideración, es necesario usar otro lenguaje que proporcione los términos para designar los elementos del sistema. Esta circunstancia ha conducido, como señala Ladrière (pag. 63), a la distinción entre lenguaje-objeto, que constituye el lenguaje formal cuyas propiedades han de ser estudiadas, y metalenguaje, constituido por las expresiones que describen o designan elementos y propiedades del lenguaje objeto. Como explica Russell (1921) en su introducción al Tractatus de Wittgenstein: “…todo lenguaje tiene una estructura de la cual nada puede decirse en el lenguaje, pero puede haber otro lenguaje que trate de la estructura del primer lenguaje y que tenga una nueva estructura y esta jerarquía de lenguaje no tiene límites” (pag. 28).

La forma más inmediata de proceder toma el lenguaje cotidiano como metalenguaje, añadiéndole algunos símbolos para designar elementos del sistema objeto. Este metalenguaje puede ser objeto de formalización, para obtener en él deducciones correspondientes a los razonamientos que en él se realizan. Por ejemplo, para designar la deducción (sintáctica) de una fórmula suele usarse el símbolo ├. Así que si en un cálculo lógico se puede deducir una fórmula A escribiremos ├ A; para designar que una fórmula A 20

es formalmente deducible a partir de un conjunto de fórmulas Γ, escribiremos Γ ├ A. La expresión ├A, que es la deducción de una fórmula a partir de un conjunto vacío de fórmulas, designa entonces un teorema o un axioma. Hemos usado además variables metalingüísticas: la letra griega mayúscula Γ como variable para designar un conjunto de fórmulas, y la letra mayúscula Apara designar una alguna fórmula particular.

Por ejemplo, la deducción que realizamos de A → A a partir de nuestros esquemas axiomáticos y de nuestra regla de inferencia, la podemos designar como ├ A → A, que significa A → A es un teorema de nuestro sistema L.

Otro ejemplo sería la derivación de una fórmula C a partir de un conjunto Γ conformado por tres fórmulas: A → (B → C), B y A: 1. B

segunda fórmula en Γ

2. A

tercera fórmula en Γ

3. A → (B → C)

primera fórmula en Γ

4. B → C

MP, 2 y 3

5. C

MP, 1 y 4

Este esquema deductivo podemos designarlo en el metalenguaje con la expresión que llamaremos esquema D: A → (B → C), B, A ├ C

(D)

Nótese, como observa Kleene (1974, pag. 87), que aquí las fórmulas en Γno son esquemas axiomáticos de nuestro sistema. Aparecen como fórmulas supuestas arbitrarias, coyunturalmente equiparables a los axiomas.

21

Para designar la derivabilidad semántica o, como la hemos llamado, consecuencia lógica, se suele usar el símbolo ╞. Si una fórmula A es una tautología en un sistema escribiremos ╞ A, lo cual dice que A es absolutamente válida o verdadera en todas las interpretaciones del sistema. Escribiremos Γ ╞ Apara significar que A es válida en todas las interpretaciones donde las fórmulas del conjunto Γ son válidas.

El esquema D, cuya derivación hemos presentado, constituye una expresión del metalenguaje que refiere a la deducibilidad de una fórmula A a partir de un conjunto Γ de fórmulas supuestas en el sistema lógico L. A los enunciados demostrados en el nivel del metalenguaje se les denomina metateoremas, por ser teoremas pertenecientes a un metalenguaje que hacen referencia a las propiedades de un lenguaje objeto. Los metateoremas ofrecen caracterizaciones globales válidas para clases enteras de proposiciones o incluso la totalidad de un sistema.

Según Ladrière (1969, pag. 67), los metateoremas pueden ser de diverso tipo: reglas derivadas, caracterizaciones de clases de teoremas de un sistema, de las propiedades globales de un sistema tomado en conjunto o de las relaciones de un sistema con otros.

Las reglas derivadas son metateoremas relativos a la existencia de demostraciones formales, tales que sus pruebas indican métodos para obtener demostraciones formales. Su uso permite abreviar la presentación de pruebas formales sin incrementar la clase de fórmulas demostrables. El llamado teorema deductivo (TD) es un ejemplo de este tipo de metateoremas. Kleene (1974, pag. 89) lo formula de la siguiente manera: Si Γ, A ├ B, entonces Γ├ A → B 22

Según este teorema podemos deducir A →

C del esquema deductivo D que hemos

representado en nuestro lenguaje como A → (B → C), B, A ├ C: 1. A → (B → C), B, A ├ C

Esquema D

2. A → (B → C), B ├ A → C

TD, 1

Demostramos de esta manera que si de las fórmulas supuestas A → (B → C), B y A podemos deducir C, entonces de las fórmulas supuestas A → (B → C) y B podemos deducir A → C.

Sin el uso del teorema deductivo nuestra demostración de A → C a partir de A → (B → C) y B sería: 1. B

Segunda fórmula supuesta

2. B → (A → B)

H1

3. A → B

MP, 1 y 2

4. A → (B → C)

Primera fórmula supuesta

5. (A → (B → C)) → ((A →B) → (A → C))

H2

6. (A → B) → (A → C)

MP , 4 y 5

7. A → C

MP, 3 y 6

El teorema de la deducción, demostrado primeramente por Herbrand (1930), además de permitir abreviar deducciones, establece precisamente, como observa Cuena (1985, pag. 26), que un esquema deductivo correcto puede ser también una regla de demostración solamente asumiendo que las premisas son válidas.

La idea que está detrás de los metateoremas como expresión de las propiedades generales o 23

globales de un sistema, tomado en conjunto, es que la afirmación de que un sistema tiene cierta propiedad constituye una proposición metalinguística o metateórica susceptible de ser demostrada en el metalenguaje. En este sentido, las propiedades de un sistema lógico quedan caracterizadas por metateoremas que informan sobre la potencia, límites, funcionalidad, uso, etc., del sistema.

Según Ladrière (1969, pag. 67), las propiedades de conjunto de los sistemas formales, las cuales quedan caracterizadas por metateoremas, las más importantes son coherencia, saturación, resolubilidad, categoricidad. Las definiciones que vamos a dar aquí de estas propiedades, sigue la exposición de Ladrière (1969, pags. 67 – 70), donde cada una de estas propiedades puede referir a la sintaxis o a la semántica del sistema. Tenemos entonces por lo menos dos variantes para cada una de las propiedades mencionadas. Por ejemplo, tenemos la definición de coherencia sintáctica por un lado y la definición de consistencia semántica, por otro lado. En el caso de la coherencia sintáctica podemos dar incluso dos definiciones: 1. Un sistema es sintácticamente coherente cuando toda proposición del sistema no puede ser derivada en él. 2. Un sistema es sintácticamente coherente cuando no es posible derivar en él a la vez una proposición y su negación. La consistencia semántica se refiere a una interpretación del sistema lógico: un sistema es coherente si es realizable, es decir, si existe por lo menos una interpretación donde las proposiciones que se derivan en él son verdaderas. La idea intuitiva detrás de la noción de consistencia semántica es que no existe una interpretación que satisfaga o haga verdadera ninguna contradicción. Algunos autores llaman satisfacibilidad a la realizabilidad: 24

Ebbinghaus (1996, pag. 35), Smullyan (1995, pag. 11), Mendelson, (1964, pag. 56); Manzano, (1989, pag. 78). Veremos, en el tercer capítulo de este trabajo, que el nombre “realizabilidad” se reserva generalmente a una noción introducida por Kleene (1974, pags. 450 – 456) para exponer la semántica de los sistemas lógicos intuicionistas, que veremos en este mismo capítulo.

La distinción entre un enfoque sintáctico y un enfoque semántico también puede aplicarse a la definición de saturación. En un sentido sintáctico, la saturación de un sistema puede ser fuerte o débil. 1. Un sistema está sintácticamente saturado, en sentido fuerte, si todas sus proposiciones son deducibles o refutables. Una proposición es refutable si puede demostrarse su negación. 2. Un sistema está sintácticamente saturado, en sentido débil, si cuando le añadimos una proposición no derivable, el sistema se vuelve inconsistente. A la saturación sintáctica fuerte también se le llama completitud (completeness) o suficiencia y a la débil no extensibilidad.

La saturación semántica puede ser absoluta o relativa: a) Un sistema está semánticamente saturado en un sentido absoluto si toda proposición deducible en él es una proposición válida, y viceversa. En un sistema absolutamente saturado todos los teoremas son al mismo tiempo tautologías. b) Un sistema está saturado semánticamente, en un sentido relativo, cuando toda proposición correspondiente a un enunciado verdadero en alguna interpretación del sistema es deducible en éste. 25

A diferencia de la saturación relativa, la saturación absoluta refiere a todas las interpretaciones del sistema.

Kleene (1974, pags. 126 – 127) define completitud tal como hemos definido aquí saturación semántica relativa: “el sistema es completo si su lista de postulados suministra de antemano todo cuanto necesitemos para un determinado propósito [...]. El sistema es completo con respecto a una propiedad (o interpretación), si todas las fórmulas que tengan la propiedad (o expresen proposiciones verdaderas bajo la interpretación) son demostrables”. En un sistema completo, en el sentido de la saturación semántica relativa, los axiomas y reglas de inferencia suministran de antemano lo necesario para demostrar las verdades que las reglas de formación nos permiten expresar. Tal sistema no amerita ser extendido mediante el agregado de nuevos axiomas o reglas de inferencia para lograr que sean deducibles las fórmulas que expresan verdades.

Una propiedad relacionada con la completitud o saturación semántica absoluta de un sistema es la corrección: un sistema es correcto si toda fórmula deducida en él es una tautología. Como explica Manzano (1989, 118), un sistema correcto no induce a error, en el sentido de que no conduce de premisas verdaderas a conclusiones falsas.

En un sentido sintáctico, un sistema es resoluble cuando es posible dar un procedimiento efectivo para decidir si cada proposición del sistema es o no deducible en él. Esta propiedad es una condición que debe cumplir un sistema lógico. En un sentido semántico, un sistema 26

es decidible si se puede encontrar un procedimiento efectivo que permita decidir si cada proposición del sistema es verdadera bajo cierta interpretación o no. Un sentido más fuerte de la resolubilidad semántica se da cuando es posible dar un procedimiento efectivo para decidir si cada proposición del sistema es una tautología o no. A la resolubilidad sintáctica se le llama también decidibilidad y al problema de encontrar un procedimiento efectivo para decidir si una proposición es derivable o no se conoce como el problema de la decisión (Entscheidungsproblem, en alemán).

La categoricidad es una propiedad semántica y refiere a relaciones o morfismos entre interpretaciones o modelos de los sistemas. Un sistema es categórico en sentido absoluto si todos sus modelos son isomorfos entre sí. Es categórico en relación a una cierta clase de objetos que le pertenecen si todos los modelos en los cuales tal clase de objetos recibe la misma interpretación son isomorfos.

Como mencionamos arriba, para comprobar que un sistema tiene alguna de estas propiedades, se formula tal propiedad en el metalenguaje donde se estudia el sistema objeto y se demuestra el enunciado correspondiente, llegándose finalmente a un metateorema sobre el sistema objeto. De las propiedades que hemos definido, la corrección y la completitud de un sistema son las más importantes en lo que refiere a las relaciones entre semántica y sintaxis de un sistema lógico. Especialmente, en un sistema completo los teoremas y las tautologías son idénticos. Para la lógica proposicional clásica se han demostrado teoremas relativos a su coherencia 27

sintáctica, su corrección y su completitud. La demostración de la consistencia y la completitud de la lógica proposicional fueron dadas por primera vez por Emil Post (1921). Otras demostraciones la presentan Hilbert y Ackermann (1938), cuya versión de demostración de completud, entendida como saturación sintáctica débil, se basa en la demostración de un teorema que afirma la existencia de una forma normal para las fórmulas del sistema. Dejaremos para el final de este capítulo la definición y explicación del concepto de forma normal.

En cuanto a la decidibilidad, podemos decir que nuestro sistema de lógica proposicional es decidible desde el punto de vista sintáctico ya que tenemos un procedimiento efectivo para determinar cuando una fórmula es deducible en nuestro sistema. También tenemos un procedimiento para determinar cuando una fórmula del sistema es válida en una interpretación. Lo importante es que, como comentan Curry y Feys (1967, 40) una vez dada toda la información requerida, la corrección de una supuesta demostración sea determinadamente verificable, tal como la noción que hemos presentado aquí.

1.3. Teoría de la demostración El estudio de las propiedades de los sistemas lógicos pertenece al campo de la teoría de la demostración, la cual trata las demostraciones como objetos matemáticos. Esta disciplina nace a comienzos del siglo XX cuando David Hilbert desarrolla su programa de fundamentación de las matemáticas, el cual tenía como finalidad la demostración formal de la consistencia de las matemáticas, es decir, demostrar que éstas estaban libres de contradicción. Para Hilbert, la consistencia era criterio suficiente de existencia matemática. 28

Según Kleene (1974, pag. 69), la demostración de existencia propuesta por Hilbert debía cumplir con ciertas condiciones: debía ser constructiva y finita, es decir, emplear sólo objetos concebibles intuitivamente y procesos mecánicos y, al mismo tiempo, no salir de un ámbito finito, sólo considerar un número finito y determinado de objetos y funciones. Las demostraciones de este tipo son relativas a enunciados que afirman la existencia de demostraciones formales, como el brevemente expuesto teorema de la deducción. Las demostraciones de tales metateoremas indican métodos para construir los objetos matemáticos cuya existencia se ha de demostrar.

Como mencionamos, para Hilbert la no contradicción era un criterio de existencia para los objetos matemáticos. Los enunciados sobre la existencia de objetos matemáticos, cuando refieren a objetos de naturaleza ideal, suponen que la existencia de estos objetos es independiente de si son pensados o imaginados, apareciendo como la determinación de algo real. La concepción de Hilbert plantea que la existencia de una entidad de la cual se requieren ciertas propiedades significa, matemáticamente hablando, la consistencia de las propiedades requeridas de dicha entidad. Kleene (1974, pags. 57 – 58) comenta que originalmente las pruebas de consistencia en matemática se hacían mediante la presentación de modelos, es decir, se trataba de demostraciones de satisfacibilidad de condiciones por una entidad teórica. El método de Hilbert en cambio proponía la prueba de consistencia por medio de la demostración constructiva y finita de la imposibilidad de llegar a una contradicción en una deducción: se trataba, como hemos comentado antes, de demostrar una proposición acerca del sistema estudiado que trate de todas las posibles demostraciones de teoremas en la teoría. Así que el estudio metamatemático de los sistemas formales y la 29

teoría de la demostración tienen su origen en el programa de fundamentación de las matemáticas de Hilbert, que tenía como objetivo la demostración de la consistencia de los sistemas estudiados.

El tipo clásico de demostración constructiva de metateoremas es el razonamiento por inducción estructural aplicado a la construcción de proposiciones y a las derivaciones o deducciones de una proposición. En el caso de las proposiciones elementales, se establece una propiedad y se demuestra que dicha propiedad se conserva al aplicar las diferentes reglas de formación; en el caso de las derivaciones, se establece una propiedad para los axiomas y se demuestra la permanencia de tal propiedad en la aplicación de las reglas de transformación o de inferencia. El proceso de demostración constructiva produce una traducción de la propiedad de los casos elementales a los casos generales. Este tipo de razonamiento es posible cuando las reglas se formulan a través de definiciones inductivas.

El programa de Hilbert fue emprendido por muchos investigadores con entusiasmo y optimismo, dando varios resultados importantes, como la demostración de la completitud de la lógica de predicados de primer orden en por parte de Kurt Gödel (1930): cada exigencia hecha a una entidad matemática que no conduce a ninguna inconsistencia puede ser satisfecha.

Sin embargo, el propio Kurt Gödel (1931) demostró la inviabilidad del programa de Hilbert en los términos en que éste los planteaba. La demostración del primer teorema de Gödel sobre completitud de la lógica de primer orden, dependía mucho de la estructura del dominio de enunciados e inferencias consideradas. Al sobrepasar tales dominios, dejan de 30

coincidir deducibilidad y satisfacibilidad. Gödel demostró en su segundo teorema sobre indecidibilidad que no es posible alcanzar coincidencia entre deducibilidad (teoremas) y satisfacibilidad (tautologías) cuando se imponen ciertas exigencias naturales a la noción de demostración, como que sean constructivas y finitas.

A pesar que el teorema de indecidibilidad de Gödel y sus corolarios respectivos sobre incompletitud de imposibilidad de dar una demostración constructiva de la consistencia de tales sistemas, la teoría de la demostración no fue abandonada: se plantearon nuevas alternativas. La demostración de la coherencia de un sistema exige procedimientos que no pueden ser formalizados en el propio sistema a estudiar. Como nada obliga a usar todos los procedimientos de razonamiento del sistema objeto, se pueden descartar los que no respondan a ciertos criterios. Así que para demostrar la consistencia de un sistema se puede evitar todo razonamiento que no sea constructivo y disponer las cosas para que los procedimientos de razonamiento no formalizables en el sistema objeto a los que haya que recurrir también sean constructivos. Si en estas condiciones logramos demostrar la coherencia del sistema objeto, se habrá demostrado que los razonamientos de la aritmética, incluyendo los no constructivos, no conducen a contradicción.

Las demostraciones de consistencia emplean un modelo que se asocia a las proposiciones del sistema, enunciados formados por los elementos del modelo. La correspondencia entre el sistema y el modelo puede hacerse por medio de transformaciones practicadas a las proposiciones del sistema. Estos procedimientos deberían permitir establecer una correspondencia entre una derivación cualquiera en el lenguaje objeto y otra cuyas proposiciones tengan un carácter más simple. El proceso de transformación así planteado se 31

llama reducción y cada transformación operada se llama etapa de reducción. De acuerdo a Ladrière (1969, pags. 184 – 185), si se puede comprobar que toda derivación en el sistema objeto es reducible, se habrá demostrado la consistencia de tal sistema, pues la proposición ¬ (A = A) no puede ser la última proposición de una derivación y existe al menos una proposición que no se deriva en el sistema objeto

El problema de esta aproximación es la dificultad de demostrar que toda derivación es efectivamente reducible, es decir, que se puede fijar un límite superior al número de etapas de reducción necesarias para transformar una derivación cualquiera en la derivación que resulta de la reducción. Como expone Ladrière (1969, pag. 185), las demostraciones de consistencia de la Aritmética de Ackermann (1924 – 1925), Von Neumann (1927) y Herbrand (1930) no han podido establecer que el proceso de reducción puede efectivamente terminarse cuando la derivación incluye un esquema de reducción y en este sentido han fracasado. Una reconsideración de este procedimiento de demostración ha sido planteada por Gerhard Gentzen.

Casi simultáneamente a la demostración del segundo teorema de Gödel, Gentzen realizó trabajos que con el tiempo se constituyeron en una base esencial y punto de partida de lo que hoy conocemos como teoría estructural de la demostración, al introducir los formalismos que él llamó cálculo de deducción natural y el cálculo de secuentes, los cuales veremos más adelante con cierto detenimiento. Entre otras cosas, estos sistemas permitieron avanzar en la fundamentación de la lógica intuicionista, cuyos planteamientos veremos adelante. En particular, Gentzen (1936) usó estos cálculos para elaborar una demostración combinatoria de la consistencia de la Aritmética de Peano. 32

Los trabajos de Gentzen también introdujeron una idea seminal de lo que hoy conocemos como demostración analítica, la cual se caracteriza por tener una estructura simple en el sentido de que tienen forma normal. Más adelante, al final de este capítulo, explicaremos esto. Antes de exponer los sistemas de Gentzen para la lógica proposicional, dado que éstos permiten una formalización de la lógica intuicionista que está en la base de la correspondencia entre demostraciones y programas que queremos presentar, vamos a ver en qué consiste la lógica intuicionista.

1.4. La lógica intuicionista El programa de fundamentación propuesto por Hilbert surge como alternativa a las críticas que a principios del siglo XX comenzaron a aparecer en contra de lo que hoy llamamos lógica clásica. Brouwer (1908), en su trabajo De onbetrouwbaarhied der logische principes (La no fiabilidad de los Principios Lógicos), cuestionó la validez absoluta atribuida a las reglas de la lógica transmitidas desde Aristóteles. Él y sus seguidores, inspirados en la filosofía de Kant, consideraban que el pensamiento matemático se fundamentaba sobre una intuición originaria: la división de la unidad, que da pie a la dualidad; como explica (Ladrière, 1969, pag, 44), se trata esencialmente de la intuición de la estructura del tiempo, una intuición pura y a priori, independiente de la experiencia que, para los kantianos, constituye la base de la noción de número entero. Según esto, una entidad matemática, como un número, sólo existe gracias al acto mental de un sujeto que lo engendra. Por esto, no se puede progresar en los fundamentos de las matemáticas si no se presta atención a los procesos mentales de donde surgen los objetos o entes matemáticos. Originada en una 33

actividad mental constructiva, las matemáticas serían independientes de la lógica. Por el contrario, la lógica tendría su origen en la matemática.

Para los intuicionistas, el objetivo de la lógica, como actividad dependiente del pensamiento matemático intuitivo, tiene como objetivo formalizar los procedimientos del pensamiento matemático. La lógica sólo tendría sentido como una disciplina de formalización de los procesos que dan origen a los procedimientos de la matemática, por lo tanto, ya no debería centrarse en los procesos deductivos de las pruebas sino indagar los procedimientos empleados en la construcción de éstas. Desde este punto de vista, probar una afirmación sería exhibir el procedimiento para construir su prueba: “probar un enunciado matemático es lo mismo que exhibir un método de construcción de la entidad de la cual habla el enunciado” (Palau, 2002, 81).

La exigencia constructivista que los intuicionistas piden a las demostraciones de existencia matemática, da una interpretación particular a la negación: negar una proposición A equivale a decir que afirmar A conduce a una contracción o absurdo. Si empleamos el símbolo ‘:=’ para significar “se define como”, y el símbolo ‘’ para representar el absurdo, tenemos formalmente que: ¬ A := A ├ 

La exigencia intuicionista de que las demostraciones tengan un carácter constructivo, se traduce en el rechazo de las demostraciones por reducción al absurdo y del principio de tercero excluido. Una demostración por reducción al absurdo deriva la validez de una fórmula A a partir de una deducción que, partiendo de la suposición de la validez de ¬A, 34

concluye en una fórmula contradictoria como B /\ ¬ B. Expresado formalmente: ¬A → (B /\ ¬B) ├ A. El intuicionismo rechaza este principio porque la deducción ‘¬A → (B /\ ¬B) ├ A’ no nos da un procedimiento para construir A. La fórmula ‘¬A → (B /\ ¬B)’ nos dice simplemente que ¬A conduce a una contradicción, algo que ya está implícito en la definición intuicionista de negación. De ello no podemos deducir más. Si pensamos en términos de construcciones mentales, no sirve como criterio de existencia de una entidad que la suposición de su no existencia conduce a un absurdo; la única forma de probar la existencia de una entidad es presentar un procedimiento que permita construirla.

Por otra parte, al interpretar la verdad en términos de “tener una prueba constructiva” y la falsedad como “generar una contradicción”, los intuicionistas toman el principio de tercero excluido “A \/ ¬A” como: la proposición A tiene una prueba constructiva o genera una contradicción. Bajo tal interpretación, no se puede admitir como válido tal principio ya que se podría referir a una afirmación a partir de la cual pudiera no construirse una prueba, lo cual no significa que su rechazo va a generar un absurdo.

En un sistema intuicionista, el concepto semántico de verdad de la lógica clásica se transforma entonces en un concepto epistemológico, pues la verdad de una afirmación matemática se entiende como prueba constructiva, lo cual significa conocimiento de cómo demostrar la verdad de la afirmación. Como consecuencia, también cambia el sentido de la noción de prueba, que ya no estará caracterizada como deducción sino como construcción mental. Esto marca una diferencia entre el planteamiento intuicionista y la teoría de la demostración, tal como originalmente la planteó Hilbert en su programa formalista: si para 35

la teoría hilbertiana una demostración es un objeto, una especie de bloque estático, para los intuicionistas en cambio una demostración es un acto por el cual se muestra la evidencia de un juicio y de esta manera lo hace conocido o aceptado. Cuando Brouwer afirma que una demostración es una construcción mental no pone a la demostración como un objeto estático sino como un proceso dinámico, porque lo que es mental son nuestros actos y la palabra construcción, tal como la usa Brouwer, no es sino sinónimo de demostración: “[Brouwer] pudo haber dicho que la demostración de un juicio es el acto de demostrar o de asirlo. Y el acto es primeramente el acto en la medida que es realizado. Sólo secundariamente e irrevocablemente, el acto que ha sido ejecutado” (Martin-Löf, 1996, pag. 18). Demostrar es aquí hacer conocer, conducir al conocimiento de algo: demostrar no es sino otro sinónimo para entender. En este sentido, desde el punto de vista intuicionista, la teoría de la demostración no es necesariamente una metamatemática, como aspiraba Hilbert, sino una teoría del conocimiento.

Para entender los términos centrales de la lógica intuicionista, vale la pena presentar una descripción de su semántica elaborada por van Dalen (1986). Suponiendo que comprendemos intuitivamente la noción de a es una prueba de la fórmula A, para el caso en que A es atómica y aceptando el conjunto de los números naturales como el dominio de las variables de nuestro lenguaje formal, podemos elucidar qué significa dar una prueba de una fórmula no atómica A en término de sus componentes. Para esto damos el significado de las conectivas proposicionales intuicionistas bajo la suposición de que se sabe qué quiere decir dar una prueba de una fórmula atómica.

36

i)

a es una prueba A /\ B si y sólo si a es un par tal que a1 es una prueba de A y a2 es una prueba de B.

ii)

a es una prueba A \/ B si y sólo si a es un par tal que a1 es una prueba de A o a2 es una prueba de B.

iii)

a es una prueba A → B si, y sólo si, A → B es una construcción que convierte cada prueba b de A en una prueba a(b) de B.

iv)

nada constituye una prueba de , que simboliza lo absurdo o lo contradictorio.

Como puede observarse, no aparece cláusula alguna relativa a la contradicción porque, como ya hemos dicho, para los intuicionistas negar una proposición equivale a decir que su afirmación conduce a un absurdo: ¬ A := A ├ .

La cláusula (ii) se corresponde a la idea de Brouwer de que ninguna fórmula de la forma A \/ B es probable a menos que se pueda demostrar alguno de sus componentes, presentando el rechazo intuicionista del principio de tercero excluido.

Un sistema lógico formalizado basado en la noción broweriana de matemática intuicionista sería llevada a cabo por Heyting (1956). El cálculo proposicional intuicionista presentado por Heyting, que denotaremos por J, fue formalizado usando un conjunto de axiomas, lo cual permite establecer comparaciones precisas con otros sistemas lógicos formalizados en forma axiomática. El sistema sólo tenía como regla de inferencia el Modus Ponens (A, A → B ├ B). Este sistema no incluye principio de tercero excluido ni principio de doble negación, por ello deja fuera de la lógica toda regla de inferencia que pudiera demostrar cualquiera de estos principios, como la reducción al absurdo. El conjunto de axiomas que 37

constituyen la lógica de Heyting son, según Palau (2002): J1

A → (B → A)

J2

(A → B) → ((A → (B →C)) → (A → C))

J3

A → (B → (A /\ B))

J4

(A /\ B) → A / (A /\ B) → B

J5

A → (A \/ B) / B → (B \/ A)

J7

((A → C) → (B → C) → ( (A \/ B) → C )

J8

A → (A → B)

Como dijimos, a estos axiomas hay que agregar el Modus Ponens como regla de inferencia.

Heyting incluyó sólo aquellos axiomas que justifican las inferencias admitidas por Brouwer para las matemáticas. Por ejemplo, según la cláusula (iii) de la semántica que hemos presentado de la lógica intuicionista, para dar una prueba de J3, A → (B → (A /\ B)), primero debemos encontrar una construcción a que convierta la prueba b de A en una prueba a(b) de (B → (A /\ B)). Nuevamente, por la clausula (iii) debemos encontrar una construcción d que convierta la prueba c de B en una prueba d(c) de A /\ B. Supongamos que hay una prueba b de A y que tenemos una prueba c de B, bajo este supuesto y por la clausula (i) podemos construir una prueba de (A /\ B). Hemos obtenido la prueba de (A /\ B) a partir, de dos supuestos: de la suposición de que tenemos una prueba c de B, lo que nos da una prueba d(c) de A /\ B, y lo expresamos por B → (A /\ B); y de la suposición b de A, lo cual nos permite dar una prueba a(b) de (B → (A /\ B)) y lo expresamos por A → (B → (A /\ B)). Cabe preguntarse si una demostración como esta última no podría realizarse en un sistema 38

formal que la hiciera más precisa. Dicho sistema debería formalizar específicamente la noción de construcción. Cómo precisar la noción de construcción de la lógica intuicionista fue un problema que preocupó a varios investigadores. Veremos en el tercer capítulo de este trabajo un par de propuestas de solución a este problema, una de las cuales tiene su origen en el isomorfismo Curry – Howard entre demostraciones y términos lambda que expresan computabilidad de funciones.

Comparando el sistema J de Heyting con el que hemos presentado antes de Hilbert, encontramos que: 1. El condicional está caracterizado por los mismos axiomas: H1 – H2 = J1 – J2. 2. Aceptando que J5 incluye los dos casos de la ley de adición, entonces la disyunción queda caracterizada por los mismos axiomas en ambos sistemas: H3 – H4 = J5. 3. Los axiomas que corresponden a la conjunción son equivales: H5 – H7 ↔ J3 – J4. 4. Los sistemas sólo comparten los axiomas H9 y H10 relativos a la negación, pues el sistema intuicionista no acepta la ley de la doble negación.

En el sistema de lógica intuicionista se entiende por deducción lo mismo que se entiende en lógica clásica, como lo demuestra el hecho de que sea posible demostrar el meta teorema de la deducción o regla de introducción del condicional en el cálculo natural: Si A1, …, A ├ B entonces A1 ,…, An -1 ├ An → B

A primera vista, desde el punto de vista estructural, la lógica intuicionista de Heyting 39

parece diferir de la lógica clásica sólo en la caracterización de la negación, ya que la lógica intuicionista no acepta un axioma del sistema H: ¬¬A → A. Sin embargo, hay que recordar siempre que, aunque los símbolos usados para representar las conectivas en el sistema intuicionista son los mismos que los usados para el mismo objetivo en la lógica clásica, los símbolos para las conectivas no tienen el mismo significado en ambos sistemas, cambia la semántica, por lo que no expresan las mismas funciones lógicas. Para empezar, hay una diferencia sustancial en cuanto a la noción de verdad entre ambos sistemas. Más que la verdad propiamente dicha, lo que interesa a los intuicionistas es la posibilidad de dar un método o procedimiento de construcción para cada entidad cuya existencia se afirma en un sistema y llega a conocerse.

No obstante, para Hilbert, la observación intuicionista respecto al significado de las conectivas lógicas era relevante, pues ponía en evidencia el hecho de que en la lógica clásica, al fijar una semántica bivalente en la que las expresiones de la matemática debe corresponder uno de dos valores, verdad o falsedad, supone que es posible resolver alguna vez todos los problemas matemáticos. Si la lógica clásica plantea una semántica en términos de verdad y falsedad, la lógica intuicionista la plantea en términos de constructividad: “una proposición está construida cuando puede probarse mediante razonamientos intuitivamente correctos” (Hilbert y Ackerman, 1938).

Como mencionamos arriba, al final del apartado anterior, hacia el año 1934 Gerhard Gentzen introdujo sistemas lógicos que permitirían puntos de vistas clarificadores respecto a la naturaleza de la lógica clásica y, en especial, de la lógica intuicionista.

40

1.5. Cálculos de deducción natural Gentzen (1934) introdujo un sistema de deducción que, según él, sería más cercano al razonamiento natural que cualquier sistema axiomático: Mein erster Gesiehtepunkt war folgender: Die Formalisierung des logischen Schliessens, wie sie insbesondere durch Frege, Eussell und Hilbert entwickelt worden ist, entfernt sich ziemlich weit von der Art des Schliessens, wie sie in Wirklichkeit bei mathematischen Beweisen geübt wird. Dafür werden beträhtliche fórmale Vorteile erzielt. Ich wollte nun zunächst einmal einen Formalismus aufstellen, der dem wirklichen Schliessen möglichst nahe kommt. So ergab sich ein “Kalkül des natürlichen SchlieBens,,. (”NJ,, für die intuitionistische, “NK,, für die klassische Prädikatenlogik.) (Gentzen, 1934, pag. 177 )

[Mi punto de partida era el siguiente: la formalización de la deducción lógica, especialmente como ha sido desarrollada por Frege, Russell y Hilbert, se ha alejado demasiado del tipo de deducción que se efectúa en las demostraciones matemáticas. Ellos sólo consideraban las ventajas formales. Yo en cambio quería un formalismo de donde pudiera surgir la deducción real. De ahí surgió un “cálculo de deducciones naturales” (NJ para la lógica de predicados intuicionista, NK para la clásica).]

Por demostración real Gentzen quiere decir las demostraciones usadas por los matemáticos en su labor práctica: Wir wollen einen Formalismus aufstelle, der möglichst genau das wirklische logische Schliessen bei mathematischen Beweisen wiedergibt (Gentzen, 1934, pag. 41

183).

[Queremos edificar un formalismo que refleje lo más exactamente posible los razonamientos lógicos que se utilizan realmente en las demostraciones matemáticas.]

Según este planteamiento, el proceso natural de razonar se realizaría de la siguiente manera:  Se hacen suposiciones temporales  Se derivan fórmulas nuevas aplicando reglas de inferencia  Se aplica un mecanismo para descargar suposiciones El sistema de deducción natural consiste entonces en derivar una proposición a partir de un número finito de suposiciones, no de axiomas, aplicando algunas reglas predefinidas de inferencia. En el curso de la deducción, algunas suposiciones pueden ser "cerradas" o "descargadas". Una suposición es descargada cuando se muestra cómo conduce a una fórmula por la aplicación de reglas de inferencia. Una prueba es una deducción en la que todas las suposiciones han sido descargadas. El concepto de “deducción” queda formalizado al describir rigurosamente el proceso de descarga de suposiciones.

Vemos, pues, que una primera diferencia que destaca entre el cálculo de deducción natural y el sistema axiomático, es que, el primero admite que las reglas de inferencia incluyan como premisas inferencias a partir de hipótesis: Der wesentlishste äusserliche Unterschied zwischen NJ-Heirlaitungen und Heirlaitungen in den Systemen von Russell, Hilbert, Heyting ist folgender: Bei letzsteren werden die richtigen Formeln aus einer Reihe von “logischen Grundformeln” durch wenige Schlussweisen hergeleitet; das natürliche Schliessen 42

geht jedoch im allgemeinen nicht von logischen Gründsetzen aus, sondern von Annahmen, an welche sich logische Schlüsse anschliessen. Durch einen späteren Schlüss wir dann das Ergebnis wieder von der Annahme unabhängig gemacht (Gentzen, 1934, pag. 184).

[La diferencia esencial entre las deducciones en NJ y las derivaciones en los sistemas de Russell, Hilbert y Heyting es la siguiente: en estos sistemas las fórmulas verdaderas son deducidas a partir de una secuencia de 'fórmulas lógicas básicas' a través de unas pocas formas de inferencia. Sin embargo, generalmente la deducción natural no comienza a partir de proposiciones lógicas básicas sino de suposiciones a las que se aplican deducciones lógicas. Por medio de una última inferencia el resultado luego se hace independiente de la suposición.]

El sistema formal de deducción natural para la lógica proposicional consiste de los siguientes componentes: 1. El lenguaje L de la lógica proposicional. 2. Dos grupos de reglas de inferencia: 

Reglas de introducción, que producen enunciados complejos a través de la introducción de conectivas lógicas.



Reglas de eliminación, que producen enunciados más simples al eliminar conectivas.

El cálculo natural carece de axiomas. Su semántica difiere de la de los sistemas axiomáticos, pues no otorga significado a las constantes lógicas presuponiendo la noción de 43

verdad, sino que asocia a cada conectiva un par de reglas de inferencia que determinan su uso. En este sentido, podría decirse que, como observa Palau (2002), la caracterización del significado de las conectivas lógicas en el cálculo natural de Gentzen sigue una línea cercana a la doctrina del significado como uso que plantea Wittgenstein (1953), al limitarse a dar reglas que especifican el uso de las conectivas lógicas3. En este punto de vista, el significado de las proposiciones y de las conectivas lógicas es presentado en términos del rol que las conectivas lógicas juegan dentro del sistema de inferencia.

1.5.1. Lógica clásica Pese a la diferencia en la caracterización semántica de las conectivas lógicas, las presentaciones de la lógica proposicional al estilo axiomático de Hilbert y al estilo inferencial de Gentzen son equivalentes, pues, como el propio Gentzen (1934) demostró, en ambos sistemas son demostrables los mismos teoremas.

A continuación presentamos las reglas básicas de un cálculo de deducción natural (NK):

3

Como veremos al final del tercer capítulo de este trabajo, en el apartado Isomorfismo Curry – Howard y el significado de las constantes lógicas, que esta consideración podría conllevar a un tratamiento convencional de las conectivas lógicas que harían inconsistente al sistema.

44

Conectiva

Cálculo de deducción natural proposicional de Gentzen Reglas de Introducción Reglas de Eliminación

/\

A B__ A /\ B (I /\)

\/

A__ A \/ B

B__ A \/ B (I \/)

→

A /\ B A (E /\) [A] . A \/ B __C C

[B] . C__

(I \/)

[A] . . B A→ B

(E \/) A

A→ B B

(I →) ¬

A /\ B B (E /\)

[A] . . B /\ ¬ B ¬ A

(E →) ¬ ¬A A

(I ¬)

(E ¬)

Intuitivamente, podemos observar correspondencias entre los axiomas H3 y H4 del sistema de Hilbert (principios de simplificación) y la regla de la eliminación de la conjunción; entre H6 y H7 (principios de adición) y la Introducción de la disyunción; entre H11 (doble negación) y la regla de la eliminación de la negación; entre el Modus Ponens y la regla de la eliminación del condicional de NK.

Una forma de razonamiento común en este cálculo es la reducción al absurdo. Para probar que algún enunciado A es el caso, primero asumimos que ¬A es el caso, si esta suposición conduce a contradicción, entonces podemos concluir que ¬A no puede ser el caso, por lo 45

tanto podemos concluir que A debe ser el caso. Como ejemplo, probemos la regla del Modus Tollens: A → B, ¬B ├ ¬ A:  A → B

1

Primera fórmula supuesta

supuesto inicial 2

¬B

Segunda fórmula supuesta supuesto inicial

3

A

Suposición de A supuesto absurdo

4

B

Eliminación de →, 3 y 1 E  1, 3

5

B /\ ¬ B

Introducción del /\, 2 y 5 I /\ 2, 4

6

¬A

Introducción de ¬, 3 y 5 I ¬ 3, 5

Como ya hemos mencionado, las deducciones de este tipo no son aceptadas en la lógica intuicionista, porque ésta, al imponer una semántica basada en la noción de constructividad, no reconoce la validez de las demostraciones por reducción al absurdo.

En realidad, Gentzen presentó sus demostraciones en forma de árbol con hojas o nodos etiquetados, de manera que la demostración que hemos presentado del Modus Tollens sería: 1 [A] (→ E)

A→B B

¬B B /\ ¬ B (¬ I,1) ¬A

(/\ I)

46

Como puede observarse, podemos dividir este árbol en tres aplicaciones de reglas de inferencia: (→ E), (/\ I) y (¬ I). Llamamos derivación inmediata a cada una de estas aplicaciones. Cada derivación inmediata forma una hoja del árbol y lleva como etiqueta una indicación que identifica la regla aplicada. A las suposiciones, que son proposiciones abiertas que deben ser descargadas en alguna derivación inmediata, las podemos poner entre corchetes y podemos ponerle un número que la identifique: es el caso de la suposición que hemos indicado con [A] en nuestra deducción, la cual es descargada en la derivación inmediata del final, donde hemos apliocado la regla (¬ I), es decir, la introducción de la negación.

Hay varias instrucciones que no son explícitas pero que se usan en derivaciones, como muestra Negri (2003): 1.

La misma fórmula puede actuar como suposición y conclusión en una derivación inmediata: 1

[A] (→ I, 1) A→A Como puede observarse, el teorema A → A, cuya deducción presentamos como ejemplo de demostración de un teorema en el cálculo estilo Hilbert para la lógica clásica, es deducible en este cálculo en un solo paso, como una derivación inmediata a partir de la regla (→ I) sobre una suposición A.

2.

Es posible descargar suposiciones que no ocurren en el tope de ninguna rama de la derivación (descarga vacua): 47

1

[A] (→ I, v) __ B → A (→ I, 1) A → (B → A) Esta es la derivación, en el cálculo de deducción natural, del esquema axiomático H2, el principio de introducción de una suposición, del sistema estilo Hilbert que presentamos arriba. Como puede observarse, A → (B → A) significa intuitivamente que podemos introducir suposiciones en una derivación. En la derivación, B → A sería la descarga de una suposión B que no aparece en el tope de ninguna rama de nuestra derivación. Esta descarga la hemos indicado con la etiqueta (→ I, v) , donde “v” indica “vacuo”.

3.

Es posible descargar más de una aparición de la misma fórmula de una vez (descarga múltiple): 3

1

[A → (B → C)] [A] B→C

2

1

(→ E)

[A → B] [A] (→ E) B (→ E) C (→ I, 1) A→C (→ I, 2) ( A → B) → (A →C) (→ I, 3) (A → (B → C)) →((A → B) → (A → C))

Esta es la drivación del esquema axiomátco H2 de nuestro sistema estilo Hilbert, el principio de distribución. Aquí, la segunda aplicación de la regla (→ E) descarga las dos apariciones de la suposición A, señalada como suposición 1. Nótese, de hecho, cuán necesario es el uso de números naturales para marcar paquetes de suposiciones en este mecanismo deductivo de de varias apariciones de una suposición en un solo paso.

4.

Es posible reemplazar una suposición A en una derivación con una derivación de A y obtener una derivación (substitución) “pegando” dos 48

derivaciones: Δ : Γ, A : C En esta derivación, las letras griegas mayúsculas Δ y Γ representan conjuntos de suposiciones.

Luego veremos que estas instrucciones se hacen explícitas en el cálculo de secuentes como reglas estructurales de este cálculo.

Llamamos fórmula principal de una regla de eliminación a la que contiene la conectiva a eliminar y a los componentes de esta fórmula que están en las premisas las llamamos fórmulas activas.

1.5.1. Lógica intuicionista Como el objetivo de Gentzen (1934) era presentar la lógica de Hilbert bajo una forma más constructiva y cercana al razonamiento cotidiano, el primer sistema que expuso fue el cálculo de deducción natural para la lógica intuicionista (NJ). Este sistema, NJ, comparte con el cálculo natural para la lógica clásica (NK) las mismas reglas de introducción y eliminación de conectivas, con excepción de las reglas para la negación, las cuales cambian: Introducción de la negación (I ¬)

Eliminación de la negación(E ¬)

A

____ 49

. __ ¬A

¬A

Hay coincidencia en NJ y NK en I¬, en el sentido de que si partimos de una fórmula A y la derivación nos conduce a una contradicción, entonces podemos concluir la negación de A. No hay coincidencia respecto a E ¬, ya que para NJ vale aquí la regla atribuida a Duns Escoto conocida como principio Ex falso sequitur quodlibet: de una contradicción se sigue cualquier fórmula, la cual no permite deducir el principio de tercero excluido.

La equivalencia entre los cálculos de deducción natural y los sistemas lógicos basados en axiomas, fue demostrada de forma indirecta por Gentzen. Primero propuso un cálculo en el que esta demostración se realizara con mayor facilidad y luego, demostró la equivalencia entre este cálculo y los de deducción natural. Este nuevo cálculo fue llamado por Gentzen el cálculo de secuentes.

1.6. El cálculo de secuentes clásico En el mismo citado trabajo, Gentzen (1934) presentó, además de los cálculos de deducción natural, un cálculo que constituye una aproximación distinta a las nociones de consecuencia lógica y de sistema deductivo: el cálculo de secuentes (Sequenzen Kalküle)4. Como lo dice su título, el trabajo de Gentzen (1934) constituía un estudio de la deducción lógica. La idea del cálculo de secuentes era, en parte, permitir una caracterización formal y rigurosa de la noción de consecuencia lógica. De hecho, podemos considerar el cálculo de secuentes 4

Hablamos de secuentes en vez de secuencias porque Kleene (1974) prefirió traducir el alemán Sequenzen por el inglés secuents, para no confundir el significado preciso al que quería referirse Gentzen con lo que podría ser una secuencia no necesariamente ordenada de fórmulas.

50

como una teoría formal de la relación de deducción.

En una demostración matemática se procede de un enunciado al siguiente hasta alcanzar la aserción del enunciado del cual se quiere probar que es un teorema. Cada enunciado depende de ciertas hipótesis, que pueden ser hipótesis del propio teorema a demostrar o hipótesis adicionales que se asumen temporalmente en el curso de la prueba. Tal procedimiento sería el esbozado por una demostración basada en el sistema de cálculo natural de Gentzen. Podemos entonces describir un estadio de la prueba a través de una lista de las suposiciones correspondientes y el respectivo enunciado que se quiere probar. Según Ebbinghaus (1996, pag. 60) llamamos secuente a una lista no vacía de fórmulas y podemos usarlos para describir estadios de una prueba. Por ejemplo, un estadio de la prueba con las suposiciones “φ1, …, φn” y la afirmación de que φ es un teorema, puede expresarse por la secuencia “φ1, …, φn, φ”. A la secuencia “φ1, …, φn” la llamamos antesecuente y a φ lo llamamos consecuente de “φ1, …, φn”.

Llamaremos secuente precisamente a un estadio o fragmento de una demostración, en la que encotramos dos partes principales: un conjunto o secuencia de hipotesis o suposiciones, que constituye el antecedente, y una secuencia de fórmulas que constituye el consecuente, en donde se descargan las suposiciones en el antecedente. Entre ambas partes, antecedente y consecuente, se establece una relación de deducción o de consecuencia que, en este cálculo, estará caracterizada por un conjunto de reglas, llamadas reglas estructurales. A esta relación la designaremos con el signo ‘’, que intuitivamente puede interpretarse como una descripción de la manera en que se realiza una deducción en el cálculo natural.

51

En este cálculo, un secuente toma la forma: Γ  , donde Γ,  son secuencias de fórmulas cualesquiera y el signo ‘’ es un signo no lógico del lenguaje objeto que permite construir las fórmulas del cálculo de secuentes. Las reglas de los secuentes son locales: cada fórmula C que tiene las suposiciones abiertas Γdepende de las que aparecen en una misma línea: ΓC Las reglas del cálculo de deducción natural sólo muestran las fórmulas activas, que son las fórmulas que funcionan como premisas en las reglas de introducción y eliminación. Las otras suposiciones abiertas, que son las que no han sido descargadas, son mantenidas como suposiciones implícitas. Por ejemplo, la siguiente regla del cálculo de deducción natural: A B A /\ B

/\ I

cuando se le hacen explícitas sus suposiciones, queda: ΓΔ : : A B A /\ B

/\ I

Aquí los puntos son una manera informal para representar la relación de deducción. Cuando se formalizan los puntos que indican la relación de deducción a través del símbolo ‘’, esta regla se convierte en: Γ  A Δ  B ΓΔ A /\ B que, como veremos luego, es una de las reglas del cálculo de secuentes.

El sentido intuitivo de un secuente Γ  es que las suposiciones en Γ implican alguna de 52

las conclusiones en , es decir, que si Γ = {φ1, …, φn} y = {1, …, n}, entonces φ1 /\ … /\ φn implica 1 \/ … \/ n. Las reglas para conjunción y disyunción reflejan esta idea con claridad.

El antesecuente y el consecuente pueden ser conjuntos vacíos: puede incluirse la secuencia nula representada por . Si el antesecuente de un secuente es , es decir,   Δ, o también  Δ, entonces Δ es un teorema y el secuente se reduce a una fórmula del tipo B 1 \/ ... \/ Bn. Si el consecuente es vacío, Γ  o Γ, entonces el secuente tendrá la forma A 1 /\ … /\ An. En efecto, el signo  puede compararse con un condicional → que establece que si todas las fórmulas del antesecuente sean verdaderas entonces alguna de las fórmulas de la consecuente debe ser verdadera:

Una demostración en el cálculo de secuentes consiste en determinar los secuentes que corresponden a fórmulas que constituyen los teoremas de un sistema axiomático. De acuerdo al propio Gentzen (1934), se trata de un cálculo logístico al estilo axiomático de Hilbert, en el sentido de que consta de un axioma y su objetivo es la demostración de teoremas. Como ya hemos dicho, el cálculo de secuentes de Gentzen no trabaja sobre fórmulas particulares sino sobre secuencias de fórmulas. No parte de supuestos sino de una secuencia básica o axioma y dos conjuntos de reglas de inferencias, uno de reglas operatorias y otras consideradas como reglas estructurales, que no hacen referencia a signos lógicos sino a la estructura de las secuencias. Como axiomas del sistema de cálculo de secuencias se toman todas las secuencias de la forma: 53

ΓΓ donde Γ es una secuencia formada por un conjunto cualquiera de fórmulas, sin importar su orden.

Como ya hemos dicho, al axioma se agregan dos conjuntos de reglas, un conjunto de reglas estructurales y un conjunto de reglas operatorias. A continuación, las reglas operatorias:

54

Reglas operatorias para el cálculo de secuencias clásico LK de Genten Conectiva En la antecedente En el consecuente /\

A, Γ   B, Γ   A /\ B, Γ   A /\ B, Γ   (\/) (\/)

\/

A, Γ   B, Γ   A \/ B, Γ  

→

Γ A_ B,   __ A → B, Γ,   

Γ  , A G  , B Γ  A /\ B (\/)

Γ   , A Γ   ,B Γ , A \/ B Γ, A \/ B (/\) (\/) (\/) A, Γ  , B Γ  A → B (→)

¬

Γ  , A ¬ A, Γ  

(→ ) A, Γ  Γ  , ¬ A

(¬)

(¬)

Como puede observarse, las reglas operatorias del cálculo no incluyen reglas de eliminación, sólo incluyen reglas de introducción. Sin embargo, también se dividen en dos grupos. Un grupo de reglas que introducen conectivas en la parte izquierda del secuente, es decir, en el antesecuente; y un grupo que introduce conectivas en la parte derecha del secuente, es decir, en el consecuente. A las primeras se les llama reglas Izquierdas y las otras reglas Derechas. A pesar de que ambos tipos de reglas intoducen conectivas, estas reglas están concebidas de manera tal que existe una correspondencia entre las reglas de introducción y eliminación del cálculo de deducción natural y las reglas derechas e izquierda cálculo de secuentes, respectivamente.

Vimos arriba cómo se obtiene una regla derecha para el conjuntor (/\) del cálculo de secuentes a partir de la regla de introducción del conjuntor del cálculo de deducción 55

natural. Lo mismo vale pare el resto de las reglas de la derecha. Por ejemplo, si hacemos explícitas las fórmulas abiertas no implícitas en la regla de introducción del disyuntor, tendremos: ΓΓ : : A \/ I B A \/ B A \/ B

\/ I

Si damos a los puntos una representación formal a través del signo ’’, y tomamos la secuencia de fórmulas  como vacía, obtendremos las reglas derechas para ‘\/’: Γ  A Γ  A \/ B

Γ  B Γ  A \/ B (\/)

(\/)

Lo mismo vale para la regla de introducción del condicional → y su respectiva regla derecha en el cálculo de secuentes, si hacemos vacía la secuencia 

[A], Γ . B . Γ├A→ B

A, Γ  B ΓA→ B (→ I)

(→)

También es fácil ver cómo la regla derecha de la negación se corresponde con la introducción de la negación, si tratamos como un secuente vacío, lo cual significaría que a partir de una secuencia Γ y una fórmula A arbitraria no se deduce nada: [A], Γ . __ ¬A

A, Γ  Γ  ¬A (¬ E) 56

(¬)

Es más difícil ver cómo se relacionan las reglas de eliminación del cálculo de deducción natural y las regas izquierda del cálculo de secuentes. Para captarlo, hay que tratar las reglas izquierda del cálculo de secuentes como una versión de abajo hacia arriba (downtop) de las reglas de eliminación del cálculo de deducción natural. Por ejemplo, podemos comparar la regla izquierda para el disyuntor, \/, del cálculo de secuentes con la regla de eliminación del cojuntor: [A] [B] . . A \/ B __C C__ C

A  C B  C A \/ B  C (\/)

(\/ E)

En este caso, tenemos la interpretación informal de estas reglas como una formalización de la idea de que si derivamos una fórmula C a partir de una fórmula A o de una fórmula B, entonces puede derivar C de A \/ B. Puede notarse que la regla izquierda del cálculo de secuentes es una representación inversa, de abajo-hacia-arriba, de la regla de eliminación correspondiente del cálculo de deducción natural.

Respecto a las reglas izquierda del cojuntor y su correspondientes reglas de eliminación del cálculo de deducción natural, tenemos: A /\ B A

A /\ B B (E /\)

A  A /\ B 

(E /\) B A /\ B 

(\/) 57

(\/)

La idea aquí es que lo que si no podemos deducir algo de una fórmula A, que en el cálculo de secuentes se representa por la expresión ‘A ’, tampoco podemos deducirlo de la conjunción de esa fórmula A con otra fórmula B. Nuevamente, las regla izquierdas del cálculo de secuentes para la conjunción son una representación inversa, de-abajo-haciaarriba, de las correspondientes reglas de eliminación del cálculo de deducción natural para la misma conectiva.

Más complicado es ver cómo se relacionan las reglas de eliminación con las reglas izquierda en el caso del condicional y de la negación. La relación formal entre la regla de eliminación del condicional y la regla izquierda del condicional es explicada en el tercer capítulo, en el apartado Cálculo de deducción natural con términos lambda, empleando el principio o regla implícita de sustitución del cálculo de deducción natural. Curry (1967, pag. 398) explica la relación apelando a la significación intuitiva de la regla de eliminación del condicional, el modus ponens, que en la práctica puede considerarse como una regla según la cual, teniendo ├ p, toda conclusión que puede obtenerse a partir de ├.q, también puede obtenerse de ├ p → q: ├p→q ├q

├p (→ E)

Γ p q,   __ p → q, Γ,    (→)

En el caso de la negación, tenemos: Γ  A ¬ A, Γ 

¬ ¬A A

(¬) Para la regla izquierda de la la negación tenemos el caso de que, viéndo esta regla como 58

una inferencia de-abajo-hacia-arriba, si no podemos deducir nada a partir de la negación de una suposición A arbitraria, entonces podemos deducir que la proposición A es el caso.

Zucker (1974) ha demostrado que es posible definir una relación correspondencia precisa entre las reglas de introducción y de eliminación del cálculo de deducción natural y las reglas derechas e izquierdas, respectivamente, del cálculo de secuentes. Dicha correspondencia no llega a ser exactamente uno-a-uno, ya que las fórmulas que constituyen una secuencia Γ no están en orden.

Como ejemplo de una derivación en el cálculo de secuentes usando sólo reglas operacionales, presentaremos una derivación del axioma H2 de nuestro sistema estilo Hilbert en el cálculo de secuentes para la lógica clásica:

(Ax) (Ax) C C B  B (→) (Ax) B, (B→ C)  C A  A (→) A, B, A → (B→ C)  C A, A → B, A → (B→ C)  C A → B, A → (B→ C)  A → C A → ( B → C)  (A → B) → (A →C)

(Ax) A  A (→) ( →) ( →) ( →)

 (A → (B → C)) → ((A → B) → (A → C)) Si las reglas operatorias determinan el uso de las conectivas lógicas en el contexto de los secuentes, las reglas estructurales caracterizan la deducción lógica en el cálculo de secuentes y son independientes de las conectivas lógicas contenidas en las partes de un secuente. A continuación presentamos una lista de las reglas estructurales: Reglas estructurales para el cálculo de secuencias clásico LK de Genten Atenuación Γ  _ _ Γ _ 59

A, Γ  

Γ  , A (A )

(A)

Contracción A, A, Γ   A, Γ  

Γ  , A, A Γ  (C )

(C)

Permutación Γ, A, B, F   Γ, B, A, F  

Γ  F, A, B,  Γ  F, B, A,  (P )

Eliminación o Corte

( P)

Γ  F, A A,    Γ,   F, 

Como mencionamos arriba, las reglas estructurales del cálculo de secuentes hacen explícitas varias instrucciones que están implícitas en el cálculo de deducción natural. Por ejemplo, la atenuación introduce una suposición extra en el antecedente y, por lo tanto, se corresponde con la descarga vacua de la deducción natural. La contracción elimina repeticiones, reemplazando la descarga múltiple de la deducción natural. El uso del corte en el cálculo de secuentes se corresponde con la instrucción de sustitución del cálculo de deducción naturtal. El corte expresa en el cálculo de secuentes aquellas instancias de las reglas de eliminación en las que la premisa mayor es derivada, es decir, no es una suposición. Permite realizar con mayor facilidad la traducción del cálculo de deducción natural al cálculo de secuentes. El corte a veces es explicado a través de la práctica familiar en matemáticas de dividir las demostraciones en lemas, como explica Negri (2003).

Una forma de ver cómo las reglas operatorias de Gentzen caracterizan la relación de deducción del cálculo de secuentes es comparar las reglas estructurales con las reglas planteadas por Alfred Tarski como caracterización de la noción de consecuencia abstracta. Varios textos presentan esta relación, por ejemplo Palau (2002, pag. 43 – 71). 60

Como hemos mencionado, el cálculo de secuentes para la lógica clásica acepta múltiples consecuentes en los secuentes. También dijimos que en esta consideración, un secuente Γ Δintuitivamente expresa que la conjunción de fórmulas Γimplica la disyunción de las fórmulas en . Este cálculo, que acepta múltiples consecuentes, se explica como la representación natural de la división en casos que frecuentemente encontramos en las demostraciones matemáticas: el antecedente Γda las suposicines abiertas y el consecuente da los casos abiertos (Negri, 2003, pag. 13). Desde este punto de vista, las reglas lógicas cambian y combinan suposiciones abiertas y casos abiertos. Por ejemplo, la regla /\ reemplaza las suposiciones abiertas A, B por la suposición abierta A /\ B; la regla \/ cambia los casos abiertos A,B en el caso abierto A \/ B. Teniendo sólo un caso, tenemos automáticamente una conclusión a partir de suposiciones abiertas. El caso donde no se tiene alguna fórmula en el consecuente, como Γ, se corresponde con el caso de la deducción vacía, es decir, la imposibilidad.

Al aceptar múltiples consecuentes en los secuentes, es posible derivar el principio de tercero excluido: A A, Γ  A, ¬ A  A \/ ¬ A Con esto, estamos demostrando en el cálculo de secuentes un principio no aceptado en la lógica intuicionista. Para obtener el cálculo de secuentes para la lógica inticionista habrá que aplicar alguna restricción en las reglas lógicas.

61

62

1.6.2. El cálculo de secuentes intuicionista Refiriéndonos exclusivamente al cálculo de secuentes de Gentzen, las derivaciones en un sistema intuicionista tendrían una restricción que lo distingue del cálculo de secuentes para la lógica clásica: en el consecuente de cada secuente no puede figurar más de una fórmula. Así que la regla estructural de atenuación no podrá aplicarse en un consecuente que tenga una fórmula y, por esto, no hay reglas de contracción ni de permutación para el consecuente.

Reglas estructurales para el cálculo de secuencias intuicionista LJ de Genten Atenuación Γ  A Γ   A Γ A (A ) (A) Contracción No hay A, A, Γ  B A, Γ  B (C ) Permutación No hay Γ, A, B  C A, Γ  C (C ) Eliminación o Corte Γ   A A,   C Γ,   C

63

Reglas operatorias para el cálculo de secuencias intuicionista SJ de Genten Conectiva En el antecedente En el consecuente \/ A, Γ  C B, Γ  C Γ  , A Γ  B A \/ B, Γ  C A \/ B, Γ  C Γ  A \/ B ( \/) ( \/) (\/ ) /\ A, Γ  C B,  ┤C Γ  A Γ  B A /\ B, Γ,   C Γ  A /\ B Γ  A /\ B (/\ ) (/\) (/\) → Γ  A B,   C A, Γ  B A → B, Γ,   C ΓA→B (→ ) ( →) ¬ A, Γ ┤ Γ  A Γ  ¬A ¬A, Γ  ( ¬ (¬ ) Las restricciones impuestas a las reglas estructurales del cálculo intuicionista de secuencias muestran que la base inferencial, caracterizada por las reglas estructurales, de la lógica intuicionista es distinta de la base inferencial de la lógica clásica, lo que significa que la relación de deducción de la lógica clásica es distinta a la de la lógica intuicionista. En Palau (2000) encontramos un análisis detallado de esta diferencia basado en la comparación de la noción de deducción del cálculo de secuentes de Gentzen con la caracterización de la noción de consecuencia abstracta de Tarski. El análisis demuestra que la relación de deducción en la lógica intuicionista se ve debilitada por las restricciones impuestas a dos de sus propiedades: la atenuación y el corte. El análisis también demuestra que la relación de deducción de la lógica intuicionista es estructural o lógica, ya que comparte propiedades de la consecuencia abstracta expuesta por Tarski, lo cual significaría que la lógica intuicionista es también una especificación de la lógica abstracta de Tarski. Así que por más débil que resulte su relación de deducción, la lógica intuicionista proposicional es una lógica 64

deductiva. Estos resultados coinciden con los de Gödel (1933) de acuerdo a los cuales

1.7. Normalización Mencionamos arriba que Gentzen introdujo las ideas seminales de lo que hoy se conoce como demostración analítica, es decir, demostraciones en forma normal. En general, podríamos definir forma normal como una organización de los componentes de un objeto formal, sea una fórmula o una demostración, que satisface ciertas propiedades sintácticas que facilitan la comprobación de propiedades sobre el sistema u optimiza la realización de demostraciones en él. De hecho, en un sistema con demostraciones analíticas las demostraciones se adaptan mejor a la automatización porque en las conclusiones aparecen todas las fórmulas usadas en la deducción, lo que reduce el espacio de búsqueda. Un procedimiento que nos permite transformar un objeto de un sistema formal, sea una fórmula o una demostración, en su correspondiente forma normal se denomina normalización. Evidentemente, no se puede hablar de normalización en un sistema en donde ninguno de sus objetos puedan ser llevados a una forma normal. Así que antes de hablar de normalización hay que demostrar que en el sistema, para alguna clase de sus objetos, siempre es posible encontrar objetos equivalentes que están en forma normal.

La prueba de la existencia en los sistemas lógicos de demostraciones en forma normal tiene la peculiaridad de servir para demostrar la consistencia de tales sistemas, pues constituyen una demostración indirecta de esta propiedad. Por ejemplo, en la lógica proposicional, llevar un enunciado a una forma normal disyuntiva permite comprobar si dicho enunciado

65

es una contradicción, como demuestran Hilbert y Ackermann (1938)5.

Junto a la especificación de una forma normal para alguna clase de objetos de un cálculo hay que ofrecer un procedimiento para llevar tales objetos a su correspondiente forma normal. Así es hecho también por Hilbert (1938) cuando proponen un procedimiento para llevar una expresión U a una forma normal conjuntiva equivalente y a su forma normal disyuntiva equivalente.

A un enunciado que afirme la existencia de una forma normal para alguna clase de objetos de un sistema lo llamaremos teorema de la forma normal. Como hemos dicho, la definición o especificación de una forma normal en ciertos cálculos ha sido usada para determinar la consistencia de un sistema. Tal ha sido el caso que hemos expuesto para el cálculo de proposiciones: a partir de la forma normal disyuntiva puede advertirse si una expresión es una contradicción. Kleene (1974) observa que también puede usarse un teorema de forma normal para demostrar consistencia en el cálculo de predicados, si vemos este cálculo como una extensión del cálculo proposicional a través de la inclusión de nuevos operadores lógicos llamados cuantificadores. En esta propuesta de demostración de la consistencia del cálculo de predicados, podemos entender por procedimiento directo de demostración lo que aquí hemos llamado demostración en forma normal y decir que podemos demostrar la consistencia de la lógica de primer orden si podemos demostrar que en ella es posible reducir cualquiera de sus demostraciones a una equivalente en forma normal, es decir, a una 5

En lógica proposicional clásica, una expresión está en forma normal disyuntiva cuando sólo contiene las conectivas \/, /\ y ¬, y en él ningún signo de negación afecta o domina a (está antes de) ninguna fórmula con \/ y ¬, ni ningún signo /\ afecta a ninguna fórmula con signo \/. Una forma normal disyuntiva está formada por una disyunción C1 \/ ... \/ Cn (incluyendo el caso n = 1), donde cada miembro Ci consiste en una conjunción de variables proposicionales negadas y no negadas. Si un enunciado en forma normal disyuntiva tuviera una contradicción, entonces todos los miembros de la disyunción, las conjunciones elementales, tendrían una variable que se presenta tanto negada como no negada.

66

demostración a través de un procedimiento directo. Si podemos demostrar que toda derivación indirecta de teoremas puede hacerse de forma directa, habremos demostrado un metateorema de forma normal para el sistema respectivo. Tal metateorema plantearía entonces que si una fórmula es demostrable, entonces es demostrable en un determinado proceso directo (Kleene, 1974, pag. 395).

Un teorema de este tipo fue obtenido por Gentzen (1934) su Hauptsatz, que en español significa proposición principal, y que no es sino el teorema de la forma normal para los sistemas de lógica de primer orden basados en el cálculo de secuentes. Precisamente, para ilustrar la utilidad de su Hauptsatz, Gentzen (1936 y 1938) estableció demostraciones de consistencia para la aritmética tales como previamente obtenidas por Ackermann (1924 – 1925), von Neumann (1927) y Herbrand (1930).

En general, para demostrar la consistencia de un sistema S usando teoremas de la forma normal puede seguirse el siguiente procedimiento: se indica cierto número de procedimientos de transformación que permitan hacer corresponder a una derivación cualquiera en S otra derivación cuyas proposiciones tengan un carácter más simple, es decir, que tengan una forma normal. Toda transformación realizada de esa manera se denomina etapa de normalización. Si es posible transformar una derivación dada en un número finito de etapas de normalización en una derivación cuya última proposición sea una proposición que satisfaga cierta propiedad, se dice que esta derivación es normalizable. Decimos también que la derivación obtenida está normalizada. La serie de etapas recorridas se denomina normalización. Si se puede demostrar que toda derivación en S es normalizable, se demuestra su consistencia como un corolario del teorema de 67

normalización.

La idea general aquí es especificar una propiedad P para los objetos de un sistema S. Como plantea Kleene (1974, pag. 127), decimos que S es consistente respecto a P si sólo podemos construir correctamente en S los objetos que tienen la propiedad P. Si determinamos que la propiedad P consiste en que las demostraciones de un sistema S son reducibles a demostraciones equivalentes en forma normal, el sistema S será consistente respecto a la respectiva noción de forma normal si sólo son válidas las demostraciones que pueden ser reducidas a su equivalente forma normal.

Gentzen prueba la consistencia de sus sistemas lógicos usando un método indirecto análogo: prueba primero el llamado teorema fundamental o Hauptsatz para el cálculo de secuentes intuicionista LJ y el clásico LK y luego obtiene el teorema de la consistencia para estos sistemas como un corolario del Hauptsatz. El Hauptsatz plantea que cualquier deducción que se realice en el cálculo de secuentes puede hacerse sin aplicar la regla del corte. Decimos que una demostración donde no se aplica la regla del corte tiene una forma normal. El Hauptsatz es, pues, un teorema de la forma normal.

Todas las demostraciones hechas en un cálculo de secuentes que tienen forma normal cumplen la propiedad de la subfórmula, según el cual cada fórmula que ocurre en la demostración de Γ ┤ Δ es una subfórmula de Γ o una subfórmula de una fórmula en Δ. La demostración el Hauptsatz supone la demostración de la propiedad de la subfórmula, formulada en Selding (1998b) de la siguiente manera: Toda fórmula que ocurre en una deducción normal, es decir, que no contiene 68

aplicaciones de la regla del corte, es una subfórmula de la conclusión o una de las suposiciones descargadas. La regla de corte puede ser vista intuitivamente como una expresión de la idea de que, en el proceso de deducción, se puede establecer algún teorema o lema A como un paso intermedio y luego, por el uso de A, podemos establecer la conclusión final B: Γ  A Δ , A  B Γ, Δ  B La regla del corte es la única donde aparecen fórmulas en las premisas que no aparecen en el secuente final: como puede observarse en este esquema, la fórmula A, llamada fórmula del corte o simplemente corte, no aparece en la conclusión, aunque sí aparece en las dos premisas. Por esto, las demostraciones donde se aplica la regla del corte no satisfacen la propiedad de la subfórmula.

Un cálculo de secuentes que no incluye la regla del corte y que es equivalente a un cálculo de secuentes con la regla del corte, es un sistema analítico, es decir, un sistema donde todas las demostraciones están en forma normal. Los sistemas analíticos tiene la propiedad de permitir encontrar demostraciones con facilidad, si tales demostraciones existen. Tal es el caso de un cálculo de secuentes sin cortes, pues en él podemos reconstruir la demostración haciendo en sentido ascendente (del secuente más abajo a los secuentes en el tope) el árbol que representa la derivación. El espacio de búsqueda a cada paso está limitado siempre a subfórmulas que ocurren en el estadio presente. El proceso de búsqueda no puede continuar indefinidamente, porque el número de fórmulas disponibles es finito y eventualmente se repetirán secuentes ya considerados.

Gentzen demostró que toda derivación del cálculo de secuentes que incluya la aplicación de 69

la regla de corte puede ser reducida a una deducción en la cual no se use esta regla. Por ejemplo, en la siguiente demostración se emplea la regla del corte para demostrar la fórmula A /\ B  A \/ C: (Ax.) A  A A /\ B A

(/\ L) A /\ B  A \/ C

(Ax.) A  A A  A \/ C

(\/ R) Corte

Esta demostración de A /\ B  A \/ C puede realizarse también en el mismo sistema del cálculo de secuentes sin usar la regla del corte, existiendo dos posibilidades dependiendo de cómo sea eliminada la regla del corte:

(Ax.) A  A (\/ R) A  A \/ C (/\ L) o A /\ B  A \/ C

(Ax.) A  A (/\ L) A /\ B  A (\/ R) A /\ B  A \/ C

Ahora bien si la regla del corte, que ha demostrado ser una regla derivada y admisible, si dificulta las deducciones en el cálculo de secuentes ¿por qué es incluida en el conjunto de reglas estructurales? Como explica Feferman (1997, pag. 10) lo que justifica la existencia de la regla del corte es que las demostraciones libres de cortes son más complejas que las que usan cortes porque son más largas. Es decir, la regla del corte, como muchas otras reglas derivadas, facilita la realización de demostraciones, especialmente la de la equivalencia entre los cálculos de deducción natural y los cálculos de secuentes.

La demostración del Hauptsatz nos da un procedimiento para construir demostraciones en forma normal en el cálculo de secuentes para la lógica de predicados de primer orden, es decir, nos da un procedimiento de normalización para las demostraciones en el cálculo de 70

secuentes. Además de la propia demostración de Gentzen, podemos encontrar otras en Kleene (1974, pags. 395 – 416), Omondi (1993) , Smullyan (1995) y Sorensen(1998).

Ahora bien, dado que los cálculos de secuentes son equivalentes a sus respectivos cálculos de deducción natural, cabe preguntarse si no habría también una forma normal para las deducciones en estos cálculos de deducción natural y, en consecuencia, un procedimiento de normalización para tales demostraciones. Prawitz (1965) mostró que las derivaciones de teoremas en el cálculo natural para la lógica de predicados de primer orden podían ser normalizadas, es decir, reducidas a una forma normal.

En el cálculo de deducción natural, una deducción en forma normal es una demostración que no tiene desvíos, es decir, una demostración directa, donde la premisa mayor de una regla de eliminación es la conclusión de una regla de introducción. Usemos las variables con la forma Di como el nombre una deducción. Entonces la deducción (*) a continuación es una deducción con desvío: (*)

[A] D1 B (→ I) A→B B D3

D2_ A

(→ E)

Como puede observarse, en la rama izquierda de nuestro árbol de derivación (*), de la suposición A hemos obtenido la fórmula requerida B a través de la deducción D1, por lo tanto podemos deducir la proposición A → B aplicando la regla (→ I). En la rama de la derecha, obtenemos la expresión A a partir de la deducción D2. Tenemos ahora la posibilidad de usar la proposición A → B como premisa mayor, que es la premisa que 71

contiene la conectiva que va a ser eliminada, y la proposición A como premisa menor de una regla (→ E) y obtener como conclusión en nuestro árbol de deducción la proposición B. Encontramos aquí un desvío pues empleamos una regla de eliminación, (→ E), que tiene como premisa mayor una fórmula que hemos obtenido por la aplicación directa de la regla de introducción correspondiente, (→ I).

Prawitz (1965) demostró que cualquier deducción realizada en el cálculo natural puede ser llevada a cabo sin desvíos, es decir, cualquier deducción puede ser transformada en una deducción en forma normal. Propuso además procedimientos para hacer esto, es decir, especificó procedimientos de normalización para el cálculo de deducción natural. Por ejemplo, la derivación (*) puede hacerse de la siguiente manera: D2 [A] D1 B D3 En esta derivación, introducimos la suposición A en una deducción D2, de lo cual deducimos B, pues de la suposición A, puedo obtener B a través de la deducción D1. Hemos hecho un reemplazo de una forma de derivación con desviós a otra equivalente que no tiene desvíos. A esta operación de reemplazo la llamamos paso de reducción. Hay que observar que el número de apariciones de D2 necesarias en la versión reducida es el mismo número de apariciones de la suposición descargada en la inferencia indicada por → I en la primera deducción. La fórmula A → B de la primera deducción, que es la introducida por la aplicación de una regla de introducción, se llama fórmula del corte o simplemente corte del paso de reducción.

72

Una reducción es una secuencia, posiblemente vacía, de pasos de reducciones. Veamos un ejemplo de reducción de una deducción. Consideremos la siguiente deducción: 2 [A → (A → A)] A→A

1 [A]

(→ E)

1 [A] (→ E) 3 A (→ I , 1) [A] (→ I, v) A→A (→ I, 2) [A → A] (→ I, 3) A → (A → A) → (A → A) A → (A → A) (→ E) A→A

Apliquemos un paso de reducción para eliminar el corte A → (A → A) → (A → A): 1 [A] (→ I, v) (A → A) (→ I, 1) A → (A → A) A→A

2 [A]

(→E)

2 [A]

(→ E)

A (→ I -2) A→A Ahora volvamos a plicar un nuevo paso de reducción para eliminar A → (A → A) 1 [A] (→ I, v) 1 [A → A] [A] (→ E) A (→ I,1) A→A Un último paso de reducción elimina el corte A → A: [A] A→A

(→ I, v)

que no es más que la aplicación de la intrucción implícita según la cual la misma fórmula puede actuar como suposición y conclusión en una derivación inmediata.

Tal posibilidad de demostraciones sin desvíos se basa en el hecho de que una regla de eliminación no agrega más información que la introducida por una regla de introducción. El propio Gentzen (1934, pag. 189) había dicho: 73

Die Einführungen stellen sozusagen die ‘Definitionen, der betreffenden Zeichen dar, und die Beseitigugen sind letzten Endes nur Konsequenzen hiervon, was sich etwa so ausdrücken lässt: Bei der Beseitigung eines Zeichens darf die betreffende Formel, un deren äusserstes Zeichen es sich handelt, nur “als das benutzt werden, was sie auf Grund der Einfürung dieses Zeichens bedeutet,,.

[En alguna manera, las introducciones representan las 'definiciones' de los símbolos involucrados y las eliminaciones no son más, en el análisis final, que las consecuencias de estas definiciones. Este hecho puede ser expresado como sigue: al eliminar un símbolo, lo hacemos ‘sólo en el sentido permitido por la introducción del símbolo’]. Inmediatamente, Gentzen intentó clarificar este pasaje a través de un ejemplo. Refiriéndonos al condicional, tenemos que la regla de introducción del implicador puede ser interpretada como lo explica Troelstra (1996, pags. 11 – 12): si tengo un método D para obtener una conclusión B a partir de una suposición A, he establecido A → B, donde A ya no es una suposición. La eliminación del condicional puede ser interpretada como: si tenemos la fórmula A → B, esto significa que tengo un método D para obtener B a partir de A; tenemos un argumento para A; por lo tanto B. Esta última regla obtiene su validez del hecho de que la regla de introducción del condicional dice que un condicional está dado por “un método D para obtener una conclusión B a partir de una suposición A”. Sin esta especificación, la regla de eliminación del condicional ya no sería válida.

74

Prawitz (1965) profundizó en este hecho y postuló el principio de inversión, según el cual, en el cálculo de deducción natural las reglas de eliminación pueden obtenerse a partir de reglas de introducción, con las cuales están en correspondencia. En palabras de Sara Negri (2003, pag. 4): La conclusión de una regla de eliminación R con premisa mayor A * B ya está contenida en las suposiciones usadas para derivar A * B a partir de las reglas de introducción de la conectiva * junto a las premisas menores de la regla. Aquí el símbolo ‘*’ representa cualquiera de las conectivas del sistema. Tenemos entonces que las reglas de eliminación son inversas a las correspondientes reglas de introducción en tanto que nada se gana si una regla de introducción es seguida por una regla de eliminación, pues una regla de eliminación no introduce más información que la que ha puesto en ella la regla de introducción. Lo que hace un desvío es simplemente añadir redundancias que incrementan inútilmente la complejidad de las deducciones.

Veámos qué ocurre ahora con un desvío que involucre la conjunción. Según la regla de introducción del conjuntor, la proposición A /\ B tiene como fundamento directo la derivación de A y la derivación de B: D1 D2 : : A B /\ I A /\ B Tenemos entonces dos deducciones con desvío sobre la conjunción: D1 D2 : : A B /\ I A /\ B /\ E A

D1 D2 : : A B /\ I A /\ B /\ E B

Las cuales pueden reducirse o contraerse respectivamente a: 75

D1 : A

D2 : B

Por tanto, si la regla /\I es seguida por /\E, la derivación puede ser simplificada o reducida.

Veámos ahora el caso de la disyunción. Aquí también tenemos dos posibles deducciones con desvío: · · A A \/ B

A · · C

B · · C___

· · B A \/ B

C

A · · C

B · · C___

C

las cuales pueden ser reducidas respectivamente a: A · · C

B · · C

Una deducción en el cálculo de deducción natural que no contiene desvíos se llama deducción en forma normal: es una deducción en la que no puede efectuarse un paso de reducción o que no puede ser ya reducida. Una deducción normal no tiene desvíos, es decir, en ninguna sus rama encontramos una aplicación de una regla de eliminación cuya premisa mayor (la que tiene la conectiva que va a ser eliminada) es la conclusión de la regla de introducción de la respectiva conectiva.

Ahora bien, es notable que, en los desvíos, la premisa mayor de la regla de eliminación es una fórmula crítica. Reducir una fórmula con desvío a una sin desvío requiere la supresión 76

de esta fórmula, que llamamos fórmula de corte o simplemente corte em el cálculo de deducción natural. Deberíamos poder decir entonces que una deducción normal es una que carece de cortes. Sin embargo, no siempre queremos eliminar los cortes. Consideremos la deducción de (A → B) \/ (A → C), A ├ B \/ C:: 3 1 [A → B] [A] (→ E) B (\/ I) ↓ (Segmento 1) ↓ B \/ C (\/ I, 1) (A → B) \/ (A → C) A → B \/ C A → B \/ C

4 2 [A → C] [A] (→ E) C (\/I) ↓ (Segmento 2) ↓ B \/ C (\/ I, 2) A → B \/ C (\/ E, 3, 4) A (→ E) B \/ C

Aunque esta deducción no contiene fórmulas de corte, lo deseable sería reducirla: 1 [A → B] A (→ E) B (\/I) (A → B) \/ (A → C) B \/ C B \/ C

2 [A → C]

A (→ E) C (\/ I) B \/ C (\/ E, 1, 2)

Para entender cómo llevar a cabo esta deducción, necesitamos la noción de segmento, que tomamos de Seldin (1988b): una secuencia de fórmulas C1, …, Cn, donde todas las fórmulas son las mismas y, para i = 1, …, n – 1, Ci es una premisa menor de una inferencia por (/\ E) para la que Ci+1 es la conclusión. Un segmento es un segmento máximo si C1 es la conclusión de una regla de introducción y Cn es la premisa mayor de una regla de eliminación. De acuerdo a estas definiciones, una fórmula de corte es un segmento máximo con un largo igual a 1.

En la primera deducción de la fórmula “(A → B) \/ (A → C), A ├ B \/ C” hay dos segmentos que tienen la fórmula “A → B \/ C”; en la segunda deducción también tenemos 77

dos segmentos, pero éstos contienen la fórmula “B \/ C”. Los segmentos de la primera deducción son máximos porque sus primeras deducciones tienen conclusiones obtenidas a partir de una regla de introducción y sus últimas fórmulas son premisas mayores de una regla de eliminación.

Las reducciones que habíamos presentado antes de estas dos últimas se habian realizado eliminando fórmulas de corte, que son segmentos máximos de largo igual a 1. Para reducir segmentos de largo mayor a uno necesitamos otro procedimiento, una reducción que reemplace por otra una parte de una deducción que tenga la siguiente forma: 1 2 [A] [B] D0 D1 D2 A \/ B C C (\/ E, 1, 2) C (D4) E D4

R

donde R es una regla de eliminación con C como su premisa mayor y D4 como la(s) deducción(es) de la(s) premisa(s) menor(es). Tal reducción convierte esta deducción en la siguiente: 1

D0 A \/ B

[A] D1 C D4 R E E D4

2 [B] D2 C D4 R E (\/ E – 1 – 2)

A un paso de reducción tal, en el que se tratan segmentos máximos, Seldin (1988b, pag. 13) lo llama paso de reducción \/E.

78

El teorema de normalización para el cálculo de deducción natural podría enunciarse según Seldin (1998b) entonces de esta manera: Toda deducción del cálculo de deducción natural puede ser reducida a una deducción en forma normal, es decir, una deducción que no puede ser reducida porque en ella no hay segmentos máximos, y tiene las msmas suposiciones descargadas y la misma conclusión.

La demostración de este teorema nos da un procedimiento de normalización: 1. Se aplican pasos de reducción a los segmentos máximos de rango máximo y tamaño mayor que uno que comience esos de máximo largo. 2. Cuando todos los segmentos máximos de rango máximo tengan un largo igual a uno, estando ya convertidos en fórmulas de corte, se aplican los pasos de reducción a las fórmulas de corte de rango máximo para el cual no hay fórmula de corte con rango máximo por encima de él o encima de cualquier premisa menor para la inferencia por la cual ellas son premisas mayores. 3. Cada paso de reducción va reduciendo la deducción hasta que eventualmente el proceso debe terminar en una deducciónn normal con las mismas suposiciones descargadas y la misma conclusión.

Como ya hemos mencionado, los teoremas de forma normal y de normalización permiten demostrar la consistencia de los sistemas. El teorema de consistencia para el cálculo de deducción natural es formulado por Seldin (1998b, pag. 15) de la siguiente manera: No hay demostración (deducción sin suposiciones descargadas) cuya conclusión sea una forma atómica. 79

La demostración de este teorema sería la siguiente: Si hubiera una demostración tal, con una fórmula atómica como conclusión, habría para ella una deducción que es normal. Para el caso del condicional, tendríamos que la rama principal de una deducción normal que termina en una fórmula atómica no puede tener ninguna inferencia por la aplicación de →I; pues estas inferencias tendrían que ocurrir al final de la rama, y esto significaría que la última inferencia de la deducción es por la aplicación de →I, lo que contradiciría la hipótesis de que la conclusión es una forma atómica. Puesto que →I descargan suposiciones, la fórmula en el tope del brazo principal no es descargado, contradiciendo la suposición de que tal deducción es una demostración. Para el resto de los casos, tendríamos la rama izquierda, que conduce a la premisa mayor de una regla de introducción, termina en una fórmula atómica que consiste solamente en reglas de eliminación y, aunque \/E puede descargar suposiciones, no se puede descargar suposiciones sobre la premisa principal.

Como hemos mencionado, Dag Prawitz (1965) demostró el teorema de normalización para el cálculo deducción natural para la lógica de predicados, presentando la noción de relación de reducción entre derivaciones en la lógica de primer orden las cuales son generadas por un conjunto de contracciones. Presentamos estas contracciones a continuación sin incluir las correspondientes a las reglas que usan cuantificadores, que pertenecen a la lógica de predicados:

80

Cálculo de deducción natural de Gentzen Fórmula no contraída Fórmula contraída

Contracción →

[A] · · B A→B

· · A · · B

· ·_ A_ B

/\ (a)

/\ (b)

\/ (a)

· · · · A B A /\ B A

· · A

· · · · A B A /\ B B

· · B

· · A A \/ B

A · · C

B · · C___

· · A · C

A · · C

B · · C___

· · B · C

C \/ (b)

· · A A \/ B C

\/E

1 2 [A] [B] D0 D1 D2 A \/ B C C (\/ E, 1, 2) C

D0 ( D4) A \/ B

R E D4 81

1 [A] D1 C D4 R E E D4

2 [B] D2 C D4 R E (\/ E, 1, 2)

En esta tabla se presenta la relación de contracción como una relación de equivalencia entre las fórmulas en la segunda columna (fórmulas no contraidas) y las fórmulas de la tercera columna (fórmulas contraidas). Hemos agregado la contracción \/E a la original de MartinLöf (1972), en la que ésta no aparece y que hemos tomado de Seldin (1988b).

El descubrimiento atribuido aquí a Prawitz (1965), y presentado aquí a través de los trabajos de Seldin (1988b), Negri (2003), Stalmarck (1991), Smullyan (1995), Stewart (1999) y Martin-Löf (1972), tiene diversas repercusiones. Por una parte nos plantea la cuestión de la relación entre la normalización en el cálculo de la deducción natural y la normalización en el cálculo de secuentes o, planteada de otra manera, la relación entre el corte en el cálculo de secuentes y de los desvíos en el cálculo de deducción natural. Al respecto vale la pena mencionar el artículo de Zucker (1974) que presenta precisamente un estudio de la correspondencia entre la eliminación del corte y la normalización.

Zucker define por inducción una relación de correspondencia  entre las derivaciones del cálculo de secuentes intuicionista (LJ) y la del cálculo de deducción natural intuicionista (NJ). La correspondencia  es definida de tal manera que es obvio que si d es una derivación en LJ del secuente Γ  C, entonces (d) es una derivación de C en NJ cuyas suposiciones abiertas son los miembros de Γ. Al mismo tiempo, Cada derivación Π de C en NJ a partir de fórmulas A1, …, An puede ser transformada en una derivación ’(Π) en LJ del secuente A1, …, An  C, siendo ’ una relación de correspondencia definida por inducción que permite transformar derivaciones en NJ a derivaciones en LJ. Por las correspondencias 82

y ’ se establece entonces la equivalencia entre NJ y LJ: Una fórmula C es derivable en NJ a partir de las suposiciones A1, …, An si, y sólo si, A1, …, An es derivable en LJ. Por esta vía, Zucker demostró la existencia de una relación de correspondencia entre la normalización en el cálculo de deducción natural y el cálculo de secuentes: si las reglas en LJ son interpretadas como una definición inductiva de la derivabilidad en NJ, entonces las reglas de un sistema LJ libre de corte pueden ser interpretadas como una definición de la derivación normal en NJy viceversa.

Tenemos entonces que la demostración del teorema de forma normal para el cálculo de deducción natural intuicionista de la lógica de predicados de primer orden establece que toda derivación en este cálculo se puede reducir a una derivación en forma normal. Veremos que la normalización en el fragmento condicional positivo cálculo de deducción natural intuicionista de la lógica proposicional, que sólo incluye las reglas operatorias de introducción y eliminación para el condicional, está en correspondencia con la normalización en el cálculo lambda con tipos. Constataremos que esta correspondencia es uno de los aspectos más esenciales y profundos la correspondencia entre demostraciones y programas que existe entre el cálculo de deducción natural intuicionista y el cálculo lambda con tipos.

83

84

II. Computabilidad y Cálculos Lambda 2.1.- Relevancia lógico – matemática de la noción de computabilidad. La noción de computabilidad surgió en el campo de la lógica y de las matemáticas a raíz de las investigaciones surgidas para determinar la decidibilidad de los sistemas formales. El objetivo de esas investigaciones era resolver el Entscheidungsproblem, que en español significa problema de la decisión, y que en lógica simbólica consiste en encontrar un algoritmo o procedimiento mecánico general que decida, para enunciados dados, si son universalmente válidos o no. Dar una respuesta a este problema condujo a la necesidad de plantear una definición rigurosa de la noción de computabilidad.

El primer trabajo que arrojó resultados decisivos en esta dirección fue el presentado por Kurt Gödel (1931), “Sobre sentencias formalmente indecidibles de Principia Mathematica y sistemas afines”, donde el autor presenta una demostración constructiva de la indecidibilidad de la lógica de primer orden. Gödel demostró que en un sistema formal de lógica de primer orden, como el presentado en los Principia Matemática de Russell y Whitehead (1910 – 1913), existe una proposición que no es decidible, es decir, una proposición tal que no es posible encontrar un procedimiento efectivo y mecánico a través del cual deducirla ni a ella ni a su negación. Aunque esta demostración no requiere una definición de la noción de computabilidad, sí supone la noción, introducida por sugerencia de Herbrand, de clase de funciones recursivas, la cual es equivalente a la noción de funciones computables: Church (1936) demostró que las funciones recursivas generales son equivalentes a las funciones definibles en el cálculo lambda, y Turing (1937) demostró que las funciones definibles en el cálculo lambda son equivalentes a las funciones computables; como la relación de equivalencia es transitiva, las funciones recursivas generales son 85

equivalentes a las funciones computables.

En el citado trabajo de Gödel, aparece la primera definición explícita de la clase de funciones numéricas recursivas primitivas: “funciones obtenidas por composición y recursión a partir de ciertas funciones iniciales triviales” (Mosterín, 1989, pag. 48). La clase de las funciones y relaciones recursivas primitivas, como afirma (Kleene, 1974, pags. 223224), son expresables numeralmente en un sistema formal, o dicho en palabras de Gödel (1931, pag. 78): “Cada relación recursiva primitiva es aritmética” y forma parte esencial de la demostración de la indecidibilidad de la lógica pura de los predicados de primer orden. Esta clase de funciones, como hemos ya mencionado, también están estrechamente relacionadas con las investigaciones acerca de la computabilidad.

Los resultados de Gödel daban un golpe decisivo al programa formalista de David Hilbert: “El fin aceptado, a saber, construir las matemáticas sólidamente, es también el mío: yo quisiera devolver a los matemáticos su antigua pretensión de una verdad inatacable, que las paradojas de la teoría de conjuntos han parecido debilitar; pero yo creo que es posible alcanzar este fin conservando íntegramente todo lo que se ha conseguido” (Tomado de Ladriére, 1974, pag. 28). Como vimos en el primer capítulo de este trabajo, Hilbert aspiraba superar las paradojas descubiertas en las matemáticas clásicas sin eliminar de ella fragmentos críticos que eran desechados el programa intuicionista emprendido por Brouwer y sus seguidores. Para esto, Hilbert proponía demostrar la consistencia de las matemáticas como criterio de existencia.

El programa de Hilbert requería una formalización completa de la matemática clásica, lo 86

cual suponía: 1) construir sistemas formales completos para las principales teorías de la matemática clásica, 2) probar la consistencia de dichos sistemas formales. Para 1930, se pensaba que los Principia Matemática de Russell y Whitehead constituían una formalización completa de la matemática clásica. Entonces la preocupación fundamental de los lógicos y matemáticos era establecer la consistencia de este formalismo y de otros equivalentes, como la teoría axiomática de conjuntos. El teorema de Gödel (1931) demostraba que los sistemas formales de la matemática clásica, incluyendo los Principia Matematica y la aritmética formal de Peano, si son consistentes y completos, entonces son indecidibles: “para cada uno de ellos puede efectivamente construirse una sentencia indecidible (tal que ni ella ni su negación es deducible)” (Mosterín, 1989, pag. 45). Quedaba demostrada la imposibilidad de demostrar la consistencia de un sistema formal de la matemática clásica a través de procedimientos constructivos y finitos, no importa los recursos y razonamientos incorporados al sistema.

Usando las ideas y técnicas basadas en la obra de Gödel, varios lógicos desarrollaron en la década de 1930 herramientas lógicas para establecer resultados de insolubilidad absoluta que condujeron a algunas aplicaciones espectaculares, incluyendo la prueba rigurosa de la imposibilidad de solucionar del décimo problema de Hilbert, el que inició el interés en la resolución del Entscheidungsproblem. Entre las pruebas de la insolubilidad absoluta, la más directa resultó la de Turing a través del uso de máquinas abstractas.

En el año 1900, David Hilbert, en el II Congreso Internacional de Matemáticos en París, 87

presentó una lista de veintitrés problemas matemáticos que todavía no estaban resueltos y que él consideraba un reto que los matemáticos del siglo XX debían enfrentar. El décimo de estos problemas era determinar si es posible encontrar un procedimiento mecánico o algoritmo para resolver ecuaciones diofánticas: “Dada una ecuación diofántica con cualquier número de cantidades desconocidas y con coeficientes numéricos de enteros racionales: diseñar un procedimiento que pueda determinar por un número finito de operaciones si la ecuación se puede solucionar en enteros racionales” (Matiyasevich, 1996, pag. 2). Este planteamiento implica la cuestión de si hay un método simple que pudiera ser aplicado a la solución de cualquier ecuación. Desde los tiempos del matemático Diofanto de Alejandría, siglo III a. C, muchos matemáticos han encontrado pruebas de que muchas ecuaciones de otro tipo no tenían solución. En estos casos, para cada clase de ecuación se tenía que inventar un método diferente. El décimo problema de Hilbert exige un método universal para reconocer la posibilidad de resolver ecuaciones diofánticas. Se trata del Entscheidungsproblem, el problema de la decisión: encontrar un método universal que pueda ser aplicado a cada problema que pueda ser solucionado a través de un sí o un no (Matiyasevich, 1996, pag. 3).

Una ecuación diofántica es una ecuación de la forma: D(x1, …, xn) = 0, donde D es un polinomio con coeficientes enteros. Es fácil determinar si una ecuación tal con coeficientes enteros a0, … an tiene soluciones enteras, pues toda raíz entera debe dividir a0, así que todo lo que hay que hacer es probar el número finito de los divisores de a0. El problema no es tan sencillo con ecuaciones como la siguiente (Penrose, 1991, pag. 91): 88

(x + 1)w+3 + (y +1) w+3 = (z + 1)w+3 Esta ecuación está relacionada con un famoso problema no resuelto en matemáticas: ¿existe un conjunto de números naturales w, x, y, z que satisface esta ecuación? Para responder a esta cuestión habría que dar un procedimiento algorítmico general para resolver cuestiones matemáticas, es decir, una respuesta a la cuestión de si semejante procedimiento podía existir en principio (Penrose, 1991, pag. 61).

Años después, en 1928, como informa Davis (1965), en un congreso de matemáticas en Boloña, Hilbert planteó el problema de decisión llamándolo “el problema fundamental de la lógica matemática”. El problema consistía en dar un algoritmo que decidiera si una fórmula lógica era una consecuencia lógica (en el sentido semántico) de un conjunto finito dado de premisas.

Como mencionamos arriba, el Entscheidungsproblem fue resuelto por Gödel (1931) de forma negativa: los sistemas formales de la matemática clásica son indecidibles, pues en ellos puede construirse efectivamente un enunciado que ni él ni su negación pueden ser deducidos. También dijimos que esta demostración estaba basada en el uso de funciones recursivas y que éstas habían demostrado ser equivalentes a las funciones computables, es decir, que podían ser computadas por cierto tipo de máquinas abstractas. La aproximación por funciones computables fue considerada por el propio Gödel como una vía más rigurosa. En la nota complementaria de 1963 a su trabajo “Sobre sentencias formalmente indecidibles”, Gödel (1931) reconoce que: Como consecuencia de avances posteriores, en particular del hecho gracias a la obra de A. M. Turing ahora disponemos de una definición precisa e indudablemente 89

adecuada de la noción general de sistema formal, ahora [...] se puede probar rigurosamente que en cada sistema formal consistente que contenga una cierta porción de teoría finitaria de números hay sentencias aritméticas indecidibles y que, además la consistencia de cualquiera de esos sistemas no puede ser probada en el sistema mismo. Gödel veía en la prueba de imposibilidad de resolver el problema de la decisión, llevada a cabo por Turing, que estaba basada en la noción de computabilidad, una herramienta rigurosa para el análisis de la decidibilidad de sistemas formales; la propiedad característica de los sistemas formales consistía en que “en ellos el razonamiento puede ser, en principio, completamente reemplazado por operaciones mecánicas” (Gödel, 1931, pag. 87). De esto último trata precisamente el estudio de Alan Turing (1937) sobre computabilidad.

Turing (1937) demostró que el Entscheidungsproblem (problema de la decisión) planteado por Hilbert en 1900, no podía ser resuelto, en concordancia con los resultados obtenidos por Gödel (1931). En consecuencia, es imposible decidir algorítmicamente si los enunciados en la aritmética son ciertos o falsos. Para sus demostraciones, Turing usó un tipo de máquinas abstractas capaces de ejecutar algoritmos a través de cómputos simbólicos. Con este sistema, probó que no había procedimiento de decisión o algoritmo general alguno para determinar si el cómputo de un algoritmo por una máquina abstracta, llamada hoy máquina de Turing, llegaría a término.

Para realizar su demostración, Turing redujo el Entscheidungsproblem al problema de la detención para máquinas de Turing. Estas máquinas son dispositivos abstractos que realizan cálculos o cómputos basándose en información simbólica. Trabajan sobre cadenas o tiras de 90

símbolos que va leyendo sobre una cinta virtualmente infinita y reconociendo uno por uno, para tomar decisiones sobre la base de la información suministrada por el símbolo leído y que van cambiando su estado interno. Una vez activada, una máquina de Turing inicia la lectura de la tira de símbolos y va pasando de un estado a otro. El paso a un nuevo estado depende de su estado actual y del símbolo que lee en determinado momento. Eventualmente, el proceso de lectura se debe detener y la máquina queda en un estado final donde la tira de símbolos que procesa la máquina informa sobre el resultado del proceso de cómputo que ha ido de un estado inicial, que ha activado la máquina, a un estado final, donde la máquina se detiene, después de haber pasado por una serie de estados intermedios. El proceso de computación de una máquina de Turing, que se inicia en un estado de activación A y conduce a un estado final B, donde el proceso se detiene, determina una función f de A hacia B: f: A → B. El problema de la detención consiste en determinar si hay procedimiento para determinar si para ciertas cadenas de símbolos la máquina llegará a un estado final y detendrá su actividad.

Para demostrar que la lógica de primer orden era indecidible, Turing supone primero que tenemos un algoritmo de decisión general para esta lógica. Luego formula el problema de la detención —la cuestión de determinar si una máquina de Turing se detiene o no para un estado inicial de activación dado— como un enunciado de la lógica de primer orden que podría ser susceptible de un algoritmo de decisión. Finalmente, Turing demuestra que ningún algoritmo general puede dar un procedimiento efectivo para decidir si una máquina de Turing dada puede detenerse sobre una cadena de símbolos arbitraria para un estado 91

inicial de activación dado: no es posible dar un algoritmo para resolver el problema de la detención.

Cualquier demostración de insolubilidad se puede establecer reduciéndolo al problema de la detención, es decir, mostrando que si tal función fuera computable entonces el problema de la detención fuera solucionable; cada prueba depende de resultados específicos al campo en que aparecen los problemas.

Varias propuestas de demostración de indecidibilidad o irresolubilidad han demostrado ser equivalentes a la computabilidad de Turing (1936-1937). Entre ellas se encuentran: 1. La recursividad general (J. Herbrand, 1930 y Gödel, 1931). 2. La definibilidad lambda (Church 1933, Kleene 1935, Church 1941). 3. Calculabilidad efectiva (Kleene, 1974, pags, 272 – 274]. 4. Sistemas canónicos y normales (Post 1943, 1946). 5. Alonso Church (1936) demostró, como ya mencionamos, la equivalencia o coextensividad de las funciones definibles en el cálculo lambda con las funciones recursivas generales. Llamaremos funciones lambda-definibles a las que pueden ser expresadas a través del cálculo lambda, originalmente concebido por Church para demostrar la consistencia de las matemáticas clásicas. Las funciones recursivas generales, como explica Kleene (1974, pag. 251) son las que pueden ser definidas recursivamente a través de un sistema de ecuaciones determinado. La equivalencia de las funciones computables con las funciones lambdadefinibles (y por lo tanto, con las funciones recursivas generales) fue demostrada por Turing (1937). Los sistemas canónicos y normales de Post (1943, 1946) dan como resultado 92

directo un equivalente de la enumerabilidad recursiva, lo cual permite obtener un equivalente de la recursividad.

La definibilidad de funciones a través del cálculo lambda es un planteamiento más abstracto de la noción de computabilidad que el de Turing, donde apenas podemos encontrar una conexión con cualquier planteamiento que intuitivamente pudiéramos considerar mecánico. Uno de los rasgos más interesantes de la definición de funciones a través del cálculo lambda es que enfatiza la idea de que “la computabilidad es una idea matemática, independiente de cualquier concepto particular sobre una máquina de computar” (Penrose, 1991, pag. 101).

2.2.- El cálculo lambda de Alonso Church y la noción de computabilidad El cálculo lambda, pensado originalmente para facilitar la fundamentación de la aritmética, es una notación especial para representar funciones. Antes de que Church hiciera su presentación, ya varios lógicos venían emprendiendo investigaciones que iban conduciendo a resultados similares.

Schönfinkel (1924) desarrolló una teoría de funciones con el objeto de reducir el número de primitivas en un sistema como el presentado entre por Russell y Whitehead (1910 - 1913). En el sistema de Schönfinkel, que él llamó Funktionenkalkül (cálculo de funciones, en español), sólo hay una operación para formar términos complejos, que se escribe «fx», representa la aplicación de una función f a un argumento x, y se define para todos los términos. Para trabajar con funciones de más de un argumento, Schönfinkel empleó un método ya usado por Gottlob Frege (1891), para reducir funciones de más de un argumento 93

a funciones de un argumento. Este método supone ampliar la idea de función para que las funciones puedan ser argumentos y valores de otras. Entonces, es posible pasar el valor de cada función g para algún argumento x, como argumento a otra función f. Para esto, se usa una notación donde es común escribir «fxyz» para «((fx)y)z». Si Fxy es una función F de dos argumentos x e y, se reemplaza por una función f de un argumento tal que fa es la función de y dada por Fay, y fab es Fab. Por ejemplo, si Fxy es x – y, entonces f 2 = 2 – y, y f 2 3 = 2 – 3 = – 1. Esta operación que permite eliminar funciones de diverso número de variables se llama aplicación. Schönfinkel introdujo varios operadores para representar la aplicación de una función a sus argumentos y los llamó combinadores, porque forman combinaciones como funciones de las variables que contienen. Schönfinkel introdujo cinco combinadores: I, C, T, Z, S (que luego fueron formulados en la lógica combinatoria de Curry (1967) como respectivamente: I, K, C, B, S) y mostró que las fórmulas lógicas podían expresarse sin variables por medio de S y K (S y K en el sistema de Curry).

A finales de la década de 1920, Haskell B. Curry, como él mismo lo comenta en Curry (1967, pags. 20 – 21), realizó investigaciones que lo llevaron a lo que en esencia sería el mismo sistema de Schönfinkel: leyendo los Principia de Whitehead y Russell, notó que en la lógica proposicional habían dos reglas, el modus ponens, que era muy simple en su estructura formal, y una regla de substitución de cualquier fórmula por una variable proposicional, que era compleja. Seldin (1998a) afirma que a mediados de 1920, Curry decidió tratar de dividir esta regla de substitución en reglas más simples y que, luego, en 1926 encontró que podía hacerlo con un formalismo que en esencia era el mismo que el de Schönfinkel, y lo llamó lógica combinatoria. Al método de tratar funciones de más de un argumento en términos de funciones de un argumento, usado por Frege y que Curry tomó 94

de Schönfinkel, se le llamó ‘curryng” (currificación), en honor al trabajo realizado por Curry en su lógica combinatoria.

De forma independiente y casi simultáneamente al trabajo de Curry, Alonzo Church se propuso construir una modificación del sistema de Frege en la que se evitara el uso de variables libres. Según Seldin (1998a), una de sus metas fue que toda combinación de símbolos perteneciente a nuestro sistema, si representa una proposición, representará también una proposición particular sin ambigüedad y sin la adición de explicaciones verbales. También propuso evitar paradojas de la teoría de conjuntos y de la lógica restringiendo la ley del tercero excluido, siguiendo en esta restricción a la tendencia intuicionista de Brouwer. Church adoptó el tratamiento de funciones de Frege que ya hemos mencionado, como la estrategia de formación básica de este sistema, en el sentido de que los términos fueran formados a partir de variables usando dos operaciones: (1) Aplicación: denotada por «MN» como en los trabajos de Schönfinkel y Curry, que representa la aplicación de una función M a un argumento N y que está definida para cualesquiera dos términos M y N (2) Abstracción: denotada por «λx.M» y definida en el sistema original de Church para cualquier término M y para cualquier variable x que aparezca libre en M.

El sistema de Church también contenía la implicación. Las reglas de inferencia de Church eran dos: la regla  y la regla β. La regla  permitía la substitución de variables: los términos que difieren sólo en los nombres de sus variables ligadas están identificados en el nivel sintáctico, de manera que λx.x = λy.y. 95

Las variables ligadas son aquellas sobre las que actúa el operador λ; por ejemplo, en λx.xy, x es una variable ligada e y una variable libre. La regla β era empleada para el cálculo de valores de una función: (λx.M)N puede ser reemplazada por el resultado de sustituir x por N en M.

Como en Curry, en el sistema de Church las conectivas lógicas pueden ser reemplazados por constantes atómicas.

Como resultado de la definición de las operaciones de aplicación y abstracción, tenemos que la teoría de Church también tenía combinadores y, por tanto, coincidía en muchos aspectos con las investigaciones de Schönfinkel y Curry. La relación exacta entre las teorías de Curry y la de Church quedó establecida por Rosser (1935), un discípulo de Church, en su trabajo de tesis, A Mathematical Logic without variables. Para establecer esta relación, Rosser construyó una teoría de combinadores que era equivalente a la de Church. Luego mostró que una teoría reforzada de la conversión lambda, que es el proceso de transformar fórmulas del sistema de Church por la aplicación de sus reglas de inferencia, es equivalente a la teoría sintética de Curry. Desde entonces quedó claro que una teoría de combinadores puede ser expresada como una teoría de la conversión lambda y viceversa, como señala Curry (1967, pag. 28). Podemos coincidir entonces con Feys y Fitch (1980, pag. 90) cuando afirman que el cálculo lambda pertenece a la lógica combinatoria, entendida ésta como el estudio de los procesos de aplicación y de abstracción de funciones.

Church (1936) demostró luego, basándose en un teorema sobre las propiedades del cálculo lambda, que siempre que consideremos un sistema equivalente a la lógica de predicados de 96

primer orden, tomado en su totalidad, es imposible resolver el problema de la decisión. Como resultado de un trabajo de representación de la aritmética en el sistema original de Church, Stephan Kleene (1936), discípulo de Church, había descubierto una gran cantidad funciones que pueden ser representadas por términos lambda. Puesto que un término lambda que representa una función calcula sus valores usando un procedimiento mecánico (reducción aplicando la regla β), cualquier función que pueda ser representada por un término lambda debería ser efectivamente calculable, es decir, calculable siguiendo un procedimiento mecánico. Estos resultados llevaron a Church a la conjetura de que las funciones efectivamente calculables de números naturales pueden ser representadas por términos lambda. Esta conjetura es el origen de la famosa Tesis de Church, publicada en Church (1936), en el marco de su demostración de que hay problemas irresolubles de la teoría elemental de números. La forma más usual de esta tesis es que todas las funciones efectivamente computables son recursivas parciales, y es una consecuencia de una prueba en Kleene (1936) de que una función es recursiva si y sólo si puede ser representada por un término lambda.

Para su demostración, Church (1936) plantea el problema de la decisión en término del problema de los invariantes de conversión, que grosso modo puede ser planteado de la siguiente manera: dadas dos fórmulas cualesquiera Y1 e Y2 de un algún sistema como el cálculo lambda ¿es posible determinar de manera efectiva si Y1 se puede convertir Y2 o no?. La respuesta positiva a esta cuestión nos daría un procedimiento efectivo para determinar un sistema completo de invariantes de conversión, es decir, de fórmulas que permanecen invariantes respecto de toda conversión. Sin embargo, Church concluye que no existe un sistema completo de invariantes de conversión que sea efectivamente calculable. Para ello 97

comienza aplicando el método de aritmetización de Gödel (1931) al cálculo de conversión lambda. Este método permite realizar una codificación que asocia a cada fórmula bien construida de un sistema formal un número, llamado número de Gödel, de manera tal que dos expresiones bien formadas no pueden tener asociado el mismo número de Gödel. Luego, identifica la noción de calculabilidad efectiva con la noción de función recursiva general (Church, 1936, pag. 347): […] esta definición de calculabilidad efectiva puede ser establecida en dos maneras equivalentes, (1) que una función de enteros positivos será efectivamente calculable si es definible en el cálculo lambda […], (2) que una función de enteros positivos será llamada calculable efectivamente si es recursiva (Church, 1936, pag. 347).

Al hacer equivalentes las funciones calculables efectivamente con las funciones recursivas, Church podrá vincular la recursión con el problema de la decisión: para cualquier función recursiva de enteros positivos hay un algoritmo con el cual cualquier valor particular requerido de la función puede calcularse efectivamente” (Church, 1936, pag. 351). Define algoritmo como: un método por el cual, dado cualquier número entero n, puede obtenerse una secuencia de expresiones (en alguna notación) En1, En2, … Enr; donde En1 es efectivamente calculable cuando se da n; donde Eni es efectivamente calculable cuando se dan n y las expresiones Enj, j < i; y donde, cuando se dan n y todas las expresiones Eni hasta incluir Enr, el hecho de que el algoritmo haya terminado llega a conocerse efectivamente y el valor de F(n) es calculable efectivamente (Church, 1936, pag. 356).

98

Church (1936, pag. 351) define una función recursiva proposicional de enteros como una función recursiva cuyo valor es 2 o 1 dependiendo de si la función proposicional es verdadera o falsa. Entonces plantea el problema siguiente: hallar una función recursiva F de dos argumentos tal que de F Y1 Y2 (donde Y1 Y2 son los números-G correspondientes a los términos Y1 e Y2 respectivamente) sea 2 o 1 según que Y 1 sea convertible en Y2 o no. Este problema es equivalente al de encontrar una función recursiva G de un argumento que dependa de un número-G de una fórmula Y3, tal que el valor de G Y3 sea 2 o 1 según que Y3 tenga una fórmula normal o no. Una fórmula del cálculo lambda tiene forma normal si es una fórmula bien formada y no contiene ninguna parte de la forma λx(M)N y B es la forma normal de A si B está en forma normal y A es convertible en el cálculo lambda a B. Cuando un término está en forma normal, no se le puede aplicar la reducción β.

Finalmente Church demuestra el teorema siguiente, el teorema XIII del artículo: Dada una fórmula Y1, no existe función recursiva G de un argumento tal que el valor de G Y1 sea 2 o 1, según que Y 1 tenga una forma normal (Church, 1936, pag. 360). Es decir, la propiedad de ser una fórmula en forma normal no es recursiva. De lo que se sigue el teorema XIX del artículo: No hay función recursiva de dos fórmulas Y1 e Y2, cuyo valor es 2 o 1 de a cuerdo a si Y1 es convertible en Y2 (Church, 1936, pag. 363)

Como corolario a este teorema, Church establece que el Entscheidungproblem es irresoluble en un sistema formal que sea ω-coherente en sentido fuerte y que permita ciertos procedimientos simples de definición y demostración, como el sistema de Principia 99

Mathematica6: En un sistema como éste, sería expresable la proposición acerca de dos enteros positivos a y b que son representaciones gödelianas (números de Gödel) de fórmulas A y B tal que A es inmediatamente convertible en B. Ya que la conversión en el cálculo lambda es una secuencia finita de conversiones β intermedias inmediatas, la proposición ψ(a, b) expresaría que a y

b son representaciones

gödelianas de fórmulas A y B tal que A es convertible en B. Además si A es convertible en B y a y b son representaciones gödelianas de fórmulas A y B respectivamente, la proposición ψ(a, b) podrá ser demostrada en el sistema, a través de una demostración que afirma exhibir, en términos de representaciones gödelianas, una secuencia finita particular de conversiones inmediatas que conduce de A a B; y si A no es convertible en B, la ω-consistencia del sistema significará que ψ(a, b) no es demostrable en él. Si el problema de la decisión para el sistema fuera resoluble, habría medios para determinar efectivamente si cualquier proposición ψ(a, b) se puede demostrar y, por lo tanto, habría algún medio para determinar efectivamente para todo par de fórmulas A y B si A es convertible en B, lo que estaría en contradicción con el teorema XIX 7 (Church 1936, pag. 363). De esta manera Church prueba que hay clases de la forma P(n) para cada número natural n tal que no hay un algoritmo general que, dado n, produzca una solución para P(n). No hay 6

7

Supongamos que Λn es una variable sintáctica para expresiones de n-ésimo tipo y expresiones correspondientes a propiedades del n-ésimo tipo; Θ es una variable sintáctica para variables individuales; ΛK es una variable para proposiciones indecididibles cuya existencia es demostrada gracias a la teoría de predicados de Kleene. Un sistema formal L de segundo orden que incluye constantes individuales que corresponden a enteros, es ω-coherente en sentido fuerte si para todo predicado Λ 2 [predicado de orden 2] de L se da que: si las proposiciones (E Θ) Λ 2 (Θ) [Existe algún individuo Θ, tal que tiene la propiedad de segundo tipo Λ] es derivable en L, al menos una de las proposiciones ~ Λ 2K [El predicado de segundo tipo Λ indecidible en el sistema de Kleene] no es derivable en L. El teorema XIX, que ya hemos citado arriba, dice textualmente: No hay función recursiva de dos fórmulas A y B cuyo valor es 2 o 1 de acuerdo a si A es convertibe en B o no. Dado que una función recursiva suministra un procedimiento efectivo, este teorema plantea que no es posible dar un procedimiento efectivo para decidir si una fórmula A es convertible en otra B.

100

pues algoritmo que decida si una formula dada del cálculo de predicados de primer orden es un teorema, un resultado que coincide con los de Turing, (1936).

Ya hemos comentado que Turing (1937), demostró que una función numérica puede ser computada por una máquina de Turing si y sólo si es recursiva parcial. También Turing demostró que las funciones computables por una máquina de Turing son idénticas a las funciones lambda-definibles de Church y a las funciones recursivas generales debidas a Herbrand y Gödel y desarrolladas por Kleene. Estos resultados le permitieron a Turing (1937) afirmar la posibilidad de reemplazar las 'máquinas' que generan funciones computables por definiciones “más convenientes” en el cálculo lambda. Podemos entonces pensar que la definibilidad lambda representa una manera particular de definir la computabilidad que, como hemos visto, tiene un fundamento aún más abstracto que el de Turing: una operación matemática precisamente llamada “abstracción”.

2.3.- Maquinas de Turing y cálculo lambda Turing y Church, casi simultáneamente e independientemente uno de otro, demostraron que cualquier operación computable por una máquina de Turing puede expresarse usando expresiones del cálculo lambda de Church, y viceversa.

En Kleene (1936) llegó a los siguientes resultados: 1. Toda función recursiva primitiva es recursivamente general. 2. Toda función recursiva general es lambda-definible 3. Toda función lambda-definible definida para todos los sistemas de sus valores de 101

sus argumentos es recursiva general.

Basado en teorema de Kleene (1938) sobre recursividad parcial, Church enunció el teorema siguiente: Toda función parcialmente recursiva es lambda-definible y viceversa.

Alan Turing (1937) estableció 1. Toda función lambda-definible es computable. 2. Toda función computable es recursiva general.

Por consiguiente, las siguientes nociones son equivalentes: (a) Función recursiva general. (b) Función computable. (c) Función lambda-definible, para todos los sistemas de valores de sus argumentos.

También se da la equivalencia entre: (a) Función parcialmente recursiva. (b) Función lambda-definible (sin restricción).

De acuerdo a la tesis de Church, la clase de las funciones recursivas parciales pueden ser computadas por cualquier dispositivo que ejecute procesos algorítmicos. Las funciones computables por máquinas de Turing son iguales a las funciones recursivas parciales. Si una máquina de Turing no puede resolver un problema, entonces ningún dispositivo mecánico de cómputo puede hacerlo, porque no existe ningún algoritmo ni procedimiento 102

para obtener su solución. Las limitaciones de indecidibilidad para el cómputo de funciones no son de orden tecnológico, sino intrínsecas a limitaciones esenciales de los procesos computacionales. No importa cuán poderosa sea una computadora en cuanto a memoria y velocidad de ejecución de sus operaciones, no existe la posibilidad ni el procedimiento para computar ciertas clases de funciones.

2.4.- Reglas del cálculo lambda El cálculo lambda es un formalismo para expresar funciones. Trabaja con un conjunto de símbolos cada uno de los cuales representa una operación matemática o función, cuyos “argumentos” son otras cosas del mismo tipo, es decir, funciones. Una función al actuar sobre otra, da como resultado o “valor” una nueva función. Por ejemplo, al escribir: a = bc decimos que a es el resultado de hacer que la función b actúe sobre la función c. A la acción de una función sobre sus argumentos la llamamos aplicación.

Además de la aplicación, Church propuso otro tipo de operación para su cálculo: la abstracción, designada por la letra griega λ. Para expresar la abstracción de una función, se coloca la letra λlambda y se le hace seguir inmediatamente por la letra que representa una de las funciones, por ejemplo x, que llamamos “variable muda”; luego seguirá un punto y después una expresión, donde cada aparición de la variable x se tratará como un “espacio” (placeholder) en el que puede sustituirse cualquier cosa que siga a la expresión completa, después del segundo corchete. Podemos entonces escribir: λx.fx para expresar la función que, al actuar sobre un objeto, como s, produce como resultado fs: 103

(λx.fx)a = fa.

Podríamos decir que la abstracción es una operación para nombrar de forma precisa una función en sí misma. Entendiendo función como una correspondencia por la que a cada elemento x de un conjunto X se hace corresponder un único elemento y de un conjunto Y, encontramos que hay dos significados para la expresión de funciones “f(x)”: 1. La función misma, en tanto que la correspondencia entre los elementos de un conjunto X y los elementos de un conjunto Y. 2. El valor de la función:, un miembro y del conjunto Y, cuando x es un objeto de un dominio X, o un valor ambiguo de la función, si no está especificado el valor de x.

Mediante la notación para la abstracción lambda, se puede representar la función f como distinta de su valor ambiguo. En este sentido, la expresión λx.[fx], es simplemente un nombre para la función f: λx.fx = f. Vemos que cuando se aplica el operador lambda a una forma funcional como fx, se aísla la función de sus argumentos, dando como resultado el nombre de la función asociada a la forma. Tenemos entonces que mientras una expresión como (x + 1) designa el sucesor de x, en cambio la expresión λx (x +1) designa la función sucesor en sí misma.

Llamamos conversión lambda a una serie finita de aplicaciones de las operaciones del cálculo lambda, que son aplicación y abstracción. Si una fórmula Y puede obtenerse por conversión, a partir de otra fórmula Z, decimos que Y es convertible en Z. La 104

convertibilidad es una relación simétrica, reflexiva y transitiva, y el cálculo lambda se dedica al estudio de las propiedades de la conversión lambda.

Una expresión está expresada en forma normal si está bien construida y no contiene ninguna parte de la forma (λx.[Y])Z, donde las variables ligadas de Y son distintas de las variables ligadas de Z. En una expresión en forma normal no es posible aplicar a ninguna de sus partes la operación de reducción.

Las funciones de números enteros que se pueden representar mediante el cálculo lambda se denominan funciones lambda-definibles: Una función de enteros f de una variable es lambda-definible si se puede encontrar una fórmula Y del cálculo lambda tal que si fa = b y si a y b son las fórmulas del cálculo lambda que representan los enteros a y b, respectivamente, la expresión lambda Ya es convertible en b.

El cálculo de la conversión lambda está en correspondencia con el cálculo de valores de una función según el esquema: fa Ya

– cálculo → – conversión →

b b

Hay, pues, como lo presenta (Ladrière, 1965, pag. 205), una correspondencia donde Y corresponde a f, a corresponde a a, y Ya o b corresponden a fa o b.

El alfabeto del cálculo lambda está constituido por: Símbolo para la operación de abstracción: 105

Símbolos para variables: a, b, c, …, z y las mismas letras con índices, por ejemplo: a0, a1, ... Símbolos auxiliaries: De agrupación: paréntesis: ), (. De separación: .

Convenciones para variables y términos: Los términos del cálculo lambda se llaman términos lambda; M, N,... son símbolos sintácticos para términos lambda; en todo caso M, N, … son expresiones del metalenguaje para referir términos cualesquiera. x, y, z,... son símbolos sintácticos para variables lambda arbitrarias. ‘=’ es un símbolo del metalenguaje denota igualdad sintáctica. M  N denota que M y N son el mismo término o que N puede ser obtenido a partir de M mediante un cambio de nombre en las variables ligadas en M.

Reglas de formación: Los términos lambda son definidos inductivamente: Toda variable es un término. Si M, N son términos, entonces MN también lo es, Si M es un término y x una variable, entonces λx.M es un término.

Convenciones de asociación: 106

Asociación a la izquierda: M1 M2 M3 ... Mn se reserva para ((...(M1 M2) M3) ... Mn) ; Asociación a la derecha: λx1, x2,...xn.[M] se reserva para λx1 (λx2 (...(λxn M))...).

Variables libres Intuitivamente, una variable aparece libre en un término M si x no está en el “alcance” de λx; si es de otra manera, x aparece ligada. El conjunto de variables libres de un término lambda M, que expresaremos con la notación FV (M), que significa “Free Variables of M” o variables libres de M, se define inductivamente por las siguientes reglas Barendregt y Barendsen (2000, pag. 10): FV (x)

=

{x};

FV (MN)

=

FV(M)  FV(N);

FV (λx. M)

=

FV(M) – {x}.

M es un término lambda cerrado o combinador si FV (M) = conjunto vacío.

Reglas de transformación: Regla de sustitución o regla alfa ‘=α’ Los términos que difieren sólo en los nombres de sus variables ligadas están identificados en el nivel sintáctico, así que: λx. M =α λy. [y/x]M. donde ‘[y/x]’ indica la sustitución de x por y. Este cambio de nombre, que expresamos por el símbolo “=α”, es lo que llamamos conversión alfa. Esta regla tiene la restricción de que y no puede aparecer libre en M, pues el caso libre de y en M resultaría ligado una vez hecha la sustitución. Por ejemplo si M fuera xy, tendríamos: 107

λx. xy =α λy. yy lo que nos daría una expresión cuyos dos lados no tienen el mismo sentido. A este fenómeno se le llama colisión de variables.

Regla de reducción o regla beta ≥ β Toda expresión que representa una aplicación, que tiene la forma (λx. f x) M, puede ser reemplazada o reducida a la fórmula f M: (λx. f x) M ≥ β f M A esta transformación

se le conoce como reducción beta (β) y la

expresaremos usando el símbolo “≥ β”.

Regla de expansión o abstracción beta ‘≤ β’ M [x/N] denota el resultado de sustituir toda aparición libre de la variable x en M por el término N. Una expresión de la forma M [x/N] puede ser reemplazada por una fórmula con la forma (λx. M) N, siempre que las variables ligadas de Y sean distintas de x y de las variables de N: M [x/N] ≤ β (λx. M) N Usaremos el símbolo ≤ β para representar la expansión beta.

Representaremos tanto la reducción beta como la expansión o abstracción beta por el símbolo “= β” que significará lo que llamaremos conversión beta.

M [x/N] denota el resultado de sustituir toda aparición libre de la variable x en M por el término N. Una expresión de la forma M [x/N] puede ser reemplazada por una 108

fórmula con la forma (λx. M) N, siempre que las variables ligadas de M sean distintas de x y de las variables de N: M [x/N] ≤ β (λx. M) N Usaremos el símbolo ≤ β para representar la expansión beta.

Representaremos tanto la reducción beta como la expansión o abstracción beta por el símbolo ‘= β’ que significará lo que llamaremos conversión beta.

Conversión lambda “λ” Se denomina conversión lambda a una serie finita de aplicaciones de estas tres reglas: conversión α, reducción β y abstracción β. Si una fórmula puede obtenerse por conversión lambda, decimos que esa fórmula es lambda convertible. Expresaremos la convertibilidad en el cálculo lambda usando el símbolo ‘λ’; entonces la expresión: M λ N significa “M es convertible a N por aplicación de las reglas de conversión del cálculo lambda”.

Forma Normal en el Cálculo Lambda Una fórmula está expresada en forma normal si está construida de acuerdo a las reglas de formación del cálculo y no contiene ninguna forma del tipo (λx. M) N, siendo las variables ligadas de M distintas de las variables de N. Esto significa que una fórmula está en forma normal si no es posible aplicarle la regla de reducción beta. 109

El resultado de sustituir N por las apariciones libres de x en M que, como dijimos al explicar la regla de expansión, se expresa por la notación M [x / N], se define por los siguientes esquemas, tomados de Barendregt (2000, pag 10). x [x / N]

=β

N;

y [x / N]

=β

y, si x  y;

M1 M2 [x / N]

=β

(M1 [x / N]) (M2 [x / N]);

(λy. M1) [x / N]

=β

λy. (M1 [x / N]).

Caracterización de la conversión lambda Si asumimos aquí la convención de usar el símbolo  para significar “implica”, podemos caracterizar la conversión lambda por los siguientes esquemas axiomáticos y reglas: () λx. M =α λy. [y/x]M

(Conversión alfa)

() (λx. M)N λ M [x / N]

(Reducción beta)

() M  λ M

(Reflexividad)

()M λ N

 N λ M

(Simetría)

() M λ N, N  λ L

 M λ L

(Transitividad)

(≤) M λ N

 ZM  λ ZN

(Monotonía de la aplicación 1)

(≤) M λ N

 MZ  λ NZ

(Monotonía de la aplicación 2)

() M λ N

 λx.M  λ λx.N

(Monotonía de la abstracción o regla )

Barendregt y Barendsen (2000) llaman a las reglas ,  y  reglas de igualdad y a las reglas ≤, ≤ y  reglas de compatibilidad. Como puede observarse, la convertibilidad lambda λ, que es una generalización de la conversión alfa, la reducción beta y la

110

expansión beta, es una relación de equivalencia, pues satisface las propiedades reflexiva, simétrica y transitiva.

Combinadores Ya hemos visto que Schöfinkel (1924), interesado en eliminar variables de la lógica, introdujo un tipo de operadores llamados combinadores, los cuales “representan combinaciones como funciones de las variables que contienen (tal vez junto con otras variables)” (Curry y Feys, 1967, pag. 24). Tales combinaciones se forman a partir de las variables y por medio de una operación postulada en correspondencia a la aplicación de una función a un argumento. El siguiente lema (&), tomado de Barendregt (2000, pag. 1) permite representar combinadores por letras simples: en el cálculo lambda podemos demostrar (λx1, …, xn. M) y1 … yn  M [x1 / y1] … [xn / yn]. Prueba: Por el axioma 1, la reducción beta, tenemos: (λx1. M) y1  λ M [x1 / y1] Entonces el lema (&) se sigue por inducción sobre n. Si definimos los siguientes combinadores [Barendregt, 12]: I



λx. x;

K



λxy. x; 111

(&)

K*



λxy. y;

S



λxyz.xz(y z).

Como puede observarse, a cada combinador simple hay asociada una regla de reducción. Esto significa que cuando el combinador es aplicado a una serie finita de variables obtenemos una combinación que se reduce a una determinada combinación de tales variables. Tal reducción se seguirá del lema (&): IM



M;

K MN



M;

K* M N



N;

SMNL



M L (N L).

Tenemos aquí que I es el operador más sencillo, el cual expresa una variable como función de sí misma. A este combinador se llama identificador elemental. El combinador K expresa un término M como función de N, mientras que K* expresa un término N como función de M.

A estos dos combinadores se les llama

canceladores elementales. El combinador S permite expresar dos términos M y N (que podrían ser dos funciones f y g) que dependen de un mismo término L (que podría ser una variable x). Schöfinkel (1924) demostró que las fórmulas lógicas pueden expresarse sin variables por medio de S y K.

112

Teoremas Church – Rosser Los teoremas de Church y Rosser (1936) demuestran la consistencia del cálculo lambda . El siguiente teorema, conocido como el teorema Church–Rosser I, responde de forma afirmativa a la cuestión de si hay más de una estrategia de reducción que conduzcan a la misma forma normal: Para cualquier expresiones lambda E, F y G, si E → F y F → G, hay una expresión lambda Z tal que F → Z y G → Z (Slonneger, 1995, pag. 153). Corolario: Para cualquier expresiones lambda E, M, y N, si E → N, estando M y N en forma normal, M y N son variantes una de otra. Esto significa que M y N serían equivalentes por reducción alfa. El siguiente teorema, llamado teorema Church – Rosser II, responde a la pregunta de si ¿hay una estrategia de reducción que garantice que se produzca una expresión en forma normal? Para cualquier expresiones lambda E y N, si E → N, estando N en forma normal, hay un orden normal de reducción de E a N (Slonneger, 1995, pag. 154). El orden normal de reducción siempre reduce primero la primera fórmula betareducible que está en el extremo izquierdo (Slonneger, 1995, pag. 152). El orden normal de reducción puede tener una de los siguientes resultados: 1. Alcanza una sola expresión en forma normal. 2. Nunca termina.

113

Como sólo existe una forma normal única para una reducción que conduzca a una forma normal, el cálculo lambda es consistente. Sin embargo, no hay algoritmo o procedimiento mecánico para determinar si alguna expresión lambda va a producir algunos de los dos resultados mencionados (Slonneger, 1995, pag. 154).

Funciones lambda-definibles Se llaman funciones lambda-definibles a las funciones de números enteros que se pueden representar en el cálculo lambda. La tesis de Church, según la cual las funciones efectivamente computables sobre enteros positivos son las funciones lambda definibles, supone que en el cálculo lambda hay una manera de definir enteros positivos. Además, para definir funciones binarias necesitamos definir un constructor y un selector. Dado que muchas funciones emplean definiciones de condicional, también necesitamos definir constantes y operaciones booleanas [Slonneger, 1995, pag. 156].

Numerales de Church Recordemos que en el cálculo lambda estamos interesados en un universo de objetos denotados por variables, cada uno de los cuales representa una operación matemática o función. En este cálculo podemos formar expresiones a partir de las operaciones elementales del sistema, aplicación y abstracción. Por ejemplo, la expresión:

114

λf. f(fx), es la función que cuando se aplica a una función g, produce g aplicada dos veces sobre x: (λf. f(fx) g λ g (gx) También podemos aplicar la expansión lambda o abstracción a λf. f(fx) y obtener: (λf. f(fx) λ λf. λx. f(fx) λ λfx. f(fx) Es la función que aplicada sobre g, produce g aplicada sobre sí misma, o “g iterada dos veces”. Church empleó este tipo de construcciones para definir números enteros a través del cálculo lambda. De hecho, la función λfx. f(fx) identificaría el número natural 2 A los números naturales definidos por este procedimiento se le llaman numerales de Church: 0 = λfx. x 1 = λfx. fx 2 = λfx. f(fx) 3 = λfx. f(f(fx)) 4 = λfx. f(f(f((fx))) etc. Cualquier aplicación de estas expresiones lambda sobre una función arbitraria f hace iterar esta tantas veces como lo indica el numeral. Por ejemplo, la aplicación de 3f sobre y sería: 115

(3f)y λ f(f(f(y))). La función sucesor, la función adición aritmética, la función multiplicación aritmética y la función potencia se expresan en el cálculo lambda respectivamente así: Suc = λn f x. f (n f x)

Sucesor

Add = λm n f x. m f (n f x)

Adición

Mul = λm f x. m (f x)

Multiplicación

Pot = λm f. m f

Potencia

Apliquemos la función sucesor a 2: Suc 2 λ

(λn f x. f (n f x)) 2

λ

λf n. f (2 f x)

λ

λf n. f (λg y. g (g y) f x)

λ

λf n. f (λ y. f (f y) x)

λ

λf n. f ( f (f x)) = 3

Constructor y selector A continuación presentamos la representación en cálculo lambda de una función para

construir pares,

que llamaremos

par. También

presentaremos

las

representaciones de dos funciones binarias selectoras, fst (first: primero) y snd 116

(second: segundo), que se corresponden a los combinadores que ya presentamos K y K*, respectivamente: par := x y f. f x y fst := p.p (x y.x) snd := p.p (x y.y) Aquí empleamos el símbolo ‘:=’ para significar ‘… se define como …’

Veamos un ejemplo que ilustra como operan estas funciones: fst par p q λ

(p.p (x y.x) a b f. f a b) p q

λ

(a b f. f a b (x y.x)) p q

λ

( b f. f p b (x y.x)) q

λ 

 f. f p q (x y.x)

λ

(x y.x) p q

λ 

(y.p) q

λ 

p

Con estas funciones simples, podemos definir otras compuestas. Como ejemplo crearemos la función swap: swap := z. snd z fst z swap par p q

λ 

(z. snd z fst z) ((x y f. f x y) p q)

λ 

(z. snd z fst z) ( f.f p q)

λ 

(z. snd z fst z) p q

λ 

(snd p q) (fst p q) 117

λ 

(p.p (x y.y) p q) (p.p (x y.x) p q))

λ 

(p.p ( y.y) q) (p.p (x y.x) p q))

λ 

(p.p q) (p.p (x y.x) p q)

λ 

(p.p q) (p.p ( y.p) q)

λ 

(p.p q) (p.p p)

λ 

q (p.p p)

λ 

qp

Constantes y operaciones booleanas Para expresar los valores verdad (True) y falso (False) en cálculo lambda usamos: T = λt. λf. t F = λt. λf. f El condicional podemos expresarlo de la siguiente manera. Si B es una expresión que evalúa verdad o falsedad, es decir, si es un booleano, entonces test: Si B entonces P sino Q Puede ser representado por: test := λc. λx. λy.c x y donde: test T v w = λc. λx. λy.c x y) T v w λ T v w λ λ v

λt. λf.t) v w

118

2.5.- El cálculo lambda con tipos: origen y reglas. Church (1940) donde presenta una versión del cálculo lambda que incluía asignación de tipos para los términos lambda. Curiosamente, este sistema con asignación de tipos para los términos del cálculo lambda ha facilitado el descubrimiento de la correspondencia entre demostraciones lógicas y programas, conocida como isomorfismo Curry-Howard. El objetivo de Church con este cálculo era dar una fórmulación de la teoría de tipos simple, sugerida independientemente por Leon Chwistek y F. P.Ramsey como una alternativa a la teoría ramificada de tipos de Russell y Whitehead, que incorporara ciertos rasgos de la conversión lambda.

El cálculo lambda y el uso de tipos tienen su origen común en la lógica. Posiblemente la primera noción de tipos se encuentra ya en Frege (1891), donde se revela la diferencia conceptual entre objetos y predicados y se consideró la jerarquía que se construía sobre estas nociones: en el nivel inferior tenemos una colección de objetos básicos, luego tenemos las propiedades de estos objetos, después tenemos propiedades de estas propiedades.

Russell y Whitehead (1910 – 1913) introdujeron la teoría ramificada de tipos como una manera de evitar una paradoja descubierta en el sistema originalmente ofrecido por Frege (1893) como fundamentación de la aritmética, conocida como paradoja de Russell. Originalmente, Church pensó que era posible evitar esta paradoja sin introducir tipos, pero sólo manteniéndose dentro de una lógica intuicionista que use solamente alguna forma limitada de la ley del tercero excluido. Sin embargo, dos estudiantes de Church, Kleene y 119

Rosser (1935), demostraron que este sistema es inconsistente. Church (1940) presentó luego una formulación de lógica usando el cálculo lambda con asignación de tipos simples, que puede concebirse como una simplificación del sistema de tipos usado en Principia Mathematica.

Una teoría de tipos supone que en un sistema simbólico no sólo tratamos con objetos, como términos, fórmulas y demostraciones. También tratamos con tipos de objetos.

El cálculo lambda con asignación de tipos incluye tipos generados a partir de una base tipo 0 usando una "flecha" (→) para representar un espacio de función A → B, un número infinito de variables de cada tipo y términos lambda construidos a partir de variables y las operaciones de aplicación y abstracción. Las fórmulas de este cálculo son ecuaciones entre términos del mismo tipo. Los axiomas y reglas de inferencia son las versiones restringidas de las reglas de transformación del cálculo lambda sin asignación de tipos.

El sistema de Church tenía dos tipos atómicos: para el tipo de proposiciones, para el tipo de individuos.  Los tipos compuestos son del tipo de funciones desde  a  β, que ahora generalmente se denota como «→  β», pero que Church denotaba  «( β )». Las “funciones (proposicionales) de primer orden” de Russell corresponden a términos del tipo →, sus “funciones (proposicionales) de segundo orden” corresponden a términos del tipo (→) → o, etc.

En general, los tipos son objetos de naturaleza sintáctica y pueden ser asignados a términos 120

lambda. Si M es un término del cálculo lambda y se le asigna un tipo , entonces decimos ‘M tiene tipo ’; la denotación que usaremos para esto es M : . Si M es una función, entonces tendrá un tipo de función de la forma → β, y lo denotaremos M : → β8.

Curry llama argumento al término lambda M en una expresión de la forma M : , y llama predicado a la parte que representa el tipo en una expresión con esta forma.

Los tipos vienen a solucionar también un cuestionamiento que se hacía al cálculo lambda: los términos del este cálculo no representaban la noción de función tal como los matemáticos acostumbraban a usar en la teoría de conjuntos, la cual incluye un dominio y un rango dados como parte de la definición de función (Hindley y Seldin, 1996, pag. 159) En este sentido, cada tipo atómico α denota un conjunto particular, como el conjunto de los números naturales, y cada tipo compuesto, de la forma α→β, que se denota alguna función de α a β, representa funciones cuyo rango es un conjunto denotado por α y cuyo rango es un subconjunto denotado por β. A lo que refieran exactamente los tipos atómicos o el conjunto de funciones definidas por tipos compuestos dependerá en todo momento dependerá siempre del uso para el cual está destinada la teoría de tipos formal que se va a desarrollar. Cuando se especifica, por ejemplo, un conjunto de funciones, como las funciones representables en algún modelo dado, todo tipo va a denotar un conjunto de individuos o funciones específicos. Más allá de esto, los tipos son simples objetos sintácticos.

La inclusión de tipos en un sistema lógico como medio para evitar paradojas se debe a que ellos, al definir algún conjunto para algún término o al establecer un dominio y un rango 8

Church empleaba superíndices para la asignación de tipos, de manera que si M es un término de tipo  escribía: M α; y si M es una función de tipo → β, se escribía M → β.

121

para un conjunto de funciones, limitan la información de los términos. Por ejemplo, a través de la asignación de tipos a términos se pueden poner restricciones a la operación de aplicación: para aplicar M a N, el tipo de N debe ser  y el tipo de M debe ser → β; entonces la aplicación MN tendrá el tipo β. En el caso de la abstracción, si x es una variable de tipo y M es un término de tipo β, entonces el término x.M, que denota una función, tendrá el tipo → β.

En el caso de los combinadores, tenemos que, por ejemplo, el identificador simple I, definido por la expresión x.x, designa una función que proyecta o asocia consigo mismo un término de tipo , por lo tanto: I: ( → ). Esto significa que si x es el argumento de I y x tiene el tipo , entonces el valor I x es de tipo .

En general, tenemos que:  → β es el tipo de funciones del tipo  al tipo β.

La expresión “x1 : β 1, …, xn : β n ├ t : ”, es un juicio sobre tipos, donde se dice que t tiene el tipo  si cada xi tiene el tipo βi. Usaremos letras griegas mayúsculas, como Γ y Δ, para designar listas de pares “variable : tipo”, a las que llamaremos contextos. Así que si, en la expresión “x1 : β 1, …, xn : β n ├ t : ” hacemos x1 : β 1, …, xn : β n= Γ, podemos decir también la expresión “Γ ├ t : ” significa que t tiene el tipo  en el contexto Γ, donde el contexto Γ no es sino una secuencia de términos lambda con tipos asignados con la forma “xi : β i”.

122

El cálculo lambda con asignación de tipos, tal como lo concibió Church (1940), incluye dos reglas de transformación o inferencia: una introduce la flecha de tipos y otra la eliminarla. Entonces enunciamos las reglas de inferencia siguientes para el cálculo lambda con asignación de tipos: (1) regla de abstracción: Si Γ, x:α ├ M : βentonces Γ├ (λx.M):α→ β, si x no aparece libre en  (2) regla de aplicación: Si M:α→ β y N:α, entonces MN:β.

Como puede notarse, la regla de abstracción introduce flecha de tipos y la regla de aplicación la elimina. Se podrá notar que hay una similaridad estructural con las reglas propuestas por Gentzen (1934) para el fragmento implicacional del cálculo de deducción natural, es decir, el cálculo lógico que sólo incluye dos reglas de inferencia para el implicador, una que lo introduce y otra que lo elimina. Esta circunstancia permite expresar en el estilo de la deducción natural las reglas del cálculo lambda con asignación de tipos.

Usemos ahora usemos letras latinas mayúsculas para designar tipos. Enunciemos la regla de aplicación en el cálculo lambda con tipos: Sea t una función ‘de tipo B a tipo A’ bajo las suposiciones en el contexto Γ; y sea u un término ‘de tipo B’ bajo las suposiciones en el contexto Δ. Podemos concluir entonces que t(u) es un término de tipo A bajo la combinación de las suposiciones en los contextos Γ, Δ. Expresada formalmente: 123

Γ ├ t: B →A Δ├ u :B Γ, Δ ├ t(u) : A

(→ E)

Enunciemos ahora la regla de abstracción: Sea t un término ‘de tipo B’ bajo las suposiciones en el contexto Γ; y sea u un término ‘de tipo A’ bajo las suposiciones en el contexto Δ. Podemos concluir entonces que λx.t es un término de tipo B → A bajo la las suposiciones en el contexto Γ. Expresada formalmente: Γ, t : B Δ ├ u : A Γ ├ λx. t : B → A

(→ I)

Algunas versiones del cálculo lambda con tipos incluye explícitamente el siguiente axioma: ___________ Id x :A├ x :A que expresa la reflexividad de las expresiones en este cálculo. Este esquema es equivalente al siguiente, si se considera que en él se tomó el contexto Δ como vacío: Id Δ, x : A ├ x : A Entonces, si tomamos a Γ = Δ, x : A, podemos plantear el esquema Id de la siguiente forma: Id Γ ├ x :A si y sólo si (x : A) está en el contexto Γ .

Tenemos entonces una regla para términos que son variables, la regla que hemos llamado Id. Las demás reglas, aplicación y abstracción, actúan sobre funciones. De estas reglas, una, 124

la abstracción, introduce el tipo de funciones y la otra, la aplicación, lo elimina. Por este motivo designamos estas dos reglas por (→ I) y (→ E), respectivamente. Reglas del cálculo lambda con tipos de Church ____________ x :A├ x :A Id Γ, x : B Δ ├ t : A Γ ├ λx. t : B → A

Γ ├ t: B →A Δ├u:B Γ, Δ ├ t u : A →I

→E

A partir de estas reglas puede decidirse si a algún término corresponde cierto tipo en este cálculo. Como ejemplo, efectuaremos tres demostraciones para tipos cualesquiera A, B y C. Demostraremos primero que para el tipoA que la siguiente expresión es válida en este cálculo: (λx. x ) : A → A Demostración: (x: A) ├ ( x: A) ├ (λx. x ) : A → A

(Id) (→I)

Demostremos ahora que la siguiente expresión pertenece al cálculo lambda con tipos: (λx y. x ) : A → B → A Demostración: (x: A), (y: B) ├ ( x: A) (x: A) ├ (λy . x) : (B → A) ├ (λx y. x ) : A → B → A

(Id) (→I) (→I)

Finalmente, demostraremos la expresión más compleja: (λx y z. x z (y z) ) : (A → B → C) → (A → B) → (A → C)

125

Demostración: x : (A → B → C) ├ x : (A → B → C) z : A ├ z : A y : (A → B) ├ y : (A → B) z : A ├ z : A x : (A → B → C), z : A ├ x z (B → C) y : (A → B), z : A ├ y z : B x : (A → B → C), y : (A → B), z : A ├ x z ( y z ): C x : (A → B → C), y : (A → B) ├ λz. x z ( y z ): (A → C) x : (A → B → C) ├ λyz. x z ( y z ) : (A → B) → (A → C) ├ λxyz. x z ( y z ) : (A → B → C) (A → B) → (A → C)

Nótese que las expresiones que hemos demostrado aquí, si le suprimiéramos los tipos asignados, tendríamos las definiciones de los combinadores: I



λx. x;

K



λxy. x;

S



λxyz.xz(y z).

Lo que quiere decir que a estos combinadores corresponden los siguientes tipos: I

:

A→A

K

:

A→ B →A

S

:

(A → B → C) → (A → B) → (A → C)

Curiosamente, puede notarse que las expresiones a la derecha de los dos puntos ( : ), son muy similares formalmente a los esquemas axiomáticos del fragmento implicacional de la lógica proposicional estilo Hilbert que presentamos en el primer capítulo: los tipos correspondientes a K y S son estructuralmente idénticos a los esquemas H 1 y H2, respectivamente. Es esta similaridad estructural la que estudiaremos en el siguiente capítulo: pareciera que los términos lambda fueran el cómputo o la construcción efectiva de demostraciones del cálculo proposicional.

126

Veamos ahora que ocurre con los tipos de los términos del cálculo lambda cuando se aplican las conversiones propias de este cálculo. La conversión en el cálculo lambda con asignación de tipos, que representaremos aquí con el signo ‘ ΛΠ’, queda caracterizada por los siguientes esquemas y reglas, que encontramos en Hindley y Seldin (1996, pag. 162): () (λx. M ) : A → B ΛΠ λy. [y : A / x : A] M : B () ( (λx. M ) : A → B ) N : A ΛΠ [N : A / x : A] M : B () M : A ΛΠ M : A () M : A ΛΠ P : A ├ (N : A → B) M : A ΛΠ (N : A → B) P : A () M : A → B ΛΠ P : A → B ├ (M : A → B) N : A ΛΠ (P : A → B) N : A () M : B ΛΠ P : B ├ (λx. M : B ) : A → B ΛΠ (λx. P : B ) : A → B () M : A ΛΠ N : A, N : A  P : A ├ M : A ΛΠ P : A

Como en el cálculo lambda sin inclusión de tipos, se denomina redex (reducible expresión, en español, expresión reducible) a toda expresión de la forma: ( (λx. M ) : A → B ) N : A

Por ejemplo, la reducción de la expresión (λ x.xz : A → B) y : A, que aplica una función M del tipo A → B, definida por xz, a un término N de tipo A, definido por y, nos da, por la regla (la expresión yz : B. Esto tiene una particular importancia en al deducción de tipos, pues una deducción de la forma: x:A├x:A · D1(x) · M:B

(→I)

(λx. M ) : A → B (λx. M ) N : B

D2 · N:A

(→I)

· 127

D3

Se reduce a la forma: D2 N :A · D1(N) · [N / x : A] M : B

· D’3

Donde D’3 se obtiene a partir de D3 reemplazando las apariciones de (λx. M )N por [N/x] M.

Al hacer este paso de reducción ocurre una contracción en el sujeto (el término lambda M en la expresión M : A). Además, si suprimimos todos los sujetos de ambas deducciones, veremos que este paso de reducción se corresponde con el paso de reducción de la implicación en el cálculo de deducción natural, tal como expusimos en el primer capítulo de este trabajo en el apartado sobre normalización. Obsérvese que en la primera derivación, el punto donde ocurre lo que sería equivalente a la fórmula de corte en un desvío en una derivación en deducción natural, aparece aquí una expresión reducible con la forma: ( (λx. M ) : A → B ) N : A

Todas las propiedades de la conversión lambda del sistema sin asignación de tipos se mantienen en el sistema con asignación de tipos. Pero, además, los sistemas con asignación de tipos tienen una propiedad extra que no tienen los sistemas sin tipos, y que juega un rol esencial en todas sus aplicaciones: las expresiones con tipos asignados son normalizables en sentido fuerte. Quiere decir que para este sistema con tipos vale el siguiente teorema: En el cálculo lambda con tipos no hay reducciones- infinitas. A diferencia de lo que ocurre en el cálculo lambda sin tipos, donde es posible encontrar 128

estrategias de reducción de un término t dado que no conduzcan a una forma normal, en el cálculo lambda con asignación de tipos todas las estrategias de normalización son buenas, en el sentido de que siempre conducen a una forma normal y, por lo tanto, siempre terminan. El problema en el cálculo lambda sin tipos es que, a pesar de que en él para todo término siempre hay alguna estrategia de normalización, el procedimiento de reducción no es un algoritmo determinista, siendo posibles muchas conversiones para un mismo término t dado. Si la normalización débil nos da un procedimiento para elegir en cada paso una expresión reducible apropiada que ha de conducir a una forma normal, es decir, un término u que es irreducible, en el caso el cálculo lambda con tipos la normalización para cualquier término t dato es fuerte, pues no hay secuencia de reducción infinita que comience con este término t. Por supuesto, esta propiedad del cálculo lambda con tipos tiene relevancia desde el punto de vista del problema de la detención, que mencionamos al comienzo de este capítulo.

Se atribuye a Tait (1967), la demostración de que la reducción beta en el cálculo lambda con tipos es fuertemente normalizable. Girard (2003, pags. 31 – 45) también presenta una versión de la demostración del teorema de normalización fuerte para el cálculo lambda con tipos también basada en la noción de reducibilidad empleada por Tait. Esta demostración de normalización fuerte debería extenderse al fragmento implicacional de la lógica intuicionista por la correspondencia Curry-Howard.

Ya hemos visto que existen similaridades estructurales entre la lógica proposicional y el cálculo lambda con asignación de tipos:

129

1. El tipo que corresponde a los combinadores I, K y S son similares a los axiomas del fragmento implicacional de la lógica proposicional estilo Hilbert. 2. La reducción beta de una expresión del cálculo lambda con tipos se similar a la reducción o contracción del desvío o eliminación de un corte en una derivación en el cálculo de deducción natural a través del paso de reducción para →.

No es de extrañar que los investigadores comenzaran a señalar estas correspondencias entre el cálculo lambda con asignación de tipos y los sistemas de lógica proposicional. Una de las primeras observaciones al respecto, y que ya hemos señalado aquí, las encontramos en Curry (1967, pag. 388): existe correspondencia entre el los tipos asignados a términos lambda y las fórmulas en un sistema axiomático de lógica intuicionista proposicional, estilo Hilbert. En esta correspondencia, los términos lambda se corresponderían con las demostraciones de las fórmulas de la lógica intuicionista. Posteriormente, después que Dag Prawitz (1965) demostrara los teoremas de forma normal y de normalización para el cálculo de deducción natural estilo Gentzen, Howard (1969) estableció la existencia de la correspondencia entre el cálculo lambda con asignación de tipos y el cálculo de deducción natural para la lógica intuicionista, no sólo para el fragmento implicacional de la lógica de primer orden, sino también para la lógica de primer orden, destacando también la correspondencia entre reducción de demostraciones y reducción lambda; a estas correspondencias se le conocen en la actualidad como isomorfismo Curry-Howard o principio de fórmulas-como-tipos.

Como veremos en el siguiente capítulo, por este isomorfismo, entre otras cosas, podemos usar el cálculo lambda con asignación de tipos como una notación natural para las 130

demostraciones en el cálculo de deducción natural: el cálculo lambda con tipos representa una manera natural de codificar las demostraciones del cálculo de deducción natural. Además, por este isomorfismo, los resultados del cálculo lambda pueden ser traducidos a un marco de demostraciones de deducción natural. Considerando que los cómputos que se hacen en el cálculo lambda se corresponden con algoritmos, se pueden ver programas como demostraciones, donde su especificación (lo que el programa debe hacer) sería como el teorema probado por la demostración, y la ejecución de un programa sería como la normalización de una demostración.

131

III. Correspondencia Curry-Howard Al final de la década de 1960, varios investigadores encontraron a través de investigaciones independientes que, respecto al cálculo lambda con asignación de tipos y la lógica proposicional intuicionista, es posible considerar los tipos asignados a los términos lambda como fórmulas del cálculo proposicional y a los términos lambda como un registro de las demostraciones de esas fórmulas. Uno de los trabajos que introdujeron esta idea de fórmulas como tipos fue el ya mencionado de Curry y Feys (1967), obra publicada originalmente en 1958 y que descubre que si se identifica el tipo de una función, expresado por la fórmula A → B, con la implicación, las fórmulas derivables en la presentación axiomática al estilo Hilbert del fragmento implicacional de la lógica intuicionista, coinciden con los tipos de la lógica combinatoria. Un trabajo posterior, Howard (1969), pero publicado en 1980, observa que la coincidencia observada por Curry (1967) se verifica también entre el cálculo lambda con tipos y el cálculo de deducción natural, estilo Gentzen, para la lógica intuicionista; que además la correspondencia se extiende hasta la lógica de primer orden y que la reducción beta de términos del cálculo lambda y la normalización de pruebas en el cálculo de deducción natural para la lógica intuicionista de primer orden. Howard extendió la correspondencia entre el fragmento implicacional de la lógica proposicional intuicionista y el cálculo lambda con tipos hasta hacer corresponder este cálculo con la aritmética intuicionista de primer orden, como informa Soresen (1998, pag. 72).

Al mostrar la correspondencia entre el proceso de reducción beta del cálculo lambda y el proceso de normalización en el cálculo natural intuicionista, Howard demostró que la relación entre estos dos sistemas no es una mera biyección entre fórmulas y tipos: la 132

correspondencia entre los sistemas mencionados es un isomorfismo, por lo tanto, ambos sistemas satisfacen las mismas propiedades formales. Dado que el trabajo de Curry fue uno de los primeros conocidos sobre el tema y como el Howard es uno de los más considerados, a la correspondencia entre el cálculo lambda con tipos y la lógica proposicional intuicionista frecuentemente se le llama «isomorfismo Curry – Howard».

En suma, el isomorfismo Curry - Howard establece que hay una correspondencia entre el cálculo de deducción natural para la lógica proposicional intuicionista y el cálculo lambda con asignación de tipos. Gracias a esto, dada una derivación de tipos en el cálculo lambda, se puede construir la demostración correspondiente en el cálculo de deducción natural, y viceversa. Esta correspondencia es tal que la reducción beta de términos lambda se halla en correspondencia con la normalización de demostraciones en el cálculo de deducción natural. Como ocurre cuando se descubre la existencia de isomorfismo entre sistemas, que es una coincidencia fuerte en sus estructuras matemáticas, esta correspondencia ha abierto interesantes perspectivas en el campo de la lógica, la matemática y la computación. Según Etayo (1971, pag. 132), desde el punto de vista matemático, decir que dos cosas son isomorfas equivale a decir que son la misma cosa. Esta identidad refiere a las relaciones existentes entre los objetos formales de cada sistema. Dado que los objetos en un sistema abstracto, Como observa Kleene (1974, pag. 34), se conocen a través de sus relaciones, entonces encontrar correspondencia entre sistemas a nivel de las relaciones que determinan sus objetos es como hallar que esos sistemas son equivalentes.

Un isomorfismo indica identidad estructural: “El isomorfismo es como un diccionario en el que no solamente a cada palabra de un idioma corresponde una única palabra en el otro, 133

sino también la construcción gramatical fuese la misma” (Etayo, 1971, pag. 132). Que exista isomorfismo entre el cálculo lambda con tipos y la lógica intuicionista puede interpretarse, por ejemplo, como que el cómputo de una función a través del cálculo lambda, que equivale a la ejecución de un programa por una computadora, es estructuralmente equivalente a una demostración en la lógica proposicional intuicionista, que corresponde a la deducción de un teorema.

También puede considerarse la sintaxis del cálculo lambda con tipos como una forma apropiada de caracterizar la noción de consecuencia de la lógica intuicionista, que daría pie a una lógica constructivista, tal como lo demuestra, por ejemplo, el sistema de tipos de Martin-Löf (1972).

3.1. Breve historia Como vimos en el primer capítulo, Gentzen (1934) demostró el llamado Hauptsatz o teorema del corte para el cálculo de secuentes, que establece que, en este cálculo, cualquier enunciado que posea una demostración haciendo uso de la regla del corte, posee una demostración libre de corte, es decir, una demostración que no hace uso de la regla del corte. Se trata del teorema de la forma normal para el cálculo de secuentes, el cual permite comprobar la propiedad de subfórmula en este cálculo y demostrar, como un corolario, la consistencia de este cálculo y de sus equivalentes, como el cálculo deducción natural. Prawitz (1965) presenta métodos para simplificar en forma directa demostraciones en el cálculo de deducción natural: se trata de reducir cualquier deducción hecha en el cálculo natural a una deducción en forma normal, que es una deducción sin desvíos y conduce a la 134

misma conclusión que la demostración original. Este método de reducción se formuló en forma de un teorema que hemos llamado teorema de normalización de Prawitz. Unos años después, Prawitz (1971) demostró que toda secuencia de reducción de una demostración en deducción natural siempre termina, una propiedad conocida como normalización fuerte.

Curry (1958) notó que si, en el cálculo lambda con tipos, los términos son suprimidos y la flecha que designa la correspondencia que define el tipo de una función, es interpretada como una implicación, entonces los esquemas axiomáticos para los combinadores básicos se convierten en los esquemas axiomáticos bien conocidos para el fragmento condicional de la lógica proposicional intuicionista, formándose de hecho un conjunto completo de esquemas axiomáticos para esta lógica, y la regla para eliminar la flecha de tipos se convierte en la regla del modus ponens (Curry, 1967, pags. 388 – 391). Este hecho ya lo hemos visto en la presentación que hicimos en el segundo capítulo del cálculo lambda con asignación de tipos. Curry además notó que había una correspondencia similar entre una formulación del fragmento condicional positivo del cálculo de deducción natural intuicionista y el cálculo lambda con tipos (Curry, 1967, pags. 392 – 397) e incluso llegó a proponer un sistema para el fragmento condicional positivo del cálculo de secuentes y una versión del con términos del cálculo lambda con tipos (Curry, 1967, pags. 397 – 404): Curry llegó a extender la correspondencia entre fórmulas y tipos al cálculo de secuentes.

Tait (1967) probó que la reducción beta en el cálculo lambda con asignación de tipos es fuertemente normalizable, es decir, toda fórmula de este cálculo es reducible a una expresión en forma normal y este proceso siempre será finito. Tait notó que, cuando se

135

analiza la teoría T de Gödel de funcionales computables de tipos finitos 9, dado que los combinadores pueden ser expresados como términos lambda, la demostración normalizante de una proposición, al eliminar los cortes, corresponde al cómputo de términos lambda asociados a una forma normal. Para esta demostración, Tait usó como método la noción de reducibilidad, lo cual le permitió dar una definición de igualdad definicional de términos con tipos asignados en términos de reducibilidad: dos términos son definicionalmente iguales si son reducibles al mismo término. Luego, Prawitz (1971) usará una variante del método de la reducibilidad de Tait para probar la normalización fuerte de la deducción natural para la lógica intuicionista de primer orden.

Howard (1969) reúne los resultados de Prawitz (1965) y Curry (1958) para establecer la existencia de una correspondencia entre la simplificación de pruebas en la deducción natural y la reducción beta del cálculo lambda. El trabajo de Howard no fue publicado hasta 1980, en el libro en homenaje a los 80 años del profesor H. Curry. Sin embargo circuló una versión facsímil durante casi dos décadas, como informa Wadler (2000, pag. 10).

El isomorfismo Curry – Howard, respecto a los resultados de Tait (1967), implica que puede obtenerse una prueba de normalización fuerte para la deducción natural usando el método de la reducibilidad, lo cual coincide con los resultados de Prawitz (1971). Tenemos entonces que al representar demostraciones en el cálculo de deducción natural como ciertos 9

Gödel (1958) presenta su sistema T de orden mayor, que debía ampliar el punto de vista finito de la noción de demostración metamatemática de Hilbert con principios constructivos de inferencia más abstractos. Según Gödel, esto permitiría conseguir una demostración de la consistencia de la aritmética clásica. Es un sistema semejante a la aritmética recursiva primitiva, basada en un sistema de ecuaciones no cuantificadas: como explica Kleene (1974, pag. 203), estos sistemas se basan en un conjunto de esquemas operatorios que tienen forma de ecuaciones. Como sistema de orden mayor, las variables y funciones del sistema T no se refieren sólo a números naturales y funciones numéricas, sino también a funcionales (funciones que tienen funciones como parámetros) computables de cualquier tipo finito.

136

términos lambda, y al explotar el hecho de que los pasos de la normalización de una demostración se corresponden con los pasos de una reducción en cierto cálculo lambda con tipos, uno puede traducir propiedades de los términos lambda en términos de propiedades de demostraciones.

Constable (1971) sugirió, basado en el isomorfismo Curry-Howard, tratar el tipo α o la proposición A como representación de una especificación de lo que un programa hace y tratar cualquier demostración M de tal proposición A como un programa que satisface lo especificado por A. Para esto se usan las matemáticas constructivas como un lenguaje de programación para el desarrollo de métodos mecánicos para extraer programas de demostraciones.

La

extracción

es

empleada

como

una

técnica

para

generar

automáticamente programas con corrección verificada.

La correspondencia Curry – Howard, aunque ya no como un isomorfismo sino limitada a la asociación de fórmulas con tipos, fue extendida a la lógica clásica: Griffin (1990) muestra como que la Ley de Pierce, que no puede ser demostrada en la lógica intuicionista por su prohibición de usar el axioma del tercero excluido, se corresponde con las instrucciones de control de los lenguajes de programación funcional. De acuerdo con estas observaciones, las demostraciones clásicas poseen contenido computacional cuando se extiende la noción de computación hasta incluir acceso explícito al contexto de control actual de un procedimiento efectivo.

Girard (1971) ha extendido y empleado el isomorfismo Curry – Howard en pruebas de 137

normalización fuerte en lógica intuicionista de orden mayor.

Ya hemos visto que Curry (1958) planteó sistemas donde se hace hacen corresponder términos del cálculo lambda con fórmulas del sistema intuicionista del cálculo de secuentes. Gallier (1993) describe dos sistemas de asignación de tipos que están en correspondencia con el cálculo de secuentes LJ y su respectivo cálculo libre de cortes. Estos cálculos están en correspondencia con sus respectivos cálculos intuicionistas de deducción natural NJ. Dada esta relación, se puede ver el Hauptsatz como una consecuencia canónica del teorema de normalización para términos lambda con tipos asignados, lo que supone una aplicación teórica de la correspondencia Curry – Howard. Herbelin (1995) estableció una relación entre las derivaciones del cálculo de secuentes y los términos del cálculo lambda con tipos, extendido con operadores de sustitución explícita. Esto ha permitido aclarar cómo los términos lambda con operadores de sustitución explícita se encuentran a mitad de camino entre las derivaciones en el cálculo de secuentes y el cálculo lambda con tipos. Barendregt y Ghilezan (2000) muestran que, en virtud del isomorfismo Curry – Howard y la correspondencia entre el cálculo de deducción natural y el cálculo de secuentes, tal como la han demostrado Zucker (1974) y Ungar (1992), se pueden emplear los resultados del Hauptsatz de Gentzen (1934) en el estudio del cálculo lambda.

Stewart (1999) ha mostrado cómo situar la correspondencia Curry-Howard bajo una consideración de la semántica lógica, en el marco de la teoría de la demostración y a partir de los trabajos de Prawitz, con su principio de inversión para los cálculos de deducción natural estilo Gentzen, y de Michael Dummett, con su noción de armonía lógica. 138

3.2. Presentación Como hemos planteado reiteradamente, la correspondencia Curry-Howard establece que hay isomorfismo entre las reglas de derivación de tipos del cálculo lambda con asignación de tipos y la lógica intuicionista. Esto quiere decir que la computación de una función a través del cálculo lambda, que podemos considerar como un programa que computa un algoritmo determinado, es equivalente a una demostración de un teorema en el cálculo proposicional intuicionista. Una comprensión apropiada de la correspondencia requiere una definición de isomorfismo, el cual refiere a una relación de correspondencia entre sistemas de objetos o estructuras matemáticas.

3.2.1. Isomorfismo Puede verse la noción de estructura como un concepto referido a la organización constitutiva de un sistema de objetos. Según Kleene (1974, 33) un sistema S de objetos podría definirse como un conjunto no vacío, o clase o dominio no vacío D de objetos, entre los cuales se establecen ciertas relaciones. Por ejemplo, la secuencia de números naturales constituye un sistema del tipo (D, 0, ‘), donde D es un conjunto no vacío, 0 es un miembro distinguido (constante o invariable) de D, y ‘ es una operación unaria sobre un miembro de D, la operación sucesor. Otro sistema más simple podría definirse por (D, >), donde D es un conjunto de objetos y > es una relación binaria definida sobre D. Observemos que en estos sistemas no se especifica qué sean los objetos que conforman D, sólo hemos presentado tuplas que representan su constitución. Es la organización constitutiva de los sistemas expresada por dichas tuplas lo que aquí denominamos estructura. Así que, por 139

ejemplo, la tupla ( S, V, F, ¬, /\, \/, →, ↔) expresa la estructura de un sistema de lógica proposicional si consideramos a S como el alfabeto del sistema, V y F son dos constantes de S para los valores verdad y falsedad, ¬ es una función unaria, y el resto de los símbolos son funciones binarias. Otra forma de especificar la estructura de un sistema lógico proposicional podría ser (A, ├), es decir, un sistema formado por un conjunto A de fórmulas cerrado por una relación de deducción ├.

Llamamos a un sistema donde lo único que sabemos de los objetos es cómo se relacionan, sistema abstracto de objetos. Luego, si especificamos cuáles son los objetos de un sistema, diremos que esta especificación constituye un modelo o representación del sistema10.

Según Ebbinghaus (1996) en lógica matemática se puede hablar de una estructura 11 en un conjunto de símbolos S que determina un lenguaje de primer orden, como un par U = (A, a) con las siguientes propiedades: c) A es un conjunto no vacío, el dominio o universo de U. d) a es una correspondencia o proyección definida en S, que satisface: 1. para todo símbolo R de relación n-aria en S, a(R) es una relación n-aria sobre A. 2. para todo símbolo f de función n-aria en S, a(f) es una función n-aria sobre A. 3. Para toda constante c en S, a(c) es un elemento de A.

10

11

Al definir una interpretación para un sistema formal, estamos estableciendo las condiciones bajo las cuales los enunciados de ese sistema son verdad. De esta manera definimos la semántica del sistema. La noción de estructura en S, como explica Ebbinghaus (1996, pag. 29) se usa en la definición de la interpretación semántica de un lenguaje formal: una interpretación I de S es un par (U, B) que consiste en una estructura U en S y una asignación B en U. Siendo la asignación B una correspondencia que se establece entre el conjunto de variables de S y el dominio A de la estructura U.

140

La tupla que define un sistema nos da información sobre su estructura. Por ejemplo, podemos expresar dos sistemas de aritmética por las tuplas: Sar := { S, +, *, 0, 1} y Sar< := { S, +, *, 0, 1,