Supongamos que A es un conjunto de premisas de un argumento y B la conclusión de ese argumento. Demostrar que si AU {¬B} ⊢ ⊥, entonces A ⊢ B

Supongamos que A es un conjunto de premisas de un argumento y B la conclusión de ese argumento. Demuestra que si AU {¬B} ⊢ ⊥, entonces A ⊢ B. (Usa Fitch)

No tengo ni idea de por dónde empezar, ¿alguien puede ayudarme?

El símbolo de operador que usa para A (op) B no aparece en mi teléfono celular Android. ¿Puedes reescribir? Segundo, $\cup$ no es un símbolo lógico. ¿Quieres decir $A\land\no B$?
@mobileink - A es un conjunto de premisas (pero usar un tipo diferente de símbolos, como Γ , sería mejor...); por lo tanto, Γ U {¬B} es correcto: significa el conjunto "ampliado" de premisas "compuesto por" todas las fórmulas en Γ más ¬B .
@MauroALLEGRANZA: entendido, mi punto quisquilloso es que FOL no es una teoría de conjuntos. $ \Gamma, A\vdash B $ no es necesariamente sinónimo de $\Gamma\cup A\vdash B$. (Lo siento, no puedo hacer que funcione el marcado de Latex).
Está escrito de esa manera en muchos libros de texto... Véase, por ejemplo , van Dalen , Lemma 2.4.3 (g), página 35.
OP: ¿Tu pregunta es sobre cómo funcionan las pruebas de estilo de Fitch?

Respuestas (2)

Suponga que AU {¬B} ⊢ ⊥

Ahora tenemos que demostrar que A ⊢ B:

Suponga ¬B, obtenga una contradicción de la premisa A y de AU {¬B} ⊢ ⊥, y luego concluya B. (Debe completar aquí los pasos de deducción natural). Eso es todo.

Estoy de acuerdo con la respuesta de Eliran H.

Aquí hay pasos específicos usando un verificador de prueba estilo Fitch sin asumir "¬B".

La prueba utiliza introducción de disyunción (∨I), eliminación condicional (→E), explosión (X) e introducción condicional (→I). Puede encontrar más información sobre estas reglas en forall x: Calgary Remix .

ingrese la descripción de la imagen aquí


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/