3

I've been stuck on this question (which uses RAA). Was wondering if somebody could help me to make sense of it?

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

Thanks

Asaf Karagila
  • 393,674
Callum P Dunne
  • 83
  • 4
  • What are you looking for exactly? A formal proof? An informal proof? Can you use the deduction theorem? – Git Gud Apr 13 '14 at 10:41
  • RAA is Reductio Ad Absurdum, more commonly known as proof by contradiction. For example, suppose we wanted to show that a statement $p$ is not true, denoted $\neg p$. Suppose that we have also the following (undischarged assumptions): ${(p \rightarrow q), (q \rightarrow r), (\neg r)}$. Then we assume that $p$ is true and deduce absurdity: – Callum P Dunne Apr 13 '14 at 10:44
  • $$p, (p \rightarrow q) \Longrightarrow q$$ and $$(q \rightarrow r) \Longrightarrow r.$$ But $(\neg r)$ is assumed, a contradiction. Therefore $p$ must be false. A formal proof such as the above would be what I'm looking to obtain. – Callum P Dunne Apr 13 '14 at 10:55

2 Answers2

2

HINT: Apply the Deduction theorem. Twice.

Asaf Karagila
  • 393,674
0

So I'm not sure which natural deduction system you're using or if you're using a sequent calculus. I use Polish notation. I'll also use lower case Latin letters than Greek letters. We want to show NEpq $\vdash$ ENpq. X-in stands for an introduction rule for connective X. X-out stands for an elimination rule for connective 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
Doug Spoonwood
  • 11,211