Can anyone help me prove this theorem via natural deduction for my class?


I can solve one side of the biconditional quite easily using conditional derivation, but have no idea how to solve the other way. Below is my proof for one direction of the biconditional.

Incomplete Proof

I am not allowed to use any other theorems in my proof (De Morgan's Laws etc.) The only tools we are allowed to use are: modus ponens, modus tollens, disjunctive syllogism, addition, adjunction, conditional derivation, indirect derivation/reductio, bicondition, reiterate/repeat.

The language used is from DeLancey's "A Concise Introduction to Logic": https://milnepublishing.geneseo.edu/concise-introduction-to-logic/front-matter/about-the-textbook/

Any geniuses who want to give this a crack?

  • $\begingroup$ I think this question should be reopened. The answers in that similar post don't use natural deduction, which is the formalism required here. $\endgroup$ Apr 20 at 9:23

1 Answer 1


$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\iff{\leftrightarrow}$ You wish to derive $~\neg(P\iff Q)\vdash P\iff\neg Q~$.

So you shall want to introduce that biconditional, which shall require indirect and reduction proof, enabled by contradicting the premise.

$\qquad\fitch{\neg(P\iff Q)}{\fitch{P}{\fitch{Q}{~\vdots\\P\iff Q\\\neg(P\iff Q)}\\\neg Q}\\\fitch{\neg Q}{\fitch{\lnot P}{~\vdots\\P\iff Q\\\neg(P\iff Q)}\\P}\\P\iff\neg Q} $

  • $\begingroup$ Thanks so much for the help! Just a few follow up questions. What does ⋮ mean? What does ⊥ mean? Also is ⊢ just indicating a conditional, like ->? $\endgroup$ Apr 19 at 7:39
  • $\begingroup$ Ah. In many natural deduction systems, $\bot$ is the symbol for contradiction (also called 'bottom', 'falsity' or similar names). It looks like your system just uses two contradictory statements, so just reiterate the assumed $\lnot(P\leftrightarrow Q)$ at that point. $\endgroup$ Apr 20 at 9:02
  • $\begingroup$ $\vdash$ is the symbol for "syntactic entailment". $\phi,\ldots,\psi\vdash \chi$ says, "from the list of assumptions , $\phi,\ldots,\psi$, you can derive $\chi$". $\endgroup$ Apr 20 at 9:11
  • $\begingroup$ $~\vdots~$ is a vertical ellipsis; just indicating missing derivation for you to complete on your own. This is merely a skeleton of a proof to get you started. @milfordcubicle2 $\endgroup$ Apr 20 at 9:12

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .