¿Por qué los sistemas lógicos de Hilbert utilizan los axiomas que utilizan?

Question

Por ejemplo, en un sistema de Hilbert para la lógica proposicional, un sistema de muestra utiliza el modus ponens junto con tres axiomas:

I. $A \to (B \to A)$

II. $(A \to (B \to C)) \to ((A \to B) \to (A \to C))$

III. $(\lnot B \to \lnot A) \to (A \to B)$

¿Cómo se le ocurrieron a Hilbert estos axiomas como suficientes para representar todo un sistema lógico?

¿Se trata sobre todo de ensayo y error para llegar a un conjunto de axiomas o hay un método para la locura?

Answer 1

La forma en que se encontró originalmente este conjunto de axiomas fue probablemente una mezcla de ensayo y error, adaptando trabajos anteriores y optimizando el número mínimo de axiomas. Las conexiones con la lógica combinatoria a las que me refiero más adelante probablemente también fueron un factor.

Para un relato (probablemente) ahistórico, permítanme empezar reescribiendo ligeramente los dos primeros axiomas:

$A\to(\Gamma\to A)$

$(\Gamma\to(A\to B))\to(\Gamma\to A)\to(\Gamma\to B)$

Si tachamos el $\Gamma$ s, obtenemos $A\to A$ y $(A\to B)\to(A\to B)$ (esta última puede considerarse una forma de curry de $(A\to B)\land A \to B$ ). Podemos pensar en ellas como internalizaciones de las reglas de Identidad y Corte: $$\dfrac{}{A\vdash A}\qquad \dfrac{A\vdash B\qquad \vdash A}{\vdash B}$$ Añadir el $\Gamma$ s de vuelta nos da internalizaciones de las reglas anteriores con contextos, es decir, las reglas: $$\dfrac{}{\Gamma,A\vdash A}\qquad \dfrac{\Gamma,A\vdash B\qquad \Gamma\vdash A}{\Gamma\vdash B}$$

El resultado es que podemos codificar el razonamiento hipotético codificando $\Gamma\vdash A$ como $\Gamma\to A$ y luego manipularlos con las "reglas" de identidad y corte internas. Efectivamente, los axiomas I y II son los necesarios para demostrar el Teorema de la Deducción. Como perspectiva relevante de la prueba, los axiomas I y II corresponden a $K$ y $S$ de lógica combinatoria y el Teorema de la Deducción corresponde a la abstracción de corchetes.

Si nos detenemos aquí, tenemos una lógica de implicación positiva. Si continuamos y seguimos usando nuestra idea de codificar el razonamiento hipotético $\Gamma\vdash A$ como $\Gamma\to A$ entonces debemos mirar las reglas para $\neg$ . En el cálculo secuencial son: $$\dfrac{\Gamma,\neg A\vdash\Delta}{\Gamma\vdash A,\Delta}\qquad\dfrac{\Gamma\vdash\neg A,\Delta}{\Gamma,A\vdash\Delta}$$ Por supuesto, el uso de estas dos reglas da: $$\dfrac{\Gamma,\neg B\vdash\neg A,\Delta}{\Gamma,A\vdash B,\Delta}$$ Esta regla tiene la ventaja de no modificar el número de conclusiones. Podemos obtener aproximadamente las reglas originales eligiendo $A$ ser algo demostrable o $B$ algo que es refutable.

La primera regla para $\neg$ sugiere que podemos representar las conclusiones adicionales, $\Delta$ mediante suposiciones adicionales negadas en $\Gamma$ . El tercer axioma no necesita entonces ocuparse de los supuestos, ya que el Teorema de la Deducción basado en los otros dos axiomas significa que podemos añadirlos cuando queramos. Lo que estoy haciendo aquí es si una regla como $\dfrac{\Gamma,\neg B\vdash\neg A}{\Gamma,A\vdash B}$ es lo suficientemente fuerte como única regla de negación para derivar todos los resultados clásicos (en un contexto en el que también tenemos reglas de implicación). Podríamos, por ejemplo, tomar $\neg\neg A\to A$ como un axioma, pero esto resulta ser demasiado débil por sí mismo. Que este podría ser el caso, se podría ver al verlo como una codificación de una regla como hemos estado haciendo. Esa regla (codificada) no nos da ninguna forma de tratar con solo hipótesis negadas o negaciones (únicas) en las conclusiones.

En general, muchos axiomas de los sistemas de estilo Hilbert pueden entenderse como codificaciones de reglas. Por ejemplo, un axioma para $\lor$ es $(A\to C)\to(B\to C)\to (A\lor B \to C)$ que podemos ver como una codificación de la regla $\dfrac{A\vdash C\qquad B\vdash C}{A\lor B\vdash C}$ . Por supuesto, la codificación representa $\vdash$ la meta-implicación (es decir, la barra horizontal en las reglas), y $\to$ todo como $\to$ . Por ejemplo, arriba dije que el segundo axioma codificaba la regla de corte, pero también podría haber dicho que codificaba una regla de modus-ponens-con-contextos.