Diferencia entre axiomas lógicos y reglas de inferencia

Un axioma lógico puede considerarse una regla de inferencia que no tiene antecedentes.

Cualquier sistema de prueba interesante debe tener al menos un axioma y una regla de inferencia con premisas. Si no tiene axiomas, entonces no hay forma de comenzar una prueba en la teoría vacía, y sin reglas de inferencia, todo lo que podría probarse serían los axiomas mismos.

Los sistemas de prueba al estilo de Hilbert generalmente tienen muchos axiomas y pocas reglas de inferencia adecuadas. Por el contrario, los cálculos de estilo Gentzen ( cálculo secuencial y deducción natural ) tienen un número mínimo de axiomas y muchas reglas de inferencia.

En ambos casos, uno puede expresar cada instancia de un axioma y/o regla de inferencia como una cadena en un lenguaje formal particular.

Una teoría consta de axiomas que se suman a los axiomas lógicos que proceden de la lógica. Las teorías no contienen ninguna regla propia de inferencia propia.

Es esencialmente una cuestión de punto de vista.

La idea de los axiomas lógicos se remonta a Begriffsschrift de Frege (1879). Para Frege, la lógica es una ciencia, en particular, la rama del conocimiento que se ocupa de la verdad. Por lo tanto, es indispensable contar con un cuerpo de leyes que rija la materia, a saber, la noción de verdad. Esas son las cosas que conocemos como axiomas lógicos.

Parece natural derivar el más complejo de estos juicios [del pensamiento puro] de los más simples, no para hacerlos más seguros, lo que sería innecesario en la mayoría de los casos, sino para poner de manifiesto las relaciones de los juicios entre sí. otro. Evidentemente, no es lo mismo simplemente conocer las leyes que conocerlas junto con las conexiones que unas tienen con otras. Llegamos así a un reducido número de leyes en las que, si sumamos las contenidas en las normas, se incluye el contenido de todas las leyes, aunque en estado no desarrollado. (Frege 1879, §13)

También es importante mencionar que, para Frege (y Russell), no había una diferencia clara entre la lógica y las matemáticas, por lo que la práctica moderna, ejemplificada en teorías de conjuntos como ZFC, de incorporar principios lógicos como reglas de inferencia y reglas específicas de la materia. hechos matemáticos como axiomas era impensable.

El Untersuchungen über das logische Schließen de Gentzen (1934/1935) marcó el punto de inflexión desde esta primera axiomática hasta la moderna concepción inferencial de la lógica. Básicamente, la idea de Gentzen era desarrollar una noción de prueba formal que representara más fielmente el razonamiento matemático real:

Mi punto de partida fue este: la formalización de la deducción lógica, especialmente tal como la desarrollaron Frege, Russell e Hilbert, está bastante alejada de las formas de deducción utilizadas en la práctica en las demostraciones matemáticas. A cambio, se obtienen considerables ventajas formales. Por el contrario, primero intenté establecer un sistema formal que se acercara lo más posible al razonamiento real. El resultado fue un ' cálculo de deducción natural '. (Gentzen, 1934/1935)

De hecho, los cálculos al estilo de Hilbert no son muy agradables para trabajar, ya que las pruebas formales de tautologías simples en esos sistemas a menudo se basan en argumentos extremadamente artificiales. Vale la pena mencionar que el propio Frege no se dio cuenta de que sus seis axiomas para el cálculo proposicional no son independientes:

1. $A \rightarrow (B \rightarrow A)$
2. $(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))$
3. $(A \rightarrow (B \rightarrow C)) \rightarrow (B \rightarrow (A \rightarrow C))$
4. $(A \rightarrow B) \rightarrow (\neg B \rightarrow \neg A)$
5. $\neg \neg A \rightarrow A$
6. $A \rightarrow \neg \neg A$

Es decir, el Axioma 3 se puede obtener del modus ponens y los Axiomas 1 y 2. Este resultado fue establecido por primera vez por Łukasicwicz en 1929. Además, los Axiomas 3, 4 y 5 se pueden reducir a un solo axioma:

Esto también pasó desapercibido para Frege.

Los cálculos de estilo Gentzen dan más protagonismo a las reglas de inferencia, que representan el proceso de razonamiento con conectivos lógicos explicando cómo se pueden obtener (reglas de introducción) y qué podemos hacer con ellos (reglas de eliminación). Por lo general, solo se basan en algunos axiomas, como el axioma de reflexión:

¡pero incluso esto puede considerarse como una regla de inferencia sin supuestos!