Pregunta de Reductio Ad Absurdum

Question

Me he atascado en esta pregunta (que utiliza RAA). Me preguntaba si alguien podría ayudarme a darle sentido.

$$\{\neg (\phi \leftrightarrow \psi )\} \vdash ((\neg \phi )\leftrightarrow \psi )$$

Gracias

Answer 1

SUGERENCIA: Aplicar el teorema de la Deducción. Dos veces.

Answer 2

Así que no estoy seguro de qué sistema de deducción natural estás usando o si estás usando un cálculo secuencial. Yo uso Notación polaca . También utilizaré letras latinas en minúsculas en lugar de letras griegas. Queremos mostrar NEpq $\vdash$ ENpq. X-in significa una regla de introducción para el conectivo X. X-out significa una regla de eliminación para el conectivo X.

  1      NEpq assumption
  2 |    Np hypothesis
  3 ||   Nq hypothesis
  4 |||  p hypothesis
  5 |||| Nq hypothesis
  6 |||| KpNp 4, 2 K-in
  7 |||  q  5-6 RAA
  8 ||   Cpq 4-7 C-in
  9 |||  q hypothesis
 10 |||| Np hypothesis
 11 |||| KqNq 9, 3 K-in
 12 |||  p 10-11 RAA
 13 ||   Cqp 9-12 C-in
 14 ||   Epq 8, 13 E-in
 15 ||   KEpqNEpq 1, 14 K-in
 16 |    q 3-15 RAA
 17      CNpq 2-16 C-in
 18 |    q hypothesis
 19 ||   NNp hypothesis
 20 |||  Np  hypothesis
 21 |||  KNpNNp 20, 19 K-in
 22 ||   p   20-21 RAA
 23 |||  q hypothesis
 24 |||| p hypothesis
 25 |||  Cpp 24-24 C-in
 26 |||  p  25, 22 C-out
 27 ||   Cqp 23-26 C-in
 28 |||  p hypothesis
 29 |||| q hypothesis
 30 |||  Cqq 29-29 C-in
 31 |||  q 18, 30 C-out
 32 ||   Cpq 28-31 C-in
 33 ||   Epq 27, 32 E-in
 34 ||   KEpqNEpq 1, 33 K-in
 35 |    Np 19-34 RAA
 36      CqNp 18-35 C-in
 37      ENpq 17, 36 E-in