En fitch, S → (R ∨ P), P → (¬R → Q) ∴ S → (Q ∨ R)

Otro enfoque es asumir ~(Q ∨ R) como lo hice en la línea 9 a continuación. Esto lleva a una contradicción en la línea 17 para que puedas completar la otra mitad de la disyunción.

1 | (S→(R ∨ P)) Premisa
2 |_ (P→(~R→Q)) Premisa
3 | |_ S Suposición
4 | | (R ∨ P) 1,3 →E
5 | | |_ R Suposición
6 | | | (Q ∨ R) 5 ∨I
7 | | |_ P Suposición
8 | | | (~R→Q) 2,7 →E
9 | | | |_ ~(Q ∨ R) Suposición
10 | | | | |_ ~R Suposición
11 | | | | | P 8,10 →E
12 | | | | | (Q ∨ R) 11 ∨I
13 | | | | | ⊥ 9,12 ⊥I
14 | | | | ~~R 10-13 ~I
15 | | | | R 14 ~E
16 | | | | (Q ∨ R) 15 ∨I
17 | | | | ⊥ 9,16 ⊥I
18 | | | ~~(Q ∨ R) 9-17 ~I
19 | | | (Q ∨ R) 18 ~E
20 | | (Q ∨ R) 4,5-6,7-19 ∨E
21 | (S→(Q ∨ R)) 3-20 →I

Insinuación

Suponga S y derive R ∨ P de la 1ra premisa.

Ahora dos sub-pruebas, para ∨ -elim:

1) Asumir R y derivar Q ∨ R por ∨ -intro, y listo.

2) Asumir P y derivar ¬R → Q de la 2ª premisa.

Ahora usa R ∨ ¬R (Excluido Medio) para un nuevo ∨ -elim:

2.1) Asumir R y derivar Q ∨ R .

2.2) Asumir ¬R y derivar Q de ¬R → Q y luego derivar Q ∨ R .

Habiendo derivado Q ∨ R en cada caso, podemos concluir con:

S → (Q ∨ R)

por → -introducción.

Al igual que Pe, hice una prueba por contradicción... y al hacer la suposición de ~(Q v R) anteriormente en la prueba (y explotar el atajo de Fitch de permitir que se use ~ Intro mientras me deshago de la negación de la suposición), Pude afeitar algunas líneas:

Lo que para mí es realmente interesante de esta demostración es que la subdemostración que comienza con R se usa dos veces: como demostración por contradicción para inferir ~R, así como también como demostración por casos para obtener la contradicción. No ves ese tipo de cosas muy a menudo.

Aquí hay una prueba usando un comprobador de pruebas al estilo de Fitch .

Las dos primeras líneas contienen las premisas.

Dado que el objetivo es un condicional, supuse el antecedente, S , en una subdemostración que comenzaba en la línea 3. Mi objetivo era llegar al consecuente, Q v R , lo cual hice en la línea 13. Esto me permitió cumplir con la suposición y cerrar la subdemostración introduciendo un condicional para completar la demostración.

Para llegar a la línea 13, asumí la negación de ese consecuente que quería probar comenzando una nueva subdemostración. Mi objetivo era llegar a una contradicción, lo cual hice en la línea 12. Usar el silogismo disyuntivo (DS) en la línea 8 me permitió acortar la prueba de los dos casos de la disyunción en la línea 6.

---

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/