¿Por qué hay infinitas pruebas para cualquier tautología en la Deducción Natural?

Question

Recientemente me he encontrado con la afirmación de que hay infinitas derivaciones en la Deducción Natural para cualquier tautología dada. Intuitivamente, esto parece impar, porque hay, digamos, una manera perfectamente directa de probar 'P o no-P' (suponer P, usar la introducción de la disyunción para obtener 'P o no-P', etc). ¿Cómo podría argumentar que hay infinitas maneras de demostrar, por ejemplo, "P o no P" en la deducción natural? ¡Estoy un poco atascado aquí!

Answer 1

Porque nada le impide decir además tonterías irrelevantes durante su prueba.

Answer 2

Comentario

Los siguientes :

1) $P$ --- asumido [a]

2) $P \lor \lnot P$ --- de 1) por $\lor$ -intro

es no a derivación de $P \lor \lnot P$ porque el supuesto [a] no ha sido descargado; es una prueba de :

$P \vdash P \lor \lnot P$ .

---

Ahora, la verdadera pregunta.

Aquí hay una prueba :

1) $\lnot (P \lor \lnot P)$ --- ssumed [a]

2) $P$ --- asumido [b]

3) $P \lor \lnot P$ --- de 2) por $\lor$ -intro

4) $\bot$ --- de 1) y 3)

5) $\lnot P$ --- de 2) y 4), descargando [b]

6) $P \lor \lnot P$ --- de 5) por $\lor$ -intro

7) $\bot$ --- de 1) y 6)

8) $P \lor \lnot P$ --- de 1) y 7), por Doble negación , descargando [a].

Después del paso 6) podemos insertar un desvío: utilizar $\lor$ -eliminación para derivar $P \lor \lnot P$ de 6) (es decir, de : $P \lor \lnot P$ ) y luego seguir con el 7).

La nueva derivación es formalmente correcta y, por tanto, es una nueva derivación ("más larga") de $P \lor \lnot P$ .