Download Texto - Academia Nacional de Ciencias de Buenos Aires

EL CENTENARIO DE GERHARD GENTZEN
(1909-2009)
Acto organizado
por el Centro de Estudios Filosóficos Eugenio Pucciarelli
y su Sección Lógica y Filosofía de las Ciencias
de la Academia Nacional de Ciencias de Buenos Aires,
el 22 de octubre de 2009
GENTZEN Y LA CONSISTENCIA DE LA ARITMÉTICA
JORGE ALFREDO ROETTI
Un objetivo central de la obra de Gerhard Gentzen fue demostrar
la consistencia de la aritmética en la versión de Peano. Esa demostración había fracasado parcialmente hasta comienzos de la década
de 1930. La tarea se facilitó en 1934-5, cuando Gentzen propuso los
cálculos clásico e intuicionista de deducción natural y sus correspondientes cálculos secuenciales, y demostró en ellos su teorema fundamental (Hauptsatz) o teorema de corte en varias formas. Ese teorema permitió demostrar sintácticamente la consistencia de la lógica
de primer orden, otras varias propiedades metateóricas y la consistencia de la aritmética de Peano sin el axioma de inducción, con un
método que recuerda al del teorema de Jacques Herbrand. Gentzen
amplió en 1936 esa demostración de consistencia de la aritmética de
Peano para ese sistema con axioma de inducción. Para ello usó un
principio de inducción transfinita, que fue luego discutido por algunos autores. Autores como Kurt Schütte y Paul Lorenzen remediaron más tarde las dificultades encontradas. Hoy podemos decir sin
exagerar que la obra de Gentzen es una de las más importantes en
la historia del conocimiento humano perfectamente fundado.
Los pasos fundamentales de esos resultados de Gentzen en los
cálculos secuenciales son los siguientes:
§ 01. Los desarrollos correctos de los cálculos secuenciales (una
presentación de la lógica creada por Gentzen) parten de ‘‘secuencias
originarias’’ de la forma A A y se desarrollan mediante reglas estructurales y reglas para constantes lógicas, en el antecedente y en
el sucedente –salvo en el caso de la regla de corte– hasta alcanzar la
secuencia final. Ellas son:
645
Reglas de desarrollo estructurales
En el antecedente.
En el sucedente.
Debilitamiento1 (Verdünnung o Abschwächung, thinning) D:
Γ Θ
(D) A, Γ Θ
ΓΘ
(D) Γ Θ, A
Contracción (Zusammenziehung o Kontraktion, contraction) C:
A, A, Γ Θ
Γ Θ, A, A
(C)
A, Γ Θ
(C) Γ Θ, A
Permutación o intercambio (Vertauschung, interchange o permutation) P:
∆, A, B, Γ Θ
Γ Θ, A, B, Λ
(P)
∆, B, A, Γ Θ
(P) Γ Θ, B, A, Λ
Corte (Schnitt, cut) S:
(S)
Γ Θ, M ,, M, ∆ Λ
Γ, ∆ Θ, Λ
2
Reglas de desarrollo para constantes lógicas.
En el antecedente.
En el sucedente.
A, Γ Θ
B, Γ Θ
(∧) A∧B, Γ Θ , A∧B, Γ Θ
Γ Θ, A
Γ Θ, B
()Γ Θ, A∨B , Γ Θ, A∨B
A, Γ Θ,,B, Γ Θ
(∨) A∨B, Γ Θ
Γ Θ, A,,
Γ Θ, B
(∧)Γ Θ, A∧B
F(a), Γ Θ
(∧) ∧xF(x), Γ Θ
Γ Θ, F(a)
(∨) Γ Θ, ∨xF(x)
1
La regla de debilitamiento en el antecedente se denomina también ‘regla de
monotonía’. Ésta vale en cálculos lógicos estrictamente demostrativos, incluso ampliativos, como los que admiten construcciones sintéticas a priori, por ejemplo pragmáticas. A la derecha damos los nombres alemanes e ingleses de las reglas.
2
Una variante de esta regla de corte es Γ > M ,, M, Γ > C
Γ>C
, versión que corresponde a los cálculos secuenciales intuicionistas, efectivos o constructivos.
646
Fa, Γ Θ
*(∨) ∨xF(x), Γ Θ
Γ Θ, F(a)
*(∧) Γ Θ, ∧xF(x)
Γ Θ, A,, B, ∆ Λ
(→) A → B, Γ, ∆ Θ, Λ
Γ Θ, A
(¬)
¬A, Θ
A, Γ Θ, B
(→) Γ Θ, A → B
A, Γ Θ
y
(¬) Γ Θ, ¬ A
Las reglas para el negador son simétricas. Esta forma del cálculo
se presenta como un ‘‘semiformalismo’’3.
§ 02. Las reglas del cálculo son de tal índole que, salvo la regla
de ‘‘corte’’ S o su equivalente de ‘‘mezcla’’ M, no hacen desaparecer en
la secuencia inferior ninguna secuencia que aparezca en las secuencias superiores o sea subfórmula en ellas. Por lo tanto se demuestra
fácilmente la:
Propiedad de las fórmulas parciales: En un desarrollo
secuencial sin corte (o mezcla), que parte de secuencias iniciales, todas las fbf.s de la deducción son fórmulas parciales de las fbf.s que
aparecen en la secuencia final4.
Es decir, en los desarrollos sin corte las fbf.s de una secuencia
nunca se tornan más simples hacia abajo: cuando se modifican, se
tornan más complejas. Gentzen llamó ‘‘deducción sin rodeos’’ a un
desarrollo con esta propiedad. En ellos las fórmulas parciales no
desaparecen: todas las expresiones que aparecen en alguna secuencia también aparecen en la secuencia final, como tales o como subfórmulas.
En consecuencia, si se puede demostrar que para cada desarrollo con corte existe otro equivalente –es decir con la misma secuenUna variante de esta regla de corte es Γ M ,, M, Γ C
ΓC
, versión que corresponde a los cálculos secuenciales intuicionistas, efectivos o constructivos.
4
Un ‘‘semiformalismo’’ (Halbformalismus o semi-formal system) es un sistema
de reglas en el que al menos una regla puede contener infinitas premisas. *(∨) y
*(∧) son reglas críticas: La variable propia a de las figuras de deducción (∨) y (∧)
no puede aparecer en la secuencia inferior de esas figuras de deducción (es decir, no
puede aparecer ni en Γ, ni en Θ, ni en F(x)). Esta restricción impide deducciones
incorrectas.
3
647
cia final– sin corte, significa que para cada desarrollo con rodeos
existe otro desarrollo equivalente ‘‘sin rodeos’’.
§ 03. El teorema fundamental (Hauptsatz)
Por razones de brevedad sólo presentamos los enunciados de las
dos formas principales del teorema fundamental o de corte. Largas
y elaboradas demostraciones se encuentran en cualquier exposición
de los cálculos secuenciales de Gentzen5. También hay presentaciones breves para los mismos sistemas presentados como cálculos de
diálogos lógicos en Lorenzen 1987 y otras. Los enunciados de estos
teoremas son:
Teorema fundamental: Todo desarrollo secuencial correcto se puede transformar en otro desarrollo secuencial correcto con la misma
secuencia final en el cual no se utiliza la regla de corte (S) (o la regla
de mezcla (M)). El caso del cálculo secuencial intuicionista es un
caso particular del teorema clásico.
Gentzen facilita la larga demostración usando la regla de mezcla (M)
en lugar de la regla de corte (S). Las reglas (S) y (M) son equivalentes.
Teorema fundamental para formas normales prenexas (o teorema fundamental ‘‘fortificado’’) para el cálculo secuencial clásico.
Sea un desarrollo en el cálculo secuencial clásico cuya secuencia
final ‘Sf’ sea tal que cada fbf. de esa secuencia final esté en forma
normal prenexa. El teorema fundamental fortificado demuestra que
ese desarrollo se puede transformar en otro equivalente con la misma secuencia final, pero que tiene las siguientes propiedades:
(1) el desarrollo equivalente cuya secuencia final ‘Sf’ no contiene ningún corte (S) o, lo que es equivalente, ninguna regla de mezcla (M);
(2) existe en el desarrollo una secuencia media ‘Sm’ tal que
(2a) su desarrollo carece de cuantores ‘∧’ y ‘∨’ y
(2b) a partir de Sm, y excluida ella misma, las únicas reglas de desarrollo que aparecen son (∧), (∧), (∨), (∨) y las reglas estructurales diferentes de la regla de corte (S).
5
Es el ‘‘suplemento al teorema fundamental’’ (Zusatz zum Hauptsatz): propiedad de las fórmulas parciales (Teilformeln-Eigenschaft). Cf. Gentzen 1934-5, 2.513,
195.
648
§ 04. La consistencia sintáctica del cálculo de predicados clásico
e intuicionista
El teorema de consistencia sintáctica de estos cálculos dice lo
siguiente: Los cálculos secuenciales intuicionista y clásico son consistentes respecto de la negación (es decir, ninguna secuencia final es de
la forma A∧¬A).
Dem. Procedemos por reducción al absurdo. Sabemos que es deducible la secuencia ‘A∧¬A ’, ya que es equivalente a la secuencia
‘ ¬(A∧¬A)’. Supongamos que fuese deducible la secuencia vacía ‘’.
Ella nos permitiría desarrollar por debilitamiento la secuencia
‘ A∧¬A’. Un desarrollo con corte para ella tendría el siguiente aspecto:
(*)
(*)
Hip.
A A ,, ¬A
A∧¬A ,,
AA
¬A, A A∧¬A, A A, A∧¬A A∧¬A, A∧¬A A∧¬A (¬)
(¬)
(∧)
(P)
(∧)
(C)
(S)
‘A’ es una fbf. de grado lógico cualquiera. Si fuera posible una
demostración de ‘’ mediante corte, entonces por el teorema fundamental debe haber otra demostración de ‘’ sin corte. Nos preguntamos entonces de qué secuencias puede surgir la secuencia nula sin
cortes. No puede surgir de ninguna de las restantes reglas estructurales, porque éstas, o bien aumentan el número de fbf.s por (D), o
bien cambian su orden por (P), o bien lo disminuyen por (C), pero
nunca lo reducen a cero. Tampoco puede surgir por ninguna de las
doce reglas de deducción para constantes lógicas, pues éstas introducen al menos una formula principal compleja en la secuencia inferior,
pero no eliminan fbf.s (por la propiedad de las fórmulas parciales
de la § 02). Por lo tanto no hay una deducción correcta de la secuencia ‘’ que le sea equivalente y carezca de cortes. Pero por el teorema fundamental, si no es deducible la secuencia ‘’ sin corte, tampoco
lo es con corte, y como sí es deducible la secuencia ‘A∧¬A »’, entonces no es deducible la secuencia ‘ A∧¬A’.
649
§ 05. La ley de tercero excluido en la lógica intuicionista
Luego de demostrar la consistencia de los cálculos lógicos clásico e intuicionista, demostraba Gentzen que las lógicas de enunciados
intuicionista y clásica son decidibles. A continuación daba algunos
resultados concernientes al tercero incluido, que es lo que consideraremos a continuación.
El principio de tercero excluido irrestricto sólo vale en casos especiales en la lógica intuicionista. Es decir, su justificación en ella no
es formal, sino material. La forma de tercero excluido formalmente
válida en la lógica intuicionista es:
¬¬(A∨A),
que se demuestra así:
A A
A A∨¬A
¬(A∨¬A), A A, ¬(A∨¬A), ¬(A∨¬A), ¬A
¬(A∨¬A), A∨¬A
¬(A∨¬A), ¬(A∨¬A), ¬(A∨¬A), ¬¬(A∨¬A)
(∨),
(¬),
(P),
(¬),
(∨),
(¬),
(C),
(¬).
La penúltima secuencia desarrollada, ¬(A∨¬A) , dice que ‘‘la
negación del tercero excluido implica lo falso’’, lo que equivale a decir que no se puede negar el tercero excluido, lo que es obvio, pues por
una equivalencia de De Morgan intuicionista demostrable, a saber
¬(A∨B) ↔ ¬A∧¬B, sabemos que ¬(A∨¬A) equivale a la contradicción
¬A∧¬¬A, que es no desarrollable en el sistema. El siguiente teorema
de indeducibilidad es crucial para la lógica intuicionista:
Teorema. La ley de tertium non datur A∨¬A no es deducible en la
lógica intuicionista.
650
Demostrar este teorema supone demostrar imposibilidad de desarrollar la secuencia A∨¬A para el caso general de cualquier fbf.
A con grado lógico G(A) ≥ 0. Comenzamos con el caso base de fbf.s A
con grado lógico G(A) = 0. La demostración se hace por raa.
Dem.: supongamos que existe un desarrollo secuencial intuicionista
para A∨¬A. Por el teorema fundamental existirá un desarrollo
equivalente de A∨¬A sin corte. En tal caso la última regla de deducción que se usó debe haber sido (∨), pues:
1. A∨¬A no puede haber surgido por (P), pues deberían haber dos
fbf.s en el sucedente de la secuencia final, ni por (C), pues ello supondría la existencia de al menos dos fbf.s en la secuencia superior
de la secuencia final. Pero estas dos posibilidades no son admisibles
en un sistema secuencial intuicionista. Tampoco puede haber surgido
por (D), pues entonces el final de la deducción se vería así:
A∨¬A,
Y sabemos que ‘’ no es deducible por la ya demostrada consistencia
del cálculo.
2. A∨¬A tampoco puede derivarse de las reglas para constantes
lógicas, pues en ellas, o bien el antecedente de la secuencia inferior
no es vacío (para las reglas (∧), (∨), (→), (¬), (∧) o (∨)), o bien
aparece una constante lógica diferente de ‘∨’ en el sucedente (para las
reglas (∧), (→), (¬), (∧) o (∨)).
Por lo tanto el final de un desarrollo sin corte debió ser uno de
los siguientes:
(I)
(II) A
(¬)
A
¬A
(∨).
A∨¬A
A∨¬A, (∨)
(Para que una disyunción A∨B sea intuicionistamente deducible es
preciso que, o bien A sea deducible, o bien B lo sea.) Consideremos ahora los dos casos:
(I) A, con G(A) = 0, no es una secuencia inicial. Pero A no puede ser
secuencia inferior de ninguna regla de deducción intuicionista, ni de
651
las estructurales (C) o (P), pues suponen al menos dos fbf.s en el
sucedente, ni de las para constantes lógicas. Por lo tanto sólo queda
(D), es decir el final de desarrollo siguiente:
(>D)
A
(>∨).
A∨A,
Pero por el teorema de consistencia la secuencia superior no es desarrollable. Por lo tanto A no es desarrollable. (Esto prueba además
el criterio de consistencia de Post, pues si A es una fbf. atómica, ella
sólo es desarrollable a partir de ‘’, pero como ya sabemos ‘’ no es
desarrollable.)
(II) A , con G(A) = 0, no es una secuencia inicial. Pero no pudo haber
sido secuencia inferior de ninguna regla de deducción intuicionista,
ni de las estructurales (D) o (P), pues suponen al menos dos fbf.s
en el sucedente, ni de las reglas para constantes lógicas, por lo que
el desarrollo sólo podría ser:
A, …, A ⯗
A, A (C),
A (C),
(¬),
¬A
(∨).
A∨¬A
Pero de ese modo no se llega nunca a una secuencia inicial A A. Por
lo tanto ¬A no es desarrollable. Esto equivalente a una forma débil
del criterio de consistencia de Post (la negación de una variable proposicional no es teorema); obviamente lo mismo se dice de ¬¬A. Por
lo tanto no es deducible el tertium non datur en el cálculo secuencial
intuicionista.
§ 06. La aritmética de Peano
Giuseppe Peano, uno de los padres del logicismo, redujo los números a expresiones de la lógica de predicados utilizando el predicado
monádico ‘C1a’, que leemos ‘a es cero’ (es decir, el objeto a tiene la
‘‘propiedad’’ cero), el predicado binario ‘P2ab’, que leemos ‘a = p(b)’ ó
‘a precede inmediatamente a b’ y el ternario ‘S3cab’, que leemos ‘c =
a+b’ ó ‘c es suma de a y b’. De este modo los números naturales se
652
pueden representar mediante esos predicados de la siguiente manera:
0
1
2
syss
n
C1a
syss
syss
⯗
syss
C1a∧P2ab
C1a∧P2ab∧P2bc
C1a ∧ P2ab∧P2bc∧…∧P2mn,
donde ‘syss’ abrevia ‘si y sólo si’.
En ese simbolismo los diez axiomas de Peano toman la siguiente forma:
Axiomas de igualdad
A1. ⵩x(x = x)
A2. ⵩x⵩y(x = y → y = x)
A3. ⵩x⵩y⵩z(x = y ∧ y = z → x = z)
(reflexividad),
(simetría),
(transitividad).
Axiomas del cero.
A4. ⵪x(C1x)
A5. ⵩x⵩y(C1x∧C1y → x = y)
(existencia),
(unicidad).
Axioma de infinitud.
A6. ⵩x⵪y(P2xy)
(infinitud).
Axiomas de buen orden.
A7. ⵩x⵩y(P2xy → ¬C1y)
A8.
A9.
⵩x⵩y⵩z⵩u(P2xy∧P2zu∧x=z → y=u)
⵩x⵩y⵩z⵩u(P2xy∧P2zu∧y=u → x=z)
Axioma de inducción.
A10. A(0)∧⵩k(A(k) → A(k’)) → ⵩x.A(x)
(el cero no sucede a ningún número),
(unicidad del sucesor),
(unicidad del predecesor).
(axioma de inducción finita)
De este conjunto P = {A1, …, A10} de axiomas de Peano no consideraremos en lo inmediato el axioma A10 de inducción finita, porque la demostración de consistencia de la aritmética de Peano con ese
axioma realizada por Gentzen en 1936 y su versión definitiva de
653
19386 tenía dificultades con los procedimientos de inducción transfinita que implicaba, que la hacían discutible, por lo que se debió esperar
algún tiempo antes de que fuera resuelta. Nuestro conjunto de axiomas
para el teorema siguiente será el conjunto disminuido A = {A1, …, A9}.
§ 07. La consistencia de la aritmética de Peano
sin el axioma de inducción
Para esta demostración es útil la siguiente definición:
Df. Una fbf. C es aritméticamente deducible sin inducción finita, si
se puede desarrollar en el cálculo secuencial clásico la secuencia Γ C,
con Γ ⊆ A = {A1, …, A9}.
Teorema. La aritmética de Peano sin inducción finita es consistente respecto de la negación, es decir, no existe una fbf. aritmética deducible que corresponda a una secuencia desarrollable de la forma
Γ A∧¬A.
Dem.: La demostración utiliza el teorema fundamental para formas
normales prenexas (o teorema de corte reforzado). En primer lugar
se demuestra que la siguiente regla simétrica es correcta:
Γ A∧¬A
Γ
La deducción de abajo hacia arriba es inmediata por (D). Puesto
que A∧¬A es deducible, esa deducción de arriba abajo depende de
la hipótesis Γ A∧¬A. A partir de ella se desarrolla Γ por corte,
como muestra el siguiente desarrollo:
A
¬A, A
A∧¬A, A
A, A∧¬A
A∧¬A, A∧¬A
Γ A∧¬A ,,
A∧¬A
Γ
(*)
(*)
Hip.
6
A
Gentzen 1936.
654
(¬)
(∧)
(P)
(∧)
(C)
(S)
Si la aritmética de Peano sin inducción finita fuera inconsistente, existiría al menos un desarrollo con la secuencia final Γ , con
Γ ⊆ A (recuérdese que Γ consta de axiomas de A que están en forma
normal prenexa).
Procedemos por raa. Supongamos que el sistema sea inconsistente y por lo tanto que exista un desarrollo correcto con la secuencia
final Γ , con Γ ⊆ A. Aplicando el teorema fundamental para formas
prenexas obtenemos un desarrollo con la misma secuencia final Sf Γ que tiene las siguientes propiedades:
1. No tiene cortes.
2. Existe una secuencia media Sm Γ’ cuya deducción no contiene
ningún cuantor, en la cual las fbf.s de Γ’ son esquemas no cuantificados de los axiomas, y a partir de la cual se desarrolla linealmente
Sf sólo mediante una sucesión de reglas (⵩), (⵪), (D), (C) y (P),
pues el sucedente es vacío y no hay otras reglas primitivas en esa
parte del desarrollo.
3. Mediante los cambios de nombre de variables libres que se requieran se asegura la corrección del desarrollo. Éste tiene además la propiedad de que la variable propia de cada regla (⵪) –que es la única
regla crítica de este desarrollo– aparece sólo en la línea de secuencias superiores a la de su aparición.
A partir de ese momento del desarrollo reemplazamos cada variable libre en todas sus apariciones por números naturales determinados del modo que indicamos más abajo. Con ello obtendremos
desarrollos que ya no serán desarrollos formales del cálculo secuencial clásico, sino aritméticos elementales. El reemplazo lo realizamos
de la siguiente manera:
1. Todas las variables libres que no aparecen como variables propias
de una (⵪) (e.d. las que contienen subfórmulas de reglas (⵩)), las
reemplazamos inicialmente por ‘0’ (luego progresaremos en la sucesión natural).
2. Consideramos la regla crítica en el antecedente, que es (⵪), y vemos sus apariciones desde la secuencia final Sf hacia arriba y reemplazamos su variable propia por un número en todas las apariciones
de los dos únicos axiomas que introducen esta regla, A4 o axioma de
existencia del cero y A6 o axioma de infinitud:
655
A4.
C10, Γ
⵪xC1x, Γ
A6.
(P2mm’), Γ ⵪y(P2my), Γ
⵩x⵪y(P2xy), Γ Esto se hace de la siguiente manera:
En A4 reemplazamos inicialmente el parámetro de la regla por 0 y
en A6 el segundo parámetro por un número m’ sucesor de m en la
construcción de los naturales (por supuesto, en su primera aparición
reemplazamos m por 0). En la línea inferior del desarrollo de (⵩) en
A6 se reemplaza m por la variable ligada x.
Este procedimiento se puede reiterar a partir de los casos iniciales de las funciones recursivas elementales, que son verdaderas en
cada uno de los casos por construcción.
Consideremos ahora el siguiente desarrollo transformado Γ’’ que hicimos de la secuencia media Sm Γ’ en este desarrollo. Por hipótesis su sucedente es vacío y todas las fbf.s de su antecedente tienen alguna de las siguientes formas.
i. o bien es C10, ó
ii. P2mm’, ó
iii. es una fbf. sin ningún cuantor ‘⵩’ en la que las variables propias
han sido reemplazados por números, que pueden comenzar por 0, y
que son instancias de los restantes axiomas.
Pero entonces, por mero cálculo con algunas de las funciones
recursivas primitivas de arriba, todas las fbf.s de las transformadas
Γ’’ son enunciados aritméticos sobre constantes numéricas verdaderos por construcción. Además las Sm transformadas
Γ’’ serán demostraciones aritméticas que sólo han empleado recursos de
la lógica de enunciados. Por lo tanto podemos afirmar que, si la aritmética de Peano sin axioma de inducción finita fuese contradictoria,
se podrían construir contradicciones a partir de enunciados numéricos todos verdaderos que son instancias de los axiomas A1-A9 usando sólo reglas primitivas del cálculo secuencial clásico7. Pero como ya
Como, por ejemplo 3 = 3, 4= 5 → 5=4, 3 = 4
→ 3 = 1, p(0,1), p(2,3)→¬C13, etc.
7
656
∧ 4 = 2 → 3 = 2, C10, C13 ∧ C11
sabemos, por teorema anterior, que el cálculo secuencial clásico es
consistente y por lo tanto, a fortiori, su fragmento de lógica de enunciados clásica también lo es, y además las fbf.s del antecedente Γ’’ son
constructivamente verdaderas.
Todo esto implica que no puede existir una secuencia media de
la forma Γ’’ , pues por las funciones recursivas primitivas se determina:
(1) que las fbf.s numéricas son constructivamente verdaderas;
(2) que sus compuestos con constantes lógicas enunciativas son también verdaderos;
(3) que son casos especiales de los esquemas de axiomas sin cuantores de la secuencia media Sm Γ’ .
Estas figuras de deducción enunciativas siempre pasan de fbf.s
verdaderas a conclusiones verdaderas, por lo que no pueden producir secuencias de la forma Γ’’ A∧¬A o, lo que es equivalente, Γ’’ .
La relación entre los casos de Γ’’ y la Sm Γ’ es de inducción
completa. Las funciones recursivas primitivas de arriba permiten
rechazar todos los casos particulares Γ’’ de los esquemas de axiomas que aparecen en Γ’ , que por el teorema fundamental para formas prenexas se habrían deducido sólo por medio de reglas de la
lógica de enunciados. Pero la lógica de primer orden es consistente.
Por lo tanto, por contraposición, así como no pueden existir secuencias Γ’’ , tampoco puede existir una secuencia de la forma Γ’ . En
consecuencia no puede existir una secuencia Γ , como decía nuestra
hipótesis para la raa. Esto equivale a decir que la axiomática de
Peano sin el axioma de inducción es consistente, demostración que
se funda en una reducción a la lógica de enunciados mediante el teorema fundamental reforzado y una demostración por inducción finita
dentro de ese fragmento de lógica, utilizando el teorema de no contradicción de la lógica de primer orden ya demostrado.
09. La consistencia de la aritmética de Peano
con el axioma de inducción
Dicha demostración se basa, como en el caso anterior, en la aritmética de funciones recursivas primitivas pero con un principio de
inducción transfinita sin cuantores hasta el ordinal ε0. Ése fue el
657
método que utilizó Gentzen. Dicho principio de inducción transfinita sin cuantores hasta ε0 dice que para cualquier fórmula A(x) sin variables ligadas vale la inducción transfinita hasta ε0, que es el primer
ordinal α, tal que ωα = α, es decir el supremo de la sucesión:
{
ω
}
sup ω ω , ω ω , ω ω ,... .
Este método tiene el inconveniente de que hay pasos de la demostración que no se reducen a operaciones de la aritmética elemental recursiva, como bien muestra Kleene, por lo que no todos lo
aceptan y por lo que no expondremos.
Otro método usa la llamada regla-ω (ω-Regel) en un semiformalismo pleno (vollständiger Halbformalismus), como hacen Kurt
Schütte y Paul Lorenzen. Para los detalles enviamos a la literatura
de esos autores. Dejamos aquí el desarrollo del tema.
Hay muchos resultados importantes conectados a estas demostraciones de Gentzen. Uno de ellos dice que todos los cálculos en los
que vale el teorema fundamental son consistentes.
También hay resultados curiosos. Es sabido que en los cálculos
de tipo Gentzen que evitan el corte, las demostraciones sin corte son
habitualmente más largas que las que tienen aplicaciones de la regla de corte. A veces son incluso mucho más largas. George Boolos
llegó a mostrar incluso que existe una fórmula que con ayuda del
corte se puede deducir en alrededor de una página, mientras que
escribir una deducción sin cortes de la misma duraría más que toda
la duración del universo. Por ello escribió un artículo titulado ‘‘Don’t
Eliminate Cut!’’.
Literatura
George Boolos, ‘‘Don’t Eliminate Cut!’’, Journal of Philosophical Logic 13
(1984), pp. 373-378.
Gerhard Gentzen, ‘‘Untersuchungen über das logische Schließen’’, Mathematische Zeitschrift 39 (1934) (reedición en Karel Berka & Lothar
Kreiser, Logik-Texte, Berlin, 1986).
Gerhard Gentzen (ed. M. E. Szabo), The Collected Papers of Gerhard
Gentzen, Amsterdam, 1969.
Gerrit Haas, Konstruktive Einführung in die formale Logik, 1984, ISBN
3411016280.
Lutz Heindorf, Elementare Beweistheorie, 1994, ISBN 3411171618.
Rüdiger Inhetveen, Logik, Eine dialog-orientierte Einführung, Leipzig,
2003, ISBN 3-937219-02-1.
658
Stephen Cole Kleene, Introduction to Metamathematics, Amsterdam,
Groningen, 1952.
Kuno Lorenz & Paul Lorenzen, Dialogische Logik, Darmstadt, 1978 (contiene la primera demostración en teoría de diálogos).
Paul Lorenzen, Metamathematik, Mannheim, 1962.
Paul Lorenzen, Lehrbuch der konstruktiven Wissenschaftstheorie, Zürich,
1987, Stuttgart, 2000, ISBN 3-476-01784-2.
Kurt Schütte, Beweistheorie, Berlin, Göttingen Heidelberg, 1960.
A. S. Troelstra & H. Schwichtenberg, Basic Proof Theory (Cambridge Tracts
in Theoretical Computer Science), Cambridge University Press, ISBN
0521779111.
CEF / CONICET, UNS
659
SEMÁNTICA DE GENTZEN
JAVIER LEGRIS
Gerhard Gentzen (1909-1945) fue uno de los lógicos más importantes del siglo XX. Sus sistemas de deducción natural y secuentes, su
célebre Hauptsatz, su demostración de la consistencia de la aritmética de 1936 y su análisis de procedimientos constructivos en matemática abrieron nuevos caminos para la lógica matemática, de riqueza
metodológica y filosófica. En este trabajo paso revista a las ideas
semánticas que están en la base de su distinción entre reglas de introducción y eliminación para las constantes lógicas, y describo cómo esas
ideas han sido desarrolladas posteriormente en la teoría general de la
demostración, añadiendo algunas observaciones filosóficas.
I
En su artículo ‘‘Investigaciones sobre la deducción lógica’’, resultado de su trabajo de doctorado en Göttingen, Gentzen presenta su
sistema de deducción natural, cuyas reglas permiten la introducción
y eliminación de cada una de las constantes lógicas. Inmediatamente
después Gentzen se ocupa del ‘‘sentido contentual’’ (inhaltliche Sinn,
es decir, el significado) de las reglas del sistema, y en la sección 5 observa:
‘‘Las introducciones representan, por así decirlo, las ‘definiciones’
de los símbolos en cuestión, y las eliminaciones son, a final de cuentas,
tan sólo consecuencias de aquéllas. Esto puede expresarse del modo
siguiente: en la eliminación de un signo, podemos usar aquella fórmula, de cuyo signo principal nos estamos ocupando, únicamente ‘como
aquel que tiene significado sobre la base de la introducción de ese signo’ ’’ (Gentzen 1934-1935, p. 189).
Tómese por ejemplo la regla del modus ponens, que expresa la
eliminación del condicional material. La idea es que esta regla pue661
de aplicarse porque responde a la respectiva regla de introducción,
la llamada regla de ‘‘demostración condicional’’ o ‘‘condicionalización’’. Gentzen sugiere aquí una concepción que se articuló más tarde en una corriente dentro de la filosofía de la lógica. Según esta
corriente, las reglas de introducción dan el significado de los símbolos
lógicos, de modo que tienen un valor semántico. En la medida en que
estas ‘‘definiciones’’ se entiendan como elucidaciones, conduce a una
formulación del significado de las constantes lógicas y, por lo tanto,
a una semántica.
Franz von Kutschera introdujo la expresión ‘‘semántica de
Gentzen’’ en su trabajo ‘‘La completitud del sistema de los operadores {¬, ∧, ∨, ⊃} para la lógica de enunciados intuicionista en el marco de la semántica de Gentzen’’ (Kutschera 1968). La denominación
‘semántica’ se entiende aquí ‘‘en el sentido más general de la palabra,
que se aplica a investigaciones que se ocupan de la interpretación de
expresiones, especialmente de operadores lógicos, y no en el sentido
estricto de las investigaciones en teoría de modelos’’ (Kutschera 1968,
p. 47, n. 1). Esta semántica queda justificada por las siguientes razones:
‘‘Desde un punto de vista constructivo la semántica conjuntística
resulta insuficiente, ya que se toman en consideración cualesquiera
valuaciones de las fórmulas atómicas con los valores de verdad, y no
sólo aquellas que resultan por la ayuda de procedimientos efectivos. Si
queremos restringirnos a tales valuaciones, entonces primero nos limitaremos a determinados procedimientos efectivos, cálculos formales
por ejemplo. Si establecemos para un cálculo K un concepto de demostración y un concepto formal de refutación, i.e. definido inductivamente
en K, entonces puede determinarse que los enunciados demostrables
en K sean destacados como verdaderos y los enunciados refutables en
K como falsos. En este enfoque resulta natural no limitarse únicamente a aquellos cálculos en los que todo enunciado atómico es demostrable o refutable, sino tomar en consideración también cálculos que dejan
indeterminados a ciertos enunciados. Así, se renuncia al principio de
bivalencia (Prinzip der Wahrheitsdefinit) respecto de los enunciados,
principio que está en la base de la semántica conjuntista’’ (Kutschera
1968, pp. 38 y s.)
Kutschera construye su semántica sobre la base de un cálculo de
secuentes. Más específicamente, formula un cálculo de secuentes
singulares (con un único sucedente) que reproduce las mismas ideas
acerca de las constantes lógicas que subyacen al cálculo de deducción
natural de Gentzen 1934. De esta manera, la semántica queda expresada mediante un cálculo formal. Cualquier sistema de lógica de
662
primer orden será adecuado si es traducible a este cálculo formal.
Esta perspectiva se opone a la semántica ‘‘conjuntista’’, basada en la
teoría de modelos.
II
Más tarde, en 1987, Peter Schröder-Heister introdujo la expresión proof-theoretic semantics, traducible como ‘‘semántica basada en
la teoría de la demostración’’ (véase Schröder-Heister 1991). La idea
básica es que las demostraciones o deducciones tienen un valor semántico, de modo que pueden definirse sobre su base nociones como
consecuencia lógica y verdad lógica. Los significados de los enunciados se entienden en términos de demostraciones y la relación de consecuencia lógica se entiende en términos de demostraciones.
Así, esta idea queda formulada más tarde en las siguientes palabras:
‘‘Según la concepción de la teoría de modelos, la cual prevalece todavía en la lógica […] una consecuencia es lógicamente válida si transmite la verdad de sus premisas a su conclusión, en relación con toda
interpretación. Se muestra que los sistemas de demostración son correctos probando que las consecuencias que ellos generan son lógicamente
válidas. […] La semántica basada en la teoría de la demostración procede al revés, asignando a las demostraciones o deducciones un papel
semántico autónomo desde el principio antes que elucidar su función
en términos de transmisión de verdad. En la semántica basada en la
teoría de la demostración, las demostraciones son […] tratadas […]
como entidades en términos de las cuales se puede elucidar el significado
y la consecuencia lógica’’ (Kahle & Schroeder-Heister 2006, p. 503).
Estas afirmaciones requieren algunas aclaraciones. En general
y siguiendo el programa de Hilbert, la teoría de la demostración se
entiende prima facie como la parte de la metalógica que estudia las
propiedades de las demostraciones formales entendidas como objetos
sintácticos. El núcleo metodológico del programa era el ‘‘punto de vista finito’’ (finite Einstellung) y según este punto de vista son caracterizadas las demostraciones matemáticas con contenido (inhaltlich),
es decir, las demostraciones matemáticas informales. El punto de vista finito se aplica a diferentes tipos de objetos matemáticos: reglas,
enunciados moleculares, definiciones, etc., y sus rasgos centrales consisten en limitar las operaciones a un número finito de objetos y funciones, en no tomar en consideración conjuntos infinitos y en no
663
admitir definiciones impredicativas. La teoría de la demostración que
Hilbert proponía caracterizaba a la deducción como un proceso
combinatorio: a partir de supuestos se obtienen consecuencias nuevas por combinación de aquéllos. La adopción del punto de vista finito da lugar a la matemática finitaria. En su programa, Hilbert
quería reducir la aritmética a esta matemática finitaria con el fin de
probar su consistencia y otorgarle un fundamento seguro. Esta reducción debía llevarse a cabo en el marco de una ‘‘lógica del pensamiento
finito’’, con características propias. Por todo esto, se ha etiquetado de
reductiva a la teoría de la demostración concebida por Hilbert.
Ahora bien, en un sentido más amplio, la teoría de la demostración se ocupa de la representación y la estructura que tienen las demostraciones matemáticas, siendo entonces una ‘‘teoría acerca de
demostraciones’’: ‘‘Las demostraciones expresadas mediante derivaciones formales es el principal objeto de estudio’’ (Kreisel 1971, p.
242). Aquí el término ‘‘demostración’’ hace referencia el proceso mediante el cual se establece la inferencia deductiva de un enunciado
(eventualmente a partir de otros), mientras que ‘‘derivación’’ denota la representación sintáctica de tal proceso. Se supone así que una
demostración es una entidad de algún tipo (no necesariamente sintáctica). Así se habla de una teoría general de la demostración (en
oposición a la teoría de la demostración reductiva), en la cual las
demostraciones se toman como objetos formales (y no meramente
sintácticos).
III
Los resultados que se adoptan para la elaboración de la semántica basada en la teoría de la demostración provienen del estudio de
los sistemas de deducción natural y de recuentes. Un problema básico que interesa en la teoría general de la demostración es el de establecer demostraciones normales (que, idealmente, puedan ser además
únicas). Del hecho de probar la existencia de demostraciones normales se siguen varios resultados. El más importante de ellos es la consistencia (no contradicción) del sistema.
En el caso específico de la deducción natural, la base para establecer la existencia de demostraciones normales consiste en mostrar
que pueden eliminarse las demostraciones ‘‘en círculo’’, en las que la
aplicación de reglas de eliminación de un símbolo lógico sigue a la
aplicación de la respectiva regla de introducción. Esto equivale a
664
mostrar que toda derivación que termine con una aplicación de una
regla de eliminación puede reducirse a una derivación más simple si
esta aplicación aparece inmediatamente después de una aplicación
de la regla de introducción correspondiente.
Por ejemplo, en el caso del condicional material, el segmento de
una demostración con la forma
:
[A]
:
B
___________(I→)
A
A→B
____________________(E→)
B
se reduce directamente.
:
[A]
:
B
Una descripción detallada de estos procedimientos para los restantes símbolos lógicos puede encontrarse en Prawitz 1977 y 1978.
En virtud de los procedimientos de reducción, las reglas de eliminación quedan justificadas sobre la base de las reglas de introducción. Los procedimientos de reducción aseguran que las reglas de
eliminación extienden conservativamente las reglas de introducción.
Esto significa que éstos aseguran que las demostraciones de las
premisas de la aplicación de una regla de eliminación pueden transformase en una demostración de su conclusión (por lo tanto, sin necesidad de aplicar la regla de eliminación). Mediante la aplicación
repetida de procedimientos de reducción, toda demostración se convierte en otra que está en una forma normal. En una demostración
en forma normal (o derivación normal) ningún enunciado aparece
como la conclusión de una regla de introducción y a la vez como la
premisa mayor de la aplicación de una regla de eliminación. Hablando metafóricamente, en la ‘‘mitad superior’’ de una derivación normal
se hace uso de reglas de eliminación para ‘‘desenvolver’’ la informa665
ción contenida en las premisas, la cual es reorganizada en la ‘‘mitad
inferior’’ mediante las reglas de introducción a fin de obtener la conclusión.
IV
La semántica verificacionista abarca actualmente diferentes
enfoques que tienen en común la tesis de que el significado de un
enunciado está determinado por aquello que cuente como un procedimiento para su verificación. Estos enfoques se diferencian del verificacionismo del positivismo lógico surgido en la década de 1920 que
consideraba significativos únicamente a los enunciados para los cuales existía, de hecho, un procedimiento efectivo de verificación, es
decir, a los enunciados decidibles.
La semántica basada en la teoría de la demostración es una forma de semántica verificacionista. En pocas palabras, un enunciado
lógico o matemático es verdadero si existe una demostración para él,
y un enunciado tiene significado si es posible determinar aquello que
cuenta como su demostración (véase, por ejemplo, Prawitz 1998, p.
44). Esta concepción semántica es verificacionista, en la medida en
que una demostración hace verdadero o verifica a un enunciado.
La semántica verificacionista basada en el concepto de demostración otorga a las demostraciones un papel semántico autónomo, contrariamente a lo que ocurre en semántica basada en la teoría de
modelos, en la que las demostraciones dependen semánticamente de
la transmisión de verdad. La idea de una semántica basada en la
teoría de la demostración puede remontarse a la observación que
hace Gentzen al presentar su sistema de deducción natural (mencionada en la sección I), según la cual las reglas de introducción proporcionan el significado de las constantes lógicas. Estas ideas fueron
desarrolladas sobre todo por Michael Dummett, Dag Prawitz y otros,
al mismo tiempo que se obtenían nuevos resultados en la teoría general de la demostración, tales como los teoremas de normalización
en deducción natural.
Esta concepción se ha usado para reconstruir y defender desde
una perspectiva semántica la lógica intuicionista. De hecho, tiene
como antecedente a la teoría BHK de las constantes lógicas, en la que
el significado de las mismas es elucidado sobre las bases de sus condiciones de demostrabilidad (véase Legris 2008, p. 78). Como ha señalado Prawitz, se habla de un verificacionismo en el sentido de que
666
la concepción del significado que propone el intuicionismo matemático se basa en un punto de vista verificacionista y no en consideraciones ontológicas (véase Prawitz 1998, p. 41).
Dummett se ha ocupado de destacar las ideas que están en la
base de la semántica basada en el concepto de demostración. Estas
son, en forma resumida, la tesis de la composicionalidad del significado (el significado de una expresión es función del significado que
los componen), el molecularismo semántico (cada enunciado del lenguaje tiene un significado independiente), la existencia de un nexo
entre significado y comprensión lingüística (la comprensión del lenguaje consiste en el conocimiento del significado), la existencia de un
único concepto clave para elucidar el significado (véase Dummett
1978, pp. 222 y s., y para una descripción más extensa véase Legris
1994, pp. 151 y ss.).
Estas ideas básicas son compartidas por otras perspectivas,
como, por ejemplo, el realismo semántico. Sin embargo, la apelación
al concepto de demostración como concepto clave para analizar el
significado de los enunciados matemáticos marca claramente una
diferencia esencial (véase Dummett 1978, p. 225 y 1991, pp. 176 y
ss.). Esta posición verificacionista surge de diversas constataciones,
que pueden sintetizarse, a grandes rasgos, del modo siguiente.
En primer lugar, el significado de una expresión es determinado por su uso: identidad de uso es identidad de significado. Esta afirmación se basa en aspectos de (a) la comunicabilidad del significado
y (b) el aprendizaje del lenguaje. Es decir, si el significado es comunicable, entonces debe haber algo observable que lo determine, y
además, aprender una lengua es aprender a usarla; captar el significado de una expresión es captar su uso. Pero una tesis adicional
importante es que (c) el conocimiento del significado de un enunciado es un conocimiento implícito, es decir el conocimiento del significado no se explicita en el mismo lenguaje. De otro modo, se caería en
un círculo o en una regresión al infinito (v. Dummett 1978, p. 217).
En segundo lugar, cualquier rasgo que determine el significado
de un enunciado está determinado por el uso que se hace de ese
enunciado. Esto no exige que sea el uso total aquello que determine
el significado, es decir hay aspectos del uso de un enunciado que no
determinan su significado. Lo que determina el significado es algún
‘‘rasgo especial’’ del uso. Esto no lleva a una refutación de una ontología platónica, pero una consecuencia es que las condiciones de verdad
no pueden estar dentro de los rasgos especiales. Basta con considerar enunciados indecidibles, para los cuales no hay un completo co667
nocimiento de sus condiciones de verdad (véase Dummett, 1973, p.
225). En el caso de los enunciados matemáticos, este rasgo especial
del uso es el conocimiento de su demostración. Dummett señala: ‘‘el
conocimiento del significado se manifiesta en la capacidad para reconocer una demostración cuando nos es mostrada’’ (Dummett 1978,
p. 225).
Finalmente, son dos los aspectos del uso de un enunciado que
están implícitos en las demostraciones: las condiciones bajo las cuales se puede aseverar el enunciado y las consecuencias que se siguen
de haberlo aseverado de este modo. De este modo, si las reglas de
introducción de la deducción natural expresan estas condiciones y las
reglas de eliminación resultan ser consecuencia de las condiciones
aceptadas. Así, las reglas de introducción se consideran como la definición de las constantes lógicas, entonces los procedimientos de
reducción completan la justificación de las reglas: las reglas de eliminación se entienden sobre la base de las de introducción (véase
Legris 1999).
V
En suma, la ‘‘semántica de Gentzen’’, basada en la teoría de la
demostración, pretende tanto llegar a una comprensión de la naturaleza de las demostraciones como a elucidar el significado de las
constantes lógicas. En este sentido, sus resultados abonan una la filosofía de la lógica más rica que incluye aspectos pragmáticos (véase Legris 1999). Obviamente, esta semántica ofrece un punto de
partida distinto de (y muchas veces opuesto a) la semántica basada
en la teoría de modelos (o ‘‘semántica de Tarski’’).
Basta con señalar una interesante diferencia entre ambas. La
semántica basada en la teoría de modelos parte de la idea de que los
conceptos de significado, verdad y consecuencia lógica deben analizarse de manera independiente de la manera en que se captan significados o los procedimientos que llevan a establecer la verdad de
enunciados o que un enunciado es consecuencia lógica de otros. En
particular, es independiente del concepto de demostración, que –desde esta perspectiva– queda caracterizado por la definición de derivabilidad en los sistemas formales. Es una tarea posterior establecer,
si esto es posible, la equivalencia extensional de ambos conceptos (esto
es la adecuación de ambos conceptos). Prawitz ha llamado a esta posición perspectiva de los dos estratos (véase Prawitz 1978, p. 25).
668
Esto no sucede en el caso de la semántica basada en la teoría de
la demostración. En el marco de esta semántica los conceptos preformales de significado, verdad y consecuencia lógica pueden ser rigurosamente definidos de una manera tal que dé lugar a una posterior
caracterización de una relación de derivabilidad en sistemas formales. Dicho de otro modo, no hay dos perspectivas diferentes de análisis (sintáctica y semántica formal), sino que ambas responden a las
mismas ideas. La posición defendida por Kutschera en su trabajo de
1968 (la definición de la consecuencia lógica en términos de derivabilidad en un sistema formal) es ciertamente extrema y no tiene actualmente muchos adherentes. Asimismo, la semántica basada en la
teoría de la demostración tiene ciertos presupuestos sobre las demostraciones (su carácter constructivo) que son problemáticos. Pero, en
todo caso, la perspectiva de un único estrato es filosóficamente atractiva.
Referencias
Dummett, Michael. 1978. ‘‘The Philosophical Basis of Intuitionistic Logic’’,
en Truth and Other Enigmas, Londres, Duckworth, pp. 215-247.
Dummett, Michael. 1991. The Logical Basis of Metaphysics, Cambridge
(Mass.), Harvard University Press.
Gentzen, Gerhard. 1934. ‘‘Untersuchungen über das logische Schließen’’,
Mathematische Zeitschrift 39, pp. 176-210 y 405-431. Trad. inglesa en
The Collected Papers of Gerhard Gentzen, comp. por M. E. Szabó,
Amsterdam, North-Holland, 1968.
Kreisel, Georg. 1971. Reseña de The Collected Papers of Gerhard Gentzen,
comp. por M. E. Szabó, en The Journal of Philosophy 68, pp. 238-265.
Kahle, Reinhard & Peter Schroeder-Heister. 2006. ‘‘Introduction: ProofTheoretic Semantics’’, Synthese 148, pp. 503-506.
Kutschera, Franz von. 1968. ‘‘Die Vollständigkeit des Operatorensystems
{¬, ∧, ∨, ⊃} für die intuitionistische Aussagenlogik im Rahmen der
Gentzensemantik’’, Archiv für mathematische Logik und Grundlagen
der Mathematik 11 (1968), pp. 3-16. Repr. en Ausgewählte Aufsätze,
Paderborn, Mentis, 2004, pp. 31- 46.
Legris, Javier. 1994. ‘‘Ideas acerca de los conceptos de demostración y de
verdad matemática’’, Análisis Filosófico 14 , pp. 149-159.
Legris, Javier. 1999. ‘‘Observaciones sobre el desarrollo de la teoría de la
demostración y su relevancia para la filosofía de la lógica’’, en Revista Patagónica de Filosofía 1 (1999), pp. 115-132.
Legris, Javier. 2008. ‘‘Intención y conflicto: sobre la interpretación de la
negación en el intuicionismo matemático’’, en O que nos faz pensar,
Cadernos do Departamento de Filosofia da PUC-Rio 23 (2008), pp. 77-89.
669
Prawitz, Dag. 1977. ‘‘Meaning and Proofs: On the Conflict between Classical
and Intuitionistic Logic’’, Theoria 43, pp. 2-40
Prawitz, Dag. 1978. ‘‘Proofs and the Meaning and Completeness of the
Logical Constants’’, en Essays on Mathematical and Philosophical
Logic, comp. por J. Hintikka, I. Niiniluoto & E. Saarinen, Dordrecht,
Reidel, pp. 25-40.
Prawitz, Dag. 1998. ‘‘Truth and Objectivity from a Verificacionist Point of
View’’, en Truth in Mathematics, comp. por H. G. Dale et al. Oxford,
Clarendon Press, pp. 41-51.
Schröder-Heister, Peter. 1991. ‘‘Uniform Proof-Theoretic Semantics for
Logical Constants’’ (abstract), Journal of Symbolic Logic 56 (1991), p.
1142.
CEF/CONICET, FCE/UBA
E-mail: [email protected]
670
EL ENFOQUE COGNITIVO DE LA LÓGICA
EN G. GENTZEN
GLADYS PALAU
Resumen
En el presente trabajo nos proponemos mostrar el enfoque cognitivo
que recibió la lógica a partir de la publicación de la tesis de Gerhard
Gentzen de 1934, reflejado tanto en el cálculo de deducción natural como en
su lógica de secuentes respecto de las versiones axiomáticas sostenidas por
Frege y en el empirismo lógico fundamentalmente por Russell, y la consecuente distinción entre lógica ‘‘lógica de fórmulas’’ y ‘‘lógica de inferencias’’
que permitió caracterizar en forma precisa diferentes nociones de consecuencia lógica y cambiar radicalmente la presentación de la lógica.
A modo de presentación comenzaremos con unas mínimas referencias al estado de la cuestión acerca de la fundamentación de la
matemática y su relación con la lógica a fin de situar la obra de G.
Gentzen dentro de tal problemática. Desde Frege y hasta bien entrado el siglo XX, tanto la presentación formal de la lógica, como la concepción filosófica acerca de la naturaleza de la misma, han estado
regidas de una u otra forma por el pensamiento fregeano y cuyas
tesis fundamentales y pertinentes a nuestros fines podrían considerarse las siguientes: (i) La lógica consiste en un sistema formado por
un conjunto de fórmulas (semánticamente un conjunto de verdades
lógicas) basado en un conjunto finito de axiomas y ciertas reglas de
inferencia primitivas preservativas de la verdad, las cuales posibilitan la deducción de teoremas que constituyen las restantes verdades
lógicas del sistema y (ii) Las leyes de la matemática y la lógica no se
conocen por medio de la intuición ni son probadas por observaciones
psicológicas, sino que son verdades a priori y analíticas. Es sabido
que estas tesis acerca de la naturaleza de la matemática y la lógica
se plasmaron en los Principia de Whitehead y Russell constituyen671
do la posición filosófica conocida con el nombre de logicismo, la cual
prevaleció hasta bien entrado el siglo XX y se consolidó definitivamente en las rigurosas obras de Alonzo Church, Introduction to Mathematical Logic de 1944 y 1956 y de Elliott Mendelson, Introduction
to Mathematical Logic, de 1964.
Es interesante señalar que la opción por el método axiomático no
se debía a una ignorancia acerca de los sistemas de deducción natural ya propuestos por S. Jaskowski y G. Gentzen, datados ambos en
1934 pero escritos en forma independiente, sino a una fundamentada y racional opción. En efecto, en el texto citado (1956 p. 164) Church
toma una decisión explícita a favor del método axiomático en contra
de los sistemas de deducción natural cuando argumenta a favor del
Teorema de la Deducción contra la regla de Introducción del Condicional sosteniendo que ésta tiene un carácter demasiado ‘‘elemental’’
y que por ello no debe ser admitida como primitiva en un sistema
logístico tal como él lo ha caracterizado. Respecto del texto de Mendelson, su única referencia a la obra de Gentzen consiste en un comentario acerca de la conocida prueba formal de la consistencia de
la aritmética de Gentzen de 1936. Asimismo, en ambos autores, la
presentación de la lógica como sistema axiomático va asociada a una
determinada versión de la noción de consecuencia lógica. En el parágrafo 55 (p. 325) de la mencionada obra, A. Church afirma: ‘‘Una
oración o forma proposicional A de un sistema logístico (...) es una
consecuencia de los postulados si el valor de A es V en todo modelo
de los postulados’’ y, en la nota 533 asociada, identifica su noción de
consecuencia lógica con la dada por A. Tarski en 1936, i.e., con la
noción de consecuencia semántica aún vigente en muchos lógicos
contemporáneos1. Por su parte, Mendelson (1964, p.30) da la versión
sintáctica de esta noción de consecuencia lógica afirmando que una
fórmula bien formada (fbf) A es una consecuencia de un conjunto de
fbf Γ y sólo si hay una secuencia de fórmulas A1,...An en Γ, tal que
para cada Ai, ella es un axioma o una consecuencia lógica de anteriores por la aplicación de una regla de inferencia. En síntesis, el eje
central de la noción de consecuencia lógica en un sistema logístico
pasa por el hecho de que ella ofrece garantía absoluta para la transmisión de la verdad lógica de los axiomas a los teoremas, fundamen1
Efectivamente, en On the Concept of logical consequence, Tarki define la noción de consecuencia lógica de la siguiente forma: Una sentencia S se sigue lógicamente de la clase K si y sólo si todo modelo de la clase K es también un modelo de
la sentencia S, la cual queda caracterizada por las propiedades de Reflexividad,
Monotonía y Corte.
672
tándose así la concepción semántica de la lógica como un conjunto de
verdades lógicas
Por otra parte, es sabido que el logicismo no ha constituido el
único enfoque de la lógica sostenido y discutido en la primera mitad
del siglo XX. En 1930 ya había aparecido en Berlín la obra de A.
Heyting Die formalen Reglen der intuitionistischen Logik, en la cual
Heyting, siguiendo las ideas de Brouwer acerca de la naturaleza
constructiva del pensamiento matemático, presenta también bajo la
forma de sistema axiomático la lógica intuicionista, precisamente con
el fin de construir una lógica acorde con la matemática de Brouwer,
lo cual implicaba que ésta debía reproducir las formas ‘‘intuitivas’’ del
pensamiento matemático y cuya diferencia fundamental con la lógica
clásica consistiría precisamente en el rechazo del principio clásico del
Tercero Excluido, debido a una interpretación diferente de la negación lógica. Si bien el sistema de lógica intuicionista de Heyting preserva la forma axiomática nos interesa destacar que ella generó un
cambio en la mirada acerca de lo que debe entenderse por ‘‘demostración’’, ya que ahora el significado de las fórmulas compuestas de un
sistema lógico no se dará ya en términos de valores de verdad sino
en términos ‘‘prueba’’ partiendo de que ésta es intuitiva para las fórmulas atómicas. Finalmente, es posible sostener que el formalismo
de Hilbert es el movimiento filosófico que finalmente rompe el ‘‘casamiento’’ entre matemática y lógica sostenido por el logicismo cuando, en su artículo de 1926 ‘‘Sobre el infinito’’2, siguiendo a Kant,
Hilbert sostiene que la lógica y la matemática son ciencias independientes y que por ello la matemática no puede fundamentarse solamente en la lógica (ob. cit., p. 142). Textualmente afirma ‘‘(...) we
conceive mathematics to be a stock of two kinds of formulas: those to
which the meaningful communication of finitary statements correspond;
and, secondly, other formulas which signify nothing and which are
the ideal structures of our theory’’ (ob. cit., p. 146) y, a fin de no dejar dudas, en el sumario final del mismo trabajo, agrega ‘‘In contrast
to the early efforts of Frege and Dedekind, we are convinced that
certain intuitive concepts and insights are necessary conditions of
scientific knowledge, that logic is not sufficient’’ (ob. cit., p. 151). Más
aún, entre 1934 y 1938 aparecen en Berlín los dos volúmenes de
Grundlagen der Mathematik de Hilbert y Bernays en los cuales los
autores profundizan estas ideas proponiendo justificar el conocimien2
Publicado en Philosophy of Mathematics, Selected Readings, ed. by P. Benacerraf y H. Putnam, Prentice-Hall Philosophy Series, 1964, pp. 134-151.
673
to matemático en tanto sistema axiomático abstracto constituido por
elementos ideales, i.e exclusivamente por métodos finitarios o constructivos, los cuales consistían en aplicar reglas de inferencia a los
axiomas para poder ‘‘deducir’’ los teoremas. Si bien debe reconocerse el giro constructivo o cognitivo que las ideas de Hilbert introdujeron en la naturaleza del conocimiento matemático, Hilbert continúa
presentado la lógica bajo la forma de sistema axiomático pero, a diferencia de presentaciones anteriores, los 11 axiomas lógicos se enuncian separados para las distintas conectivas proposicionales y tal vez
por esta razón la lógica se siguió presentando como conjunto de teoremas derivados a partir de los axiomas por medio de reglas de inferencia. En síntesis, la verdad de los axiomas continuó siendo el
fundamento del conocimiento lógico-matemático, característica ésta
que impide poner el acento en la noción de regla de inferencia, la cual
precisamente expresa el proceso cognitivo involucrado en el pasaje
de los axiomas a los teoremas.
Seguramente son los trabajos de Paul Hertz de 19203 sobre las
nociones de derivabilidad y la obra de Stanislaw Jaskowski On the
Rules of Supposition in Formal Logic, de 1934, los que primero plantean la cuestión de cómo construir un sistema lógico que capte esta
idea de construcción a partir de supuestos en tanto prueba de teoremas a partir de suposiciones y no de axiomas4. Más aún, según el testimonio dejado por Jaskowski, en el año 1926 Lukasiewicz ya había
planteado en un seminario a su cargo el mismo problema. Sin embargo, pese a estos trabajos que describen de cierta forma la problemática de la época en el campo del pensamiento matemático es en la obra
de G. Gentzen donde la idea se cristaliza ya que, si bien Jaskowski,
ya había introducido la idea de razonar a partir de suposiciones, es
Gentzen quien introduce la división entre reglas de introducción y de
eliminación para caracterizar las conectivas proposicionales y el
nombre de deducción natural (das natuerliche Schliessen) en su obra
Investigations into logical deduction (Untersuchungen über das
Logische Schliessen, 1934-5).
En efecto, para materializar sus ideas, Gentzen debió romper
drásticamente con la formulación axiomática tradicional de la lógica de predicados de Frege, Russell y del mismo Hilbert. A este fin,
3
Para tomar conocimiento de la influencia de la obra de Hertz en el Sistema
de Deducción Natural de Gentzen remitimos al trabajo de J. Legris, ‘‘Paul Hertz y
los orígenes de la teoría de la demostración’’, Episteme, vol. 3, n. 6, 1998.
4
W. Marciszewski, ‘‘A system of Suppositional Logic as embodied in the Proof
of Checker Mizar’’, Mathesis Universales, Nº 3, 1996.
674
construye primero los llamados N-sistemas o N-cálculos pero continuando con el uso de los símbolos de Hilbert en particular para los
cuantificadores5. En ellos la idea central de Gentzen consiste en
construir sistemas formales que expresen lo más adecuadamente
posible los procesos naturales de razonamiento involucrados en la
demostración matemática, objetivo éste que se pone en evidencia en
su primera prueba de consistencia de la aritmética, la cual expone
mediante los N-cálculos y en los cuales la simplicidad y elegancia de
los procedimientos es sacrificada a fin de la ‘‘naturalidad’’ (Szabó,
1969, p. 4). Más aún, hoy en día hay coincidencia en sostener, por un
lado, que los N-cálculos le posibilitaron a Gentzen considerar a la
matemática y a la lógica intuicionista como más natural y más básica
que la lógica clásica y por ello más apropiada para la metamatemática y, por el otro, que las reglas de deducción natural, vía la afirmación
de proposiciones a partir de suposiciones, reflejan más adecuadamente
los aspectos esenciales del razonamiento natural de los matemáticos.
Más aún, en la actualidad existen buenas razones para sostener que
las reglas de eliminación e introducción de las conectivas lógicas
explicitan el significado de las mismas, a pesar de las críticas recibidas de A. Prior y refutadas N. Belnap en su célebre artículo de 1962
‘‘Tonk, Plonk and Plink’’ y en el cual Belnap deja claramente sentado que el significado de las constantes lógicas debe establecerse dentro de un contexto previo de deducibilidad, i.e., dentro de una noción
de consecuencia lógica, tal como lo pensaba Gentzen. Esta noción es
la que precisamente Gentzen caracteriza con las reglas de su cálculo de secuentes, para cuya construcción los especialistas en el tema
coinciden en que Gentzen se inspiró en el enfoque estructural de la
prueba dado por Paul Hertz6, dado que sus reglas explicitan las distintas estructuras que pueden adoptar en una demostración.
Por nuestra parte, somos de la opinión de que la noción de consecuencia lógica expresada por Gentzen en los L-cálculos elucida más
exhaustivamente los aspectos constructivos de la noción de consecuencia lógica que la formulación atribuida a Tarski y también a
Carnap. Nuestras principales razones son las siguientes: (i) La regla
de Atenuación en el antecedente que se corresponde con Monotonía es
complementada con Atenuación en el postsecuente, la cual permitió
luego contar con un método para determinar si una fórmula es o no
5
Jaskowski elaboró un método análogo en 1934, a partir de una sugerencia de
Lukasiewicz en un seminario dictado en 1926.
6
P. Schroeder-Heister, ‘‘Resolution and the origins of structural reasoning’’,
The Bulletin of Symbolic Logic, vol. 8, 2, 2002.
675
es un teorema intuicionista, ya que un teorema será intuicionista si
y solo si no tiene más de una fórmula en el postsecuente; (ii) la propuesta de Gentzen muestra que la regla de Corte, presente en la
caracterización de Tarski, es prescindible, resultado que se demuestra en su célebre teorema Hauptsatz7; (iii) Las reglas estructurales
conjuntamente con las N-reglas o reglas operatorias permiten caracterizar claramente no solamente la noción de consecuencia de la lógica
clásica y la lógica intuicionista sino también la noción de consecuencia
lógica de las lógicas subclásicas, mostrando que ellas no son estructuralmente completas (Wójciki, 1984) y que pueden diferenciarse según sea las reglas que rechacen; y (iv) las reglas de Introducción y
Eliminación permiten otorgar un significado a las constantes lógicas
por su uso y en forma independiente de los clásicos valores de verdad,
camino este tomado por Ian Hacking, en su célebre artículo ‘‘What is
Logic?’’ de 1979.
A partir de los años ’50 distintas propuestas de sistemas de deducción natural comenzaron a aparecer en los textos introductorios
de lógica en nuestro medio tales como Methods of Logic de W. V. O.
Quine (1950), Introduction to Logical Theory de P. F. Strawson
(1952), Symbolic Logic de I. Copi (1958), Elements of Symbolic logic
de H. Reichembach (1956), Logic y Techiques of Formal Reasoning de
D. Kalish & R. Montague (1964), entre muchos otros. Lo común de
todos ellos consiste en afirmar de una u otra forma que los sistemas
de Gentzen son aptos para modelizar los razonamientos del lenguaje ordinario. Por ejemplo, en uno muy reciente8 se afirma: ‘‘Los cálculos de deducción natural (de Gentzen) pretenden describir o modelar
los principios de razonamiento informal o ‘natural’ donde la conclusión se deriva de las premisas en una cadena de razonamientos utilizando unas reglas de deducción que formalizarían principios de
razonamiento formal o natural’’. Sin embargo, opinamos que de los
trabajos escritos por Gentzen no se sigue que su intención haya sido
formalizar el pensamiento natural o de sentido común, tal como se
sostiene en algunos textos. Contrariamente a esta posición creemos
que los cálculos de deducción natural no intentan describir los argumentos que conforman lo que hoy en día se conoce como ‘‘lógica natural’’ o ‘‘lógica de sentido común’’, pese a lo cual en los manuales de
7
Sin embargo, es bueno tenerla formulada en forma explícita porque ella será
explícitamente modificada en la actual formalización de la consecuencia no-monótona.
8
M. Manzano y A. Huertas, ‘‘Lógica para principiantes’’, Alianza, 2004, pp. 137138.
676
lógica se apliquen, en nuestra opinión a veces equivocadamente, a
cualquier argumento del lenguaje natural que sea posible reformular
como argumento deductivo, aunque con esfuerzo y distorsiones vía
un dudoso proceso de formalización. Pese a ello se debe reconocer que
estos cálculos son mucho más adecuados que el método axiomático
para modelizar el razonamiento de sentido común y que su enseñanza será útil y positiva siempre y cuando se especifiquen meticulosamente sus alcances y sus limitaciones, ya que no es posible hoy en día
ignorar que hay otros formalismos con formulaciones incluso ‘‘al estilo Gentzen’’ que, construidos sobre una noción de una consecuencia no monótona, i.e., que no satisfacen la regla de Atenuación en el
Prosecuente, dan cuenta más adecuadamente de los argumentos de
la lógica natural de los sujetos que los propios sistemas de deducción
natural de Gentzen. Sin embargo, es admisible sostener que el enfoque cognitivo de los cálculos de deducción natural han obrado como
‘‘condición de posibilidad’’ para la construcción de las lógicas y formalismos no monótonos construidos precisamente para dar cuenta del
pensamiento natural. Pese a las observaciones apuntadas estimo que
‘‘algo’’ hay en los cálculos de deducción natural que han motivado a
transponer sus aplicaciones más allá del razonamiento matemático.
Creo que la respuesta se encuentra precisamente en el enfoque
cognitivo que subyace en los cálculos de deducción natural tanto en
los de Gentzen como en los de sus predecesores ya que ellos permitieron introducir otra distinta forma de pensar la naturaleza de la
matemática y de la lógica y que ello es lo que hace posible trasponerlos al análisis de la lógica de los lenguajes naturales. Usando una
metáfora más arriesgada: los sistemas de deducción natural, y en
particular con la pulida presentación de Gentzen, bajaron los principios de la lógica (i.e., verdades lógicas) del mundo de las ideas y los
transformaron en reglas o procesos normativos de la mente humana
para razonar correctamente.
No deseo finalizar este trabajo sin mencionar que la introducción
en nuestro medio del enfoque de Gentzen en la concepción de la lógica se debe a los lógicos argentinos Andrés Raggio y Carlos E. Alchourrón. En efecto, Andrés Raggio es quien escribe el primer artículo
en el año 1979, titulado Processes cognitifs logiques9 destinado precisamente a defender la posición filosófica implícita en los cálculos de
deducción natural de Gentzen. Asimismo la concepción abstracta (o
estructural) de la noción de consecuencia lógica subyace en las últi9
Andrés Raggio, Escritos completos, Eudeba, 2002, pp. 287-8.
677
mas obras de Alchourrón y está expresamente sostenida en su trabajo Concepciones de la lógica10. Por el contrario, desde los años 1956,
en nuestro medio los estudios lógicos giraron casi exclusivamente en
torno a las obras de A. Church, Introduction to Mathematical Logic
(1956), S. Kleene, Introduction to Metamathematics (1952) y E. Mendelson, Introduction to Mathematical Logic (1964) en las cuales –a
excepción de la obra de Kleene que dedica el capítulo XV a la presentación de lógica de Secuentes– el nombre de Gentzen solamente es
citado en relación con su prueba de consistencia de la aritmética,
cuya exposición está explícitamente desarrollada en el Apéndice de
la obra de Mendelson citada. La razón de esta ausencia creemos que
en parte se encuentran en el trabajo antes mencionado de A. Raggio.
En efecto, Raggio ubica la labor de Gentzen en la tradición kantiana
porque, según su opinión, a Kant se le debe el mérito de haber sido
el primero en reconocer la importancia de los procesos cognitivos en
filosofía y el haber dado una primera descripción de su estructura y
funcionamiento11. Más aún, según Raggio, el positivismo y en particular el positivismo lógico de la Escuela de Viena, sostuvo dos dicotomías
sumamente inapropiadas para la caracterización del conocimiento
matemático y especialmente para abordar la naturaleza de la lógica,
a saber: 1) la separación ‘‘brutal’’ entre los aspectos puramente teóricos de la explicación científica y la génesis histórico psicológica del
pensamiento científico por el otro y 2) la separación tajante entre
contexto de descubrimiento y contexto de justificación, dejando sólo
para este último el reinado de la lógica (como si en el contexto de
descubrimiento no se utilizaran inferencias lógicas). Y estas eran
precisamente las ideas que predominaban en ese entonces en las
aulas argentinas y que explican la ausencia de la deducción natural
en los cursos superiores de lógica.
En oposición a las ideas imperantes expuestas, en el artículo de
A. Raggio mencionado y respecto de la axiomatización de la lógica de
Frege y Russell, éste afirma que ‘‘ella está muy lejos de la comprensión inmediata y natural de los conceptos lógicos, ya que ellos no han
10
En tomo 7, Lógica, de la Enciclopedia Iberoamericana de Filosofía, Ed. Trotta
CSIC, España,1995.
11
Andrés Raggio en un trabajo de 1967 titulado Consideraciones sobre la concepción kantiana de la lógica formal, afirma: ‘‘para Kant la lógica general hace abstracción de todo contenido del conocimiento (B335), esto es, de toda relación del
mismo con su objeto y considera solo la forma lógica en la relación de los conocimientos entre sí, es decir, la forma de pensar en general, [...] y de esta forma –prosigue
Raggio– Kant desontologiza la lógica’’.
678
utilizado los procesos cognitivos naturales sobre los que se constituyen nuestros conceptos lógicos, sino que solo han tomado en cuenta la
oposición entre lo verdadero y lo falso’’. Y a continuación, como si estuviera hablando en nuestro propio presente afirma con gran convicción y tal vez demasiada fuerza, ‘‘Quiconque a enseigné la logique
connait très bien les difficultés reencontrées par les étudiants de
reconaître dans les connecteurs logiques définis à l’aide des tableaux
de verité les concepts logiques dont ils se servent dans la vie quotidienne et dans la pensée scientifique avec une naturel et une précision
admirable. D’où la vérité incontestable de l’affirmation de beaucoup
de mathématiciens, surtout des mathématiciens français, que l’étude
de la logique empêche le développment des connaissances mathématiques’’. Y a pocas líneas agrega: ‘‘C’est la thèse de Gerhardt Gentzen
‘Recherches sur la déduction logique’ ce qui a bouleversé la situation
du point de vue logique et philosophique’’.
Pasados los años, hoy es imposible desconocer la importancia de
los aportes de la deducción natural vía los cálculos de Gentzen de
deducción natural y de secuentes para la clarificación de la noción de
consecuencia lógica clásica, la cual ha permitido lograr una precisa
caracterización de la noción de consecuencia de las lógicas subclásicas y de las supraclásicas (tanto monótonas como no monótonas) y del
significado de las conectivas lógicas asociado a la noción de consecuencia lógica adoptada.
Referencias
Curry, H., Foundations of Mathematical Logic, New York, Dover, 1976.
Freys, R. y Ladrière, L. (ed.), G. Gentzen: Recherches sur la déduction Logique, Paris, Presses Universitaires de France, 1955.
Goré, Rajeev, ‘‘An Introduction to Classical Propositional Logic: Syntax,
Semantics, Sequent’’, en Foundations of Pure Science in History and
Philosophy of Science, Ghana University Press, Ghana, cap. 49.
Legris, Javier, ‘‘Reglas estructurales y análisis de la consecuencia lógica’’,
en Epistemología e historia de la ciencia, vol. 5, 1999.
Legris, Javier, ‘‘Paul Hetz y los orígenes de la teoría de la demostración’’,
Episteme, Porto Alegre, v. 3, n. 6, pp. 89-99, 1998.
Marciszewski, W., ‘‘A System of Supositional Logic as Embodied in the
Proof Checker Mizar MSE’’, Mathesis Universalis, Nº 3, 1996.
Palau, Gladys, ‘‘Lógica y Psicología’’, en Filosofía de la Lógica, vol. 27 de la
Enciclopedia Iberoamericana de Filosofía, Madrid, Trotta y Consejo
Superior de Investigación Científica de España, 2004, pp. 43-66.
Prawitz, Natural Deduction, Dover, New York, 2006.
679
Raggio, Andrés, ‘‘Processus cognitifs logiques’’, en Andrés Raggio, Escritos
completos, Eudeba, 2002, pp. 287-292, 1965
Rayo, Agustín, ‘‘Logicism Reconsidered’’, en The Oxford Handbook of Philosophy of Mathematics and Logic, Ed. by S. Shapiro, Oxford University
Press, 2007, pp. 203-235.
Szabo, M. E. (ed.), The Collected Papers of Gerhard Gentzen, North-Holland
Publishing Comnpany, 1969.
Wojcicki, Ryszard, Theory of logical calculi, Basic Theory of Consequence
Operations, Dordrecht, Kluwer Academic Publishers, 1988.
Hacking, Jan, ‘‘What is logic?’’, en The Journal of Philosophy, vol. LXXVI,
6, 1979.
UBA- UNLP
680