Diferencia entre $\vdash A\to B$ y $A\vdash B$

Question

Es $\vdash A\to B$ equivalente a $A\vdash B$ ¿en el sentido de que si se puede probar una, entonces se puede probar la otra? Yo probaría la primera tomando $A$ como hipótesis, y luego demostrar $B$ . Esto produciría $A\to B$ con la regla de introducción de $\to$ . Y para esto último tomaría $A$ como premisa, y luego mostrar $B$ .

Así que mi pregunta es: ¿hay alguna diferencia importante entre ambos?

Answer 1

Normalmente lo son, pero los detalles dependen del sistema lógico con el que se trabaje.

Por ejemplo, si se tiene la regla de inferencia modus ponens, entonces se deduce que $\vdash A\to B$ implica $A\vdash B,$ ya que usted toma $A$ como una suposición, demuestre $A\to B$ y luego usar el modus ponens para concluir $B.$ En un marco de deducción natural, esto no es más que la regla de eliminación de $\to.$

Por otra parte, el hecho de que $A\vdash B$ implica $\vdash A\to B$ se suele demostrar como un teorema y se denomina teorema de la deducción en el estudio de los sistemas de estilo Hilbert (por ejemplo, en Mendelson). En un sistema de deducción natural, normalmente sólo sería una regla de introducción para $\to.$

La equivalencia depende de que su sistema formal tenga las características mencionadas, pero la mayoría de los sistemas de importancia práctica las tienen.

Answer 2

Tienes razón en que -en cualquier lógica medianamente sensata- es el caso que $\vdash A\to B$ se mantiene si y sólo si $A\vdash B$ lo hace.

Ambas formas existen porque sirven para cosas diferentes en la estructura de una prueba. La forma $A\vdash B$ le da la posibilidad de aplicar otras reglas que dependen de la estructura interna de $B$ (o, dependiendo del sistema, posiblemente también $A$ ). Estas normas no podrían "ver detrás" del $\to$ en el $\vdash A\to B$ forma.

Por otro lado, $\vdash A\to B$ es lo que se necesita si se está emparejando con una regla que trata $A\to B$ como una unidad. Por ejemplo, si se quiere probar $(A\to B)\land(C\to D)$ primero tendría que establecer $\vdash A\to B$ y $\vdash C\to D$ y luego aplicar un $\land$ regla. El $\land$ regla no sabe nada de $\to$ y no sería capaz de inventar un $\to$ de la $A\vdash B$ forma por sí misma.

El formulario que necesita para probando algo no es siempre igual a la forma que se necesita al utilizarlo, por lo que es necesario poder pasar de uno a otro y viceversa. Afortunadamente esto es bastante fácil en más sistemas de prueba. (La principal excepción son los sistemas de estilo Hilbert, en los que puede ser necesaria una importante reescritura de la derivación de $A\vdash B$ para obtener $\vdash A\to B$ ).