¿Cómo puedo probar ⊢(∀x)(Fx V ~Fx) con deducción natural?

Depende de las reglas que tenga permitido usar ...

Aquí hay una prueba usando la eliminación de doble negación:

1) ¬ (Fx ∨ ¬Fx) --- asumido [a]

2) Fx --- asumido [b]

3) Fx ∨ ¬Fx --- de 2) por ∨-intro

4) ⊥ --- de 1) y 3)

5) ¬Fx --- de 2) y 4) por ¬-intro, descargando [b]

6) Fx ∨ ¬Fx --- de 5) por ∨-intro

7) ⊥ --- de 1) y 6)

8) Fx ∨ ¬Fx --- de 1) y 7) por ¬¬-elim, descargando [a]

9) ∀x (Fx ∨ ¬Fx) --- de 8) por ∀-intro

Aquí hay una prueba formal en Fitch:

La pregunta es: ⊢(∀x)(Fx V ~Fx) ¿Cómo puedo probar esto con deducción natural?

Proporcionaré dos pruebas, una indirecta y otra directa.

La prueba indirecta utiliza conversión de cuantificadores (CQ), la regla de De Morgan (DeM), eliminación de doble negación (DNE), prueba indirecta (IP), así como reglas de introducción y eliminación.

La siguiente prueba utiliza la ley del tercero excluido (LEM). Puede parecer que eso es lo que estamos tratando de mostrar, pero la pregunta parece ser si podemos usar la regla de introducción universal dada la ley del tercero excluido.

Consulte forall x: Calgary Remix para obtener más información y ejemplos de cómo usar estas reglas.

Referencias

Editor y comprobador de pruebas de deducción natural JavaScript/PHP estilo Fitch de Kevin Klement http://proofs.openlogicproject.org/

PD Magnus, Tim Button con adiciones de J. Robert Loftis remezcladas y revisadas por Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, invierno de 2018. http://forallx.openlogicproject.org/