¿Cómo se utiliza aquí la introducción de la implicación?

Question

No entiendo cómo las intruducciones de implicación, las marcadas con el subíndice $2 $ y $3 $ se utilizan aquí. Tal y como yo lo entiendo, la introducción de la implicación se utiliza cuando tenemos una derivación de, por ejemplo $\phi $ a $\psi $ podemos descargar la suposición de $\phi $ y concluye $(\phi \to \psi )$ . Pero aquí la derivación antes de la indruducción de la implicación $2 $ no comienza con $\top $ y la derivación que termina en $\top $ antes de la introducción de la implicación $3 $ no comienza con $\neg \bot $ . ¿Qué significa esto?

Gracias de antemano.

Answer 1

El primer paso ( $\rightarrow I_1$ : arriba a la izquierda) es :

i) $\bot$ --- asumido

ii) $\bot \vdash \bot$

iii) $\vdash \bot \rightarrow \bot$ --- de ii) por $\rightarrow$ -Introducción

iv) $\vdash \lnot \bot$ --- a partir de iii) por abreviatura : $\lnot P := P \rightarrow \bot$ .

---

El segundo paso ( $\rightarrow I_2$ : abajo a la izquierda) es sólo una aplicación "engañosa" de $\rightarrow$ -Introducción : $A \vdash B \rightarrow A$ .

Para comprobar que es correcto, podemos utilizar la función Estilo Hilbert versión de lógica proposicional .

Es un hecho conocido que $A \rightarrow (B \rightarrow A)$ es un válido ley lógica (en la lógica clásica, es una tautología ).

Intuitivamente, es así porque, si $A$ es verdadero, entonces el condicional $B \rightarrow A$ también es cierto.

En el Estilo Hilbert versión de cálculo proposicional esta fórmula suele ser una axioma .

Así, desde $\vdash A \rightarrow (B \rightarrow A)$ si asumimos que $A$ , entonces por modus ponens podemos derivar : $B \rightarrow A$ .

El mismo hecho se puede "traducir" en Deducción natural con la posibilidad de "descargar" una fórmula $B$ lo que sea con una aplicación de $\rightarrow$ -Introducción :

$$\frac{A}{B \rightarrow A}$$

Conclusión: aplícalo con $\lnot \bot$ como $A$ y $\top$ como $B$ para obtener :

$$\frac{\lnot \bot }{\top \rightarrow \lnot \bot} (\rightarrow I_2)$$

Lo mismo para la parte superior derecha, con $(\rightarrow I_3)$ .

---

Nota

Para una explicación, véase Jan von Plato, Elementos de razonamiento lógico (2013), página 22 :

Hay un caso límite de una derivación en la que una suposición $A$ está hecho. Es al mismo tiempo una derivación de la conclusión $A$ de la suposición $A$ como en:

1. $A$ : hipótesis

2. $A \rightarrow A$ : 1, $\rightarrow$ -I

En términos de la relación de derivabilidad, la hipótesis de la línea 1 puede escribirse como $A \vdash A$ y la línea 2 como $\vdash A \rightarrow A$ .

Considere como otro caso $\vdash A \rightarrow (B \rightarrow A)$ . Verbalmente, si asumimos $A$ entonces $A$ se deduce bajo cualquier otro supuesto $B$ :

1. $A$ : hipótesis

2. $B \rightarrow A$ : 1, $\rightarrow$ -I

3. $A \rightarrow (B \rightarrow A)$ : 1-2, $\rightarrow$ -I

Esto no parece especialmente agradable: Hemos cerrado un supuesto $B$ que no se hizo. Pero si decimos que se utilizó una suposición $0$ veces, la cosa empieza a parecer más razonable. [...] podemos decir que la suposición $B$ en la derivación de $A \rightarrow (B \rightarrow A)$ se utilizó vacuamente .

En detalle, tenemos que comparar las dos derivaciones siguientes :

(A) $\vdash A \rightarrow A$

i) $A$ - asumido

ii) $A \vdash A$

iii) $\vdash A \rightarrow A$ --- de ii) por $\rightarrow$ -I.

(B) $\vdash A \rightarrow (B \rightarrow A)$

i) $A$ - asumido

ii) $B$ --- asumido

iii) $A,B \vdash A$ --- de i) y ii)

iv) $A \vdash (B \rightarrow A)$ --- de iii) por $\rightarrow$ -I

v) $\vdash A \rightarrow (B \rightarrow A)$ --- de iv) por $\rightarrow$ -I.

Answer 2

La manera formal de introducir la implicación es asumiendo primero $A$ entonces derivando algunos $B$ y a continuación introduces $A \rightarrow B$ y descarga $A$ . Puedes asumir lo que quieras (cualquier $A$ ) pero si no utiliza $A$ en la derivación se puede tomar una abreviatura informal al no asumir ninguna $A$ (ya que de todas formas no lo vas a usar) y sólo introducir $A \rightarrow$ en algún momento. Se puede hacer esto porque se puede traducir este tipo de prueba a una prueba correcta en la que primero se asume $A$ y más tarde descargarlo.