Con una premisa que $p \implies q$ ¿cómo esta prueba del sistema Fitch "prueba" que $\neg q \implies \neg p$ ?

Question

Estoy teniendo problemas para "sentir" las pruebas del sistema Fitch. Me sorprendió la resolución de este problema en la clase de Lógica de Stanford utilizando su motor de sistema Fitch.

Parece trivialmente obvio que $(\phi \implies \psi) \models (\neg \psi \implies \neg \phi)$ en el sentido de que dada la premisa de que "si $\phi$ entonces $\psi$ ", entonces, si se da el caso de que hay $\neg \psi$ entonces esto implica que debe haber $\neg \phi$ . Las tablas de la verdad lo confirman $(\phi \implies \psi) \equiv (\neg \psi \implies \neg \phi)$ :

| $p$ | $q$ | $\neg q$ | $\neg p$ | $p \implies q$ | $\neg q \implies \neg p$ |

T | T| F | F |    T    |     T     |  
T | F| T | F |    F    |     F     |  
F | T| F | T |    T    |     T     |  
F | F| T | T |    T    |     T     |  

No acabo de entender cómo esta prueba del sistema Fitch lo "demuestra":

1) $p \implies q$ --------Premisa
2) | $\neg q$ --------------Assumption
3) | | $p$ --------------Assumption
4) | | $\neg q$ ------------Reiteración, 2
5) | $p => \neg q$ -------Implicación Introducción: 3, 4
6) | $\neg p$ --------------Negation Introduction: 1, 5
7) $\neg q \implies \neg p$ ----Implicación Introducción: 2, 6

Entiendo que estoy negando una contradicción para derivar $\neg p$ pero no entiendo muy bien cómo el sistema Fitch demuestra esto como una prueba concluyente (digamos en comparación con la evaluación de la tabla de verdad).

Estoy confundido en un par de puntos.

1. ¿Estoy usando $\models$ y $\equiv$ ¿correctamente?
2. ¿Por qué el segundo supuesto aumenta el "nivel" de subprueba?
3. ¿Es la reiteración una mera maniobra de puesta en escena, es decir, la introducción de la implicación es siempre tal que la prueba de Fitch traduce "de arriba abajo" en una implicación "de izquierda a derecha"?
4. ¿por qué es necesario reiterar la 2?
   es decir, ¿por qué esto:
   1) p => q ------Premisa
   2) | ~q --------Asunción
   3) | | p --------Asunción
   ...resultan en esto:
   4) | p => p ----Implicación Introducción: 3, 3
   ...cuando selecciono 2 y 3 para la introducción de la implicación?
5. Me gusta hacer divisiones largas, pero Fitch me parece un rococó división larga. Donde las tablas de la verdad pueden convertirse rápidamente en algo parecido a hacer divisiones largas con números romanos, la elegancia de Fitch no es tan evidente cuando se trabaja con $2^2$ ¿valores de verdad?

Answer 1

Comentarios

1) Sí: podemos decir que la tabla de verdad "demuestra" $\vDash$ por qué el "cálculo" (como la Deducción Natural, el sistema de prueba implementado en Fitch) "prueba" $\vdash$ .

2) El "sangrado" de las subpruebas es una forma de mantener un registro de las suposiciones y del modo en que qué depende de qué. Así, la subprueba interna depende tanto de la suposición 3) como de la suposición 2).

3) Sí; la reiteración no es "formalmente" necesaria. Si "ejecutamos" la derivación a mano utilizando papel y lápiz, podemos comprobar visualmente que después del paso 3) la hipótesis 2) "sigue ahí" y no nos vemos obligados a reescribirla.

4) La reiteración de $\lnot q$ bajo el supuesto $p$ para utilizar $\to$ -intro para derivar $p \to \lnot q$ no es estrictamente necesario.

En Deducción Natural, un uso correcto de $→$ -intro es: de $q$ derivar $p → q$ para $p$ lo que sea.

La inferencia es válida porque, suponiendo $q$ (es decir, que $q$ es verdadero ), tenemos que, por la tabla de verdad para el condicional, $p→q$ debe ser cierto.

Supongo que este "movimiento" no está implementado en Fitch, y por lo tanto el sistema necesita la reiteración.