Non-Equivalence as Equivalence with Negation/Formulation 1/Reverse Implication

From ProofWiki
Jump to navigation Jump to search

Theorem

$\paren {p \iff \neg q} \vdash \neg \paren {p \iff q}$


Proof

By the tableau method of natural deduction:

$ \paren {p \iff \neg q} \vdash \neg \paren {p \iff q} $
Line Pool Formula Rule Depends upon Notes
1 1 $p \iff \neg q$ Premise (None)
2 1 $\neg \paren {p \iff \neg \neg q}$ Sequent Introduction 1 Non-Equivalence as Equivalence with Negation: Forward Implication
3 $\neg \neg q \iff q$ Theorem Introduction (None) Double Negation
4 1 $\neg \paren {p \iff q}$ Sequent Introduction 2, 3 Biconditional is Transitive