¿Quién robó los axiomas en la Deducción Natural?

Question

El estudio del cálculo de secuentes de Gentzen me da la oportunidad de proponer algunas reflexiones sobre el concepto de verdad lógica.

Me referiré a la edición en inglés de las obras de Gentzen: Los escritos recopilados (1969), con referencias adicionales a Gaisi Takeuti, Teoría de la demostración (2da ed - 1987).

El cálculo de secuentes LK y LJ asumen como secuente lógico básico un secuente de la forma :

$A \rightarrow A$,

donde $A$ puede ser cualquier fórmula arbitraria [página 151].

Un secuente de la forma $A \rightarrow A$ también se denomina un secuente inicial, o axioma [ver Takeuti].

Podemos restringir los secuentes anteriores a fórmulas atómicas $A$ [ver Takeuti, página 19: Si un secuente es demostrable, entonces es demostrable con una prueba en la que todos los secuentes iniciales consisten en fórmulas atómicas.]

Como explica Gentzen [página 82], el "significado informal" de $A \rightarrow A$ es $\vdash A \supset A$ [a partir del axioma $A \rightarrow A$, por $\supset$-R, obtenemos $\rightarrow A \supset A°: es decir, tenemos una prueba de $A \supset A$].

Tenemos que [Takeuti, página 11] una fórmula $A$ es LK-demostrable (o un teorema de LK) si el secuente $\rightarrow A$ es LK-demostrable, donde una demostración LK (o prueba de LK) es un árbol de secuentes que cumple las siguientes condiciones:

(i) Los secuentes más arriba son secuentes iniciales

(ii) Cada secuente excepto el más bajo es un secuente superior de una inferencia cuyo secuente inferior también está en la prueba.

Debido a los teoremas de corrección y completitud para LK, tenemos que todas y solo las fórmulas válidas son demostrables.

Si consideramos los secuentes lógicos básicos $A \rightarrow A$, con $A$ atómico, podemos decir que son la quintaesencia de la tautología (en el sentido no técnico de "verdad lógica" trivial).

Esto me sugiere una posible forma de "reinterpretar" algunos pasajes del Tractatus de Wittgenstein (1921):

6.1 Las proposiciones de la lógica son tautologías.

Ver en SEP Verdad lógica :

"[Wittgenstein] afirma que las verdades lógicas no “dicen” nada (6.11). [...] Wittgenstein llama a las verdades lógicas analíticas (6.11), y dice que "uno puede reconocer en el símbolo solo que son verdaderas" (6.113). Parece tener en mente el hecho de que se puede "ver" que una verdad lógica de la lógica de funciones de verdad debe ser válida al inspeccionar una representación adecuada de su contenido de funciones de verdad (6.1203, 6.122). Pero la extensión de la idea a la lógica cuantificaciona es problemática [...]"

En el cálculo de secuentes también tenemos, como corolario del teorema de eliminación de cortes, la propiedad de subfórmula [Takeuti, página 29]:

En una prueba libre de cortes en LK (o LJ), todas las fórmulas que ocurren en ella son subfórmulas de las fórmulas en el secuente final.

El "Hauptsatz" de Gentzen a menudo se describe: "como afirmando que una prueba puede organizarse de manera que las premisas de cada paso de inferencia sean siempre más simples [o no más complicadas] que su conclusión" [Sara Negri & Jan von Plato, Teoría de la prueba estructural (2001), página xii].

Esta propiedad me parece ser el contraparte preciso del objetivo de Frege de la formalización:

que a través de la formalización "llegamos a un pequeño número de leyes en las cuales, si agregamos las contenidas en las reglas, se incluye todo el contenido de todas las leyes, aunque en un estado subdesarrollado" (Frege, Begriffsschrift, 1879).

En mi exposición se reduce a la pregunta:

¿Podemos decir que el cálculo de secuentes apoya la idea de que las verdades lógicas son las fórmulas demostrables a partir de axiomas lógicos básicos, es decir, a partir de fórmulas que son "tautologías" (en el sentido de una verdad lógica "trivial" cuya verdad podemos afirmar "por inspección") formadas con "proposiciones elementales" (nuevamente Wittgenstein) ? ¿Y que estas fórmulas son "analíticas" (en el sentido de Kant y Frege)?

