Teorema de la deducción

Question

¿Existe un sistema axiomático en el que no se cumpla el teorema de la deducción?

Answer 1

Los fallos del teorema de la deducción son uno de los temas más misteriosos de la lógica, según mi experiencia. El lema es que los axiomas son más fuertes que las reglas .

He aquí el ejemplo no trivial más sencillo que conozco. Comience con la lógica proposicional con dos variables $A$ y $B$ . Añade la nueva regla de inferencia única $A \vdash B$ al sistema deductivo habitual al estilo de Hilbert, sin nuevos axiomas. Nótese que esto no cambia en absoluto la colección de fórmulas que se pueden derivar. (Prueba: la primera vez que se usa la nueva regla, ya se tuvo que derivar $A$ en el sistema original, pero no se puede, porque el sistema original sólo deriva tautologías. Así que nunca se puede utilizar la nueva regla). Así, el nuevo sistema tiene la regla $A \vdash B$ pero no deriva $A \to B$ y por lo tanto el teorema de la deducción falla.

Pero este nuevo sistema no es del todo trivial. Si añadimos $A$ como un nuevo axioma, entonces podemos derivar $B$ en la lógica expandida, lo que no podemos hacer en la lógica proposicional ordinaria. Así que hay una interacción entre las reglas de inferencia y los axiomas de una teoría dada.

El teorema de la deducción para la lógica de primer orden muestra que esta interacción se comporta muy bien en ese contexto: una teoría de primer orden arbitraria $\Delta$ con el sistema deductivo habitual tiene la regla derivada $\phi \vdash \psi$ si y sólo si tiene la regla derivada $\vdash \phi \to \psi$ . En retrospectiva, no hay razón para esperar que esto se mantenga para conjuntos arbitrarios de reglas de deducción, porque los nuevos axiomas pueden dar fuerza adicional a las reglas existentes.

Como ha mencionado François G. Dorais en los comentarios, se conocen ejemplos más complicados en la teoría de las pruebas. Son similares al ejemplo anterior en el sentido de que debilitan un axioma sustituyéndolo por una regla. La idea general es que un axioma de extensionalidad de la forma $x = y \to f(x) = f(y)$ podría sustituirse por una regla $x = y \vdash f(x) = f(y)$ . Esto sugiere inmediatamente cómo puede fallar el teorema de la deducción: si $x$ y $y$ son términos que no son probablemente iguales, pero son iguales en alguna interpretación, entonces el axioma de extensionalidad podría fallar en esa interpretación incluso si la regla de inferencia se satisface en algún sentido. Pero esto es sólo un esbozo heurístico del argumento. Para una explicación breve y rigurosa, véase " Una nota sobre la regla de extensionalidad sin cuantificadores de Spector "por Ulrich Kohlenbach, Archivo de Lógica Matemática 40:2 (2001), pp 89-92.

Answer 2

Lógica algebraica abstracta ha estudiado las conexiones entre varias formas del Teorema de la Deducción, para una lógica algebraizable dada, y nociones algebraicas universales como la existencia de relaciones de congruencia principales definibles para su cuasivariedad equivalente. Para una explicación cuidadosa de esto, véase " Lógica algebraica abstracta y el teorema de la deducción "de Blok y Pigozzi. Estas herramientas ayudan a demostrar que el Teorema de la Deducción falla para algunas lógicas lineales, o para la lógica ortomodular.

Answer 3

La respuesta de Carl es muy buena, pero voy a añadir algo que creo que puede ser útil desde el punto de vista de la comprensión del problema. Como ejemplo se puede tomar también alguna formalización axiomática estándar de la lógica de primer orden con la regla de generalización: $$\frac{\varphi}{\forall x\varphi}$$ Entonces, para cualquier fórmula $\varphi(x)$ con $x$ libre es el caso que $\varphi(x)\vdash\forall x\varphi(x)$ pero, en general, no se da el caso de que $\vdash\varphi(x)\rightarrow\forall x\varphi(x)$ . Así que el teorema de la deducción se mantiene, pero de forma ligeramente modificada:

Si $\varphi\vdash\forall x\varphi$ entonces $\vdash\varphi\rightarrow\forall x\varphi$ siempre que no se aplique la regla de generalización con respecto a las variables libres en $\varphi$ .

Otro ejemplo pueden ser algunos sistemas de lógica modal con la regla de la necesidad: $$\frac{\varphi}{\square\varphi}$$ $\varphi\rightarrow\square\varphi$ normalmente NO es una tesis de tales sistemas.

Answer 4

Las lógicas no clásicas, como la lógica paraconsistente, etc., normalmente no tienen problemas con el teorema de la deducción, siempre que no no tengan una implicación basada en la relevancia, es decir, si se basan en en celosías residuadas y no tratan de evitar la paradoja positiva.

Por otro lado, muchas personas creen que el teorema de la deducción no se cumple en las lógicas modales, especialmente en las lógicas interesantes como la lógica temporal. Un argumento típico es el siguiente. En la lógica modal tendríamos una regla de inferencia:

  P
----
[] P

Y por lo tanto si un teorema de deducción estuviera disponible, nosotros podría probar P -> [] P, lo que no se desea. Este argumento se repite, por ejemplo, de manera informal en la Lógica Temporal, El menor de los tres males , Leslie Lamport, Microsoft Research, MSR-TR-2004-104.

Afortunadamente, las cosas no son tan graves. Un análisis más detallado análisis es el siguiente ¿Falla el teorema de la deducción para la lógica modal? Raul Hakli, Sara Negri, 10 de noviembre de 2010. En un cálculo de estilo Hilbert HK la regla anterior debería ser formulada de forma más precisa como sigue:

    |- A
 ---------
 G |- [] A

Entonces se cumple el teorema de la deducción. Y no podemos demostrar |- P en primer lugar, y por lo tanto tampoco ir a |- P -> [] P. Además de un cálculo de estilo Hilbert, el documento también presenta un cálculo equivalente al estilo Gentzen que tiene el teorema de deducción ya como regla de inferencia. Es la regla de introducción de la implicación correcta.

Adiós

Answer 5

Como parece que en el nivel de investigación la notación es el mayor problema para algunas personas, voy a compartir un enlace a la notación clásica del sistema L3 de Ukasiewicz, donde el teorema deductivo en sentido clásico no se sostiene (pero la versión modificada - se sostiene) - sólo echa un vistazo aquí: L3 lógica de ukasiewicz y aquí: sistema ukasiewicz L3 y la referencia:

Bergmann, Merrie (2008). Una introducción a la lógica multivaluada y difusa logic: semantics, algebras, and derivation systems. Cambridge University Press. p. 114. ISBN 978-0-521-88128-9.