Sobre la justificación de la introducción de la negación

Question

En para todos x: Calgary, por P. D. Magnus , sección 16.6 p. 153, aparece esta prueba de deducción natural utilizando el estilo Fitch:

La línea 8 no debería ser Prueba indirecta porque no está introduciendo una negación?

Answer 1

Tienes razón, según sus definiciones, debería ser IP. En el desarrollo de la prueba en las páginas anteriores, en realidad tiene $IP$ en lugar de $\neg I$ en la última línea, por lo que el $IP$ etiqueta en la prueba final es probablemente un error tipográfico.

Dicho esto, se puede definir $IP$ en términos de $\neg I$ pero con un paso adicional, la eliminación de la doble negación ( $DNE$ ):

m   | | ¬A
    | |---
    | | ...
n   | | ⊥
n+1 | ¬¬A    (¬I, m-n)
n+2 | A      (DNE, n+1)

donde $DNE$ significa pasar de $\neg \neg A$ a $A$ .

Pero como $DNE$ es un paso de inferencia adicional (implícito) que no es válido en todas las lógicas que tienen $\neg I$ (es decir, en la lógica intuicionista), no hay que confundir $IP$ con $\neg I$ y no lo hacen en sus definiciones de reglas, por lo que se trata de una incoherencia, y probablemente de un error.