En apoyo de esta interpretación (y este hecho aclara, para mí, también la interrelación entre la lógica y las matemáticas), sugiero considerar también la forma en que Gentzen extiende el cálculo de secuentes a la aritmética [página 151]:

Un secuente matemático básico es un secuente de la forma $\rightarrow C$, donde la fórmula $C$ representa un "axioma matemático".

Según la interpretación anterior, la fórmula $C$ no es una "tautología", y los teoremas matemáticos demostrados en el cálculo de secuentes con la adición de "axiomas matemáticos" claramente no son más "analíticos" [página 151].

---

Es bien conocido que el cálculo de secuentes y la deducción natural tienen su origen común en el trabajo de Gentzen.

Existe una traducción "estándar" de derivaciones sin cortes en el cálculo de secuentes a derivaciones de deducción natural [ver Negri & von Plato, capítulo 8].

En la deducción natural no hay axiomas: la traducción mencionada mapea el secuente $A \rightarrow A$ en una suposición $A$.

Así que mi pregunta final es:

¿Qué está mal en la interpretación anterior de la verdad lógica "según" el cálculo de secuentes? ¿Es posible conciliarlo con la deducción natural?

---

Agregado 15 de marzo

Tras algunos comentarios, parece un poco "inapropiado" llamar axiomas a los secuentes iniciales; Gentzen no lo hizo. Utiliza el término solo en el contexto de 'axiomas matemáticos', es decir, para secuentes matemáticos básicos [página 151].

Entonces podemos "restaurar la simetría" entre el cálculo de secuentes y la deducción natural: los secuentes iniciales son -exactamente como las suposiciones- una forma de "iniciar" las inferencias.

En conclusión, el cálculo de secuentes (exactamente como la deducción natural) apoya la idea de que un cálculo lógico se basa en reglas de inferencia: en este sentido, es eminentemente "formal".

Solo cuando "aplicamos" esto, es decir, introducimos axiomas matemáticos (o axiomas relacionados con otras ciencias), "introducimos significado".

Si esta visión es sólida, me parece que se mantiene una caracterización "estrictamente formal" de la verdad lógica; para caracterizarla necesitamos semántica, a través del concepto de validez.

Answer 1

No creo que necesariamente haya algo profundo ocurriendo aquí.

Tu observación inicial parece ser simplemente que podemos intercambiar axiomas lógicos por reglas de inferencia y viceversa. Un sistema de tipo Hilbert trata de tener la menor cantidad de reglas de inferencia posible (sólo necesita al menos una, es decir, el modus ponens, para poder hacer algo) y pone todo el trabajo en los axiomas, mientras que el cálculo de secuentes va al otro extremo y hace todo el trabajo con una gran cantidad de reglas de inferencia mientras se adhiere al axioma más simple imaginable.

En principio, sería igualmente posible redactar la mayoría de los axiomas no lógicos de una teoría como reglas de inferencia en lugar de axiomas. Por ejemplo, si estamos haciendo Aritmética de Peano en deducción natural, podríamos elegir escribir la regla de inducción como $$\frac{n=0\to\psi \qquad (\forall n. n=x\to\psi)\to(\forall n.n=S(x)\to\psi)}{\psi} x\text{ no libre en }\psi$$

La única razón por la que no estamos haciendo rutinariamente eso es que a menudo queremos recopilar los axiomas no lógicos como "objetos de interés" en sí mismos, para ser manipulados, colocados en conjuntos, etc., lo cual es técnicamente más conveniente si son fórmulas que si son reglas de inferencia.

Por lo tanto, creo que la escala de reglas/axiomas ejemplificada por el estilo Hilbert o Gentzen es más o menos ortogonal al concepto de "verdad lógica", entendido como fórmulas que pueden demostrarse por medios puramente lógicos (ya sea que estos medios lógicos sean axiomas o reglas), sin utilizar ninguna de las reglas/axiomas específicos de la teoría.

Answer 2

Ten mucho cuidado aquí:

El Tractatus de Wittgenstein

El Tractatus de Wittgenstein fue escrito mucho antes que las "Untersuchungen uber das logischen schliessen" de Gentzen (1916 vs 1933), por lo que no hay una relación real entre ellos. (Creo que es dudoso que Gentzen haya leído a Wittgenstein, pero eso es otro asunto).

Deducción natural:

