# Non-Equivalence as Equivalence with Negation/Formulation 1/Forward Implication/Proof

Jump to navigation
Jump to search

## Theorem

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

## Proof

By the tableau method of natural deduction:

$\blacksquare$

#### Law of the Excluded Middle

This proof depends on the Law of the Excluded Middle.

This is one of the axioms of logic that was determined by Aristotle, and forms part of the backbone of classical (Aristotelian) logic.

However, the intuitionist school rejects the Law of the Excluded Middle as a valid logical axiom.

This in turn invalidates this proof from an intuitionistic perspective.

This article needs proofreading.Please check it for mathematical errors.If you believe there are none, please remove `{{Proofread}}` from the code.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Proofread}}` from the code. |

Although this article appears correct, it's inelegant. There has to be a better way of doing it.In particular: I was tired when I posted this up so probably missed out on some obvious usage of Properties of Biconditional that would make this considerably easier. If you find such, then (unless there are blatant flaws in the above) feel free to add them as new proofs.You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by redesigning it.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Improve}}` from the code.If you would welcome a second opinion as to whether your work is correct, add a call to `{{Proofread}}` the page. |