Silogismo disyuntivo en un sistema de estilo Fitch

Aquí hay un par de opciones:

• Si tiene una regla de doble negación, puede convertir B en ~~B. Entonces puedes usar una regla de silogismo disyuntivo junto con (~C v ~B) para obtener ~C.

• Puede intentar una prueba indirecta, donde asume C, y luego la une con B para obtener (C & B), lo que produce una contradicción con la línea 2, lo que implica ~C.

Aquí hay un enfoque que usa la eliminación disyuntiva. Dado lo siguiente, asumo que las reglas de DeMorgan están disponibles:

Puedo expandir ~(C & B) a ~C O ~B

En la línea 3, utilicé las reglas de DeMorgan (DeM) para obtener una disyunción que luego tendré que eliminar para alcanzar la meta.

Para eliminar la disyunción, tengo que considerar ambas disyunciones, "¬C" y "¬B".

La primera disyunción es la más fácil, pero puede resultar confusa porque es muy fácil. La suposición, "¬C", para esa subdemostración es precisamente lo que quiero mostrar. No hay nada más que hacer (al menos para este comprobador de pruebas).

La segunda disyunción usa explosión basada en la observación de que las líneas 1 y 5 son contradictorias. Este comprobador de pruebas me permite declarar la contradicción (⊥) en la línea 6 y usar la explosión (X) en la línea 7 para llegar a la conclusión de que quiero "¬C". El que está utilizando puede requerir algo diferente.

Como tengo la misma conclusión para cada disyunción, puedo cumplir con las dos suposiciones de las líneas 4 y 5 citando la regla de eliminación de disyunciones (∨E). En este comprobador de prueba, tengo que hacer referencia a la disyunción en sí (3), la primera subprueba (que es solo la línea 4 pero está escrita como un rango 4-4) y la segunda subprueba (5-7).

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/

Te han prometido B y ~(C ^ B). Si asume C, puede derivar C ^ B de la primera premisa, contradiciendo la segunda premisa, lo que le permite cumplir con la suposición mediante la introducción de la negación y, por lo tanto, deducir ~C según sea necesario. Eso es todo.

|  B           Premise
|_ ~(C ^ B)    Premise
|  |_ C        Assumption
|  |  C ^ B    Conjunction Introduction
|  |  #        Negation Elimination
|  ~C          Negation Introduction

Bueno, la versión de la regla de introducción de negación que emplea su sistema puede variar, pero eso es básicamente todo.

|  B           Premise
|_ ~(C ^ B)    Premise
|  |_ C        Assumption
|  |  C ^ B    Conjunction Introduction
|  C->(C ^ B)  Conditional Introduction
|  |_ C        Assumption
|  |  ~(C ^ B) Reiteration
|  C->~(C ^ B) Conditional Introduction
|  ~C          Negation Introduction