Se puede ver en Elliott Mendelson, Introducción a la Lógica Matemática (4ª ed - 1997), página 38, el Lema 1.11.c [consulte la página 39 para la derivación] :
$\vdash \lnot \mathcal B \rightarrow (\mathcal B \rightarrow \mathcal C)$.
Es el "bloque de construcción básico" para probar en una de Hilbert de estilo a prueba de sistema de axiomas + modus ponens) el Ex Falso Quodlibet.
En Deducción Natural, puede utilizar el llamado $\lnot$-eliminación de la regla (de$A$$\lnot A$, inferir $\bot$, es decir, el falsum), seguido por la Abs-regla (de $\bot$, inferir $B$ lo que sea) que se derivan de una contradicción, una fórmula wathever [puedes ver el debate acerca de la DN reglas que implican $\lnot$ y $\bot$ en este post].
Nota.
Este es Mendelson sistema de axiomas :
(A1) $\mathcal{B} \rightarrow ( \mathcal{C} \rightarrow \mathcal{B})$
(A2) $(\mathcal{B} \rightarrow ( \mathcal{C} \rightarrow \mathcal{D})) \rightarrow ((\mathcal{B} \rightarrow \mathcal{C}) \rightarrow (\mathcal{B} \rightarrow \mathcal{D}))$
(A3) $(\lnot \mathcal{C} \rightarrow \lnot \mathcal{B}) \rightarrow ((\lnot \mathcal{C} \rightarrow \mathcal{B}) \rightarrow \mathcal{C})$.
Con (A1) y (A2) demuestra Lema 1.8 [página 36] :
$\vdash \mathcal{B} \rightarrow \mathcal{B}$.
Con la ayuda de Lema 1.8 y el uso de sólo (A1) y (A2) es posible demostrar el Teorema de la Deducción [la Proposición 1.9, página 37]:
si $\Gamma, \mathcal{B} \vdash \mathcal{C}$,$\Gamma \vdash \mathcal{B} \rightarrow \mathcal{C}$.
Finalmente, Mendelson demuestra Lema 1.11.c :
$\vdash \lnot \mathcal B \rightarrow (\mathcal B \rightarrow \mathcal C)$.
Sin DT aún podemos tener ex falso quodlibet como un "derivado de la regla" :
(1) $\quad \lnot \mathcal B$ --- supone
(2) $\quad \mathcal B$ --- supone
(3) $\quad \vdash \mathcal B \rightarrow ( \lnot \mathcal C \rightarrow \mathcal B )$ --- (A1)
(4) $\quad \vdash \mathcal{\lnot B} \rightarrow ( \mathcal{\lnot C} \rightarrow \mathcal{\lnot B})$ --- (A1)
(5) $\quad \mathcal{\lnot C} \rightarrow \mathcal B$ --- a partir de (2) y (3) por modus ponens
(6) $\quad \mathcal{\lnot C} \rightarrow \mathcal{\lnot B}$ --- a partir de (1) y (4) por modus ponens
(7) $\quad \vdash (\lnot \mathcal{C} \rightarrow \lnot \mathcal{B}) \rightarrow ((\lnot \mathcal{C} \rightarrow \mathcal{B}) \rightarrow \mathcal{C})$ --- (A3)
(8) $\quad \mathcal{C}$ --- a partir de (5), (6) y (7) por modus ponens dos veces.
Por lo tanto :
$\quad \lnot \mathcal B, \mathcal B \vdash \mathcal C$.
En Mendelson del sistema, $\land$ $\lor$ son no primitivo; se definen como :
$p \land q =_{def} \lnot (p \rightarrow \lnot q)$
$p \lor q =_{def} \lnot p \rightarrow q$
Tener el Teorema de la Deducción, Mendelson, prueba un par de otros resultados de utilidad [ver Corolario 1.10, página 38] y, a continuación, Lema 1.11 incluyendo :
$\vdash \lnot \lnot \mathcal B \rightarrow \mathcal B$ --- Lema 1.11.un
y
$\vdash \mathcal B \rightarrow \lnot \lnot \mathcal B$ --- Lema 1.11.b.
Ahora tenemos :
(a)$\quad \vdash \mathcal B \rightarrow \lnot \lnot \mathcal B$ --- Lema 1.11.b
(b)$\quad \vdash \lnot \lnot (\mathcal B \rightarrow \lnot \lnot \mathcal B)$ --- de Lema 1.11.b ", que se aplica a sí mismo" modus ponens
(c)$\quad \vdash \lnot (\mathcal B \land \lnot \mathcal B)$ --- con la definición de $\land$
(d)$\quad \vdash \lnot (\mathcal B \land \lnot \mathcal B) \rightarrow ((\mathcal B \land \lnot \mathcal B) \rightarrow \mathcal C)$ --- Lema 1.11 c con la sustitución de $(\mathcal B \land \lnot \mathcal B)$ en lugar de $\mathcal B$.
Por lo tanto :
$\vdash \mathcal B \land \lnot \mathcal B \rightarrow \mathcal C$ --- de (c) y (d) por modus ponens.
Leer más.
Puede ser útil ver la nota por Peter Smith en los Tipos de prueba del sistema en su Lógica de Asuntos blog.