Gentzen encontró la lógica axiomática muy diferente a las demostraciones matemáticas normales (creo que podemos estar de acuerdo con él en esto) e inventó la deducción natural, con la esperanza de que funcione más como se hacen realmente las demostraciones matemáticas. (Gentzen escribe bastante bien sobre esto, "el arte de hacer demostraciones matemáticas" y así, no puedo hacerle justicia en la traducción).

Las demostraciones matemáticas normales no razonan realmente con axiomas lógicos sino con reglas de inferencia, por lo que la deducción natural tampoco tiene axiomas lógicos, la diferencia principal es que mientras que en la mayoría de las demostraciones matemáticas las reglas de inferencia son implícitas (no realmente mencionadas), en la deducción natural estas reglas se mencionan explícitamente.

Cálculo de secuentes

El cálculo de secuentes es una forma más técnica de la Deducción Natural, permite más fórmulas en uno u otro lado del $ \rightarrow $ (excepto en el caso intuicionista donde solo se permite una fórmula en el lado derecho) y tiene sus propias reglas de inferencia. (y por lo tanto, nuevamente no está realmente como se hacen las demostraciones matemáticas, pero el cálculo de secuentes es un área fértil de estudio lógico, especialmente para los muchos tipos diferentes de lógicas subestructurales, consulta http://en.wikipedia.org/wiki/Substructural_logic )

Aunque informalmente, como Gentzen explica el "significado informal" de $A \rightarrow A$ es $A \supset A$, hay una diferencia fundamental entre ellos.

El $ \rightarrow $ no es realmente un conectivo, es más como un marcador de límites entre la sección derecha (consecuente) e izquierda (antecedente) de un secuente (y por lo tanto, en cada secuente necesitas uno y solo puedes tener uno).

Y aunque informalmente significa que la conjunción de todas las fórmulas en el lado izquierdo implica la disyunción de las fórmulas en el lado derecho. Formalmente hay que tener mucho cuidado, las fórmulas y los secuentes son entidades formales diferentes, $ A_1,....,A_n \rightarrow B_1,...,B_m $ es un secuente mientras que $ A \supset B $ es una fórmula.

Por lo tanto, llamar a $ B \rightarrow B $ un axioma es un poco incorrecto. Un axioma es una fórmula, y esto es un secuente, por lo que el nombre secuente inicial es más adecuado. (pero por supuesto, llamarlo informalmente un axioma, siempre y cuando te des cuenta de que es solo informalmente)

Los lados de un secuente pueden estar vacíos si el lado antecedente (izquierdo) está vacío, el lado consecuente (derecho) es un teorema, si el lado derecho está vacío, puedes colocar el signo de contradicción allí. Entonces $ \rightarrow B \supset B $ (antecedente vacío) es un secuente, al igual que $ B \supset B \rightarrow $ (consecuente vacío) e incluso solo $ \rightarrow $ (ambos vacíos) son secuentes bien formados.

Pero $ A \rightarrow (B \rightarrow B )$ y $ \supset $ no son bien formados.

Un secuente es algo entre el metalenguaje y las fórmulas (comparable al signo $ \vdash $ o $ \Rightarrow $ que a veces se usa en su lugar).

El cálculo de secuentes tiene sus propias reglas de inferencia y son del tipo en uno o más secuentes de entrada, un secuente de salida (muy parecido a la Deducción Natural).

Concluyendo con Godel

Un último punto que no se menciona lo suficiente (o nada), en los teoremas de incompletitud de Gödel, una prueba es una prueba axiomática no una prueba usando deducción natural o cálculo de secuentes.

Debido a que una prueba axiomática es solo una lista de fórmulas (donde cada fórmula en la lista es un teorema), es fácilmente codificable (relativamente).

Las pruebas de deducción natural y cálculo de secuentes, por otro lado, donde no todas las fórmulas son teoremas, la codificación es horrible.

Espero que esto ayude.

Answer 3

Wittgenstein estaba interesado en la noción de átomos lógicos. No lo probó, sino que simplemente afirmó que ese era el caso.

Aparentemente, Conifold sugiere que Wittgenstein estaba interesado en el diatleitismo. Él (Conifold) no presentó evidencia para esta tesis. Así que saca tus propias conclusiones.

Nadie "robó" los axiomas para la deducción natural. Las ideas no pertenecen a nadie, sino que simplemente se filtran a través de una comunidad a medida que la opinión se vuelve favorable y las modas cambian.

Sí. Incluso las matemáticas tienen modas.