En Fitch, ¿cómo se prueba “P” a partir de la premisa “(¬P ∨ Q)→P”?

En Fitch, ¿cómo se prueba “P” a partir de la premisa “(¬P ∨ Q)→P”?

Uno asume no-P y usa una prueba de Reducción al Absurdo.

|_ (~P v Q) -> P   Premise
|  |_ ~P           Assumption
|  |  :            :
|  |  :            :
|  |  :            :
|  ~~P             Negation Introduction
|  P               Double Negation Elimination

Aquí hay una manera de probar esto usando las reglas del verificador de pruebas estilo Fitch de Klement. Las reglas se describen en forallx . Ambos están disponibles en los enlaces a continuación y serían un buen material complementario para cualquier texto que esté utilizando.

Esta prueba utiliza la ley del tercero excluido (LEM). Para usar esto, tomo una declaración simple y su negación y de ambos trato de derivar el mismo resultado. Si obtengo el mismo resultado, puedo invocar la ley del tercero excluido. Aquí elegí "P" y "¬P", porque uno de estos, "P", es la meta misma.

Para "P" no necesito hacer nada más que agregar la subprueba con la suposición "P". Para "¬P" utilizo la introducción de la disyunción para obtener la línea 4 y luego la eliminación condicional en la línea 5 (modus ponens) para obtener "P". Alcancé la meta, "P", en ambos casos y así puedo descargar las dos suposiciones en la línea 2 y 3 y llegar al final de la prueba.

Referencia

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/