Material Equivalence

From ProofWiki
Jump to: navigation, search

Contents

Theorem

  • $p \iff q \dashv \vdash \left({p \land q}\right) \lor \left({\neg p \land \neg q}\right)$
  • $p \iff q \dashv \vdash \neg p \iff \neg q$
  • $p \iff q \dashv \vdash \left({p \lor q}\right) \implies \left({p \land q}\right)$


Alternative rendition

These can alternatively be rendered as:

  • $\vdash \left({p \iff q}\right) \iff \left({\left({p \land q}\right) \lor \left({\neg p \land \neg q}\right)}\right)$
  • $\vdash \left({p \iff q}\right) \iff \left({\neg p \iff \neg q}\right)$
  • $\vdash \left({p \iff q}\right) \iff \left({\left({p \lor q}\right) \implies \left({p \land q}\right)}\right)$

They can be seen to be logically equivalent to the forms above.


Proof

Proof by Natural Deduction

By the tableau method:


$p \iff q \vdash \left({p \land q}\right) \lor \left({\neg p \land \neg q}\right)$
Line Pool Formula Rule Depends upon
1 1 $p \iff q$ P (None)
2 1 $\left ({p \implies q}\right) \land \left ({q \implies p}\right)$ By definition 1
3 1 $p \implies q$ $\land \mathcal{E}_1$ 2
4 1 $q \implies p$ $\land \mathcal{E}_2$ 2
5 $p \lor \neg p$ LEM (None)
6 6 $p$ A (None)
7 1, 6 $q$ $\implies \mathcal{E}$ 3, 6
8 1, 6 $p \land q$ $\land \mathcal{I}$ 6, 7
9 1, 6 $\left({p \land q}\right) \lor \left({\neg p \land \neg q}\right)$ $\lor \mathcal{I}_1$ 8
10 10 $\neg p$ A (None)
11 1, 10 $\neg q$ MTT 4, 10
12 1, 10 $\neg p \land \neg q$ $\land \mathcal{I}$ 10, 11
13 1, 10 $\left({p \land q}\right) \lor \left({\neg p \land \neg q}\right)$ $\lor \mathcal{I}_2$ 12
14 1 $\left({p \land q}\right) \lor \left({\neg p \land \neg q}\right)$ $\lor \mathcal{E}$ 1, 6-9, 10-13


$\left({p \land q}\right) \lor \left({\neg p \land \neg q}\right) \vdash p \iff q$
Line Pool Formula Rule Depends upon
1 1 $\left({p \land q}\right) \lor \left({\neg p \land \neg q}\right)$ P (None)
2 2 $p \land q$ A (None)
3 3 $p$ A (None)
4 2 $q$ $\land \mathcal{E}_2$ 2
5 2 $p \implies q$ $\implies \mathcal{I}$ 3, 4
6 6 $q$ A (None)
7 2 $p$ $\land \mathcal{E}_1$ 2
8 2 $q \implies p$ $\implies \mathcal{I}$ 6, 7
9 2 $\left ({p \implies q}\right) \land \left ({q \implies p}\right)$ $\land \mathcal{I}$ 5, 8
10 10 $\neg p \land \neg q$ A (None)
11 11 $\neg p$ A (None)
12 10 $\neg q$ $\land \mathcal{E}_2$ 10
13 10 $\neg p \implies \neg q$ $\implies \mathcal{I}$ 11, 12
14 10 $q \implies p$ TP 13
15 15 $\neg q$ A (None)
16 10 $\neg p$ $\land \mathcal{E}_1$ 10
17 10 $\neg q \implies \neg p$ $\implies \mathcal{I}$ 15, 16
18 10 $p \implies q$ TP 17
19 10 $\left ({p \implies q}\right) \land \left ({q \implies p}\right)$ $\land \mathcal{I}$ 17, 13
20 1 $\left ({p \implies q}\right) \land \left ({q \implies p}\right)$ $\lor \mathcal{E}$ 1, 2-9, 10-20
20 1 $p \iff q$ By definition 19

$\blacksquare$



$p \iff q \vdash \neg p \iff \neg q$
Line Pool Formula Rule Depends upon
1 1 $p \iff q$ P (None)
2 1 $\left ({p \implies q}\right) \land \left ({q \implies p}\right)$ By definition 1
3 1 $\left ({\neg q \implies \neg p}\right) \land \left ({\neg p \implies \neg q}\right)$ TP 2
4 1 $\left ({\neg p \implies \neg q}\right) \land \left ({\neg q \implies \neg p}\right)$ Comm 3
5 1 $\neg p \iff \neg q$ By definition 4


The argument reverses:

$\neg p \iff \neg q \vdash p \iff q$
Line Pool Formula Rule Depends upon
1 1 $\neg p \iff \neg q$ P (None)
2 1 $\left ({\neg p \implies \neg q}\right) \land \left ({\neg q \implies \neg p}\right)$ By definition 1
3 1 $\left ({\neg \neg q \implies \neg \neg p}\right) \land \left ({\neg \neg p \implies \neg \neg q}\right)$ TP 2
4 1 $\left ({q \implies p}\right) \land \left ({p \implies q}\right)$ $\neg \neg \mathcal{E}$ 3
5 1 $\left ({p \implies q}\right) \land \left ({q \implies p}\right)$ Comm 4
6 1 $p \iff q$ By definition 5

$\blacksquare$



$p \iff q \vdash \left({p \lor q}\right) \implies \left({p \land q}\right)$
Line Pool Formula Rule Depends upon Notes
1 1 $p \iff q$ P (None)
2 1 $\left({p \land q}\right) \lor \left({\neg p \land \neg q}\right)$ SI 1 From above
3 1 $\left({p \land q}\right) \lor \neg \left({p \lor q}\right)$ DM 2
4 1 $\neg \left({p \lor q}\right) \lor \left({p \land q}\right)$ Comm 3
5 1 $\left({p \lor q}\right) \implies \left({p \land q}\right)$ Rule of Material Implication 4


The argument reverses:

$\left({p \lor q}\right) \implies \left({p \land q}\right) \vdash p \iff q$
Line Pool Formula Rule Depends upon Notes
1 1 $\left({p \lor q}\right) \implies \left({p \land q}\right)$ P (None)
2 1 $\neg \left({p \lor q}\right) \lor \left({p \land q}\right)$ Rule of Material Implication 1
3 1 $\left({p \land q}\right) \lor \neg \left({p \lor q}\right)$ Comm 2
4 1 $\left({p \land q}\right) \lor \left({\neg p \land \neg q}\right)$ DM 3
5 1 $\left ({p \implies q}\right) \land \left ({q \implies p}\right)$ Comm 4
6 1 $p \iff q$ SI 5 From above

$\blacksquare$


Proof by Truth Table

We apply the Method of Truth Tables to the propositions in turn.

As can be seen by inspection, in all cases the truth values under the main connectives match for all models.


$\begin{array}{|ccc||ccccccccc|} \hline p & \iff & q & (p & \land & q) & \lor & (\neg & p & \land & \neg & q) \\ \hline F & T & F & F & F & F & T & T & F & T & T & F \\ F & F & T & F & F & T & F & T & F & F & F & T \\ T & F & F & T & F & F & F & F & T & F & T & F \\ T & T & T & T & T & T & T & F & T & F & F & T \\ \hline \end{array}$

$\blacksquare$


$\begin{array}{|ccc||ccccc|} \hline p & \iff & q & \neg & p & \iff & \neg & q \\ \hline F & T & F & T & F & T & T & F \\ F & F & T & T & F & F & F & T \\ T & F & F & F & T & F & T & F \\ T & T & T & F & T & T & F & T \\ \hline \end{array}$

$\blacksquare$


$\begin{array}{|ccc||ccccccc|} \hline p & \iff & q & (p & \lor & q) & \implies & (p & \land & q) \\ \hline F & T & F & F & F & F & T & F & F & F \\ F & F & T & F & T & T & F & F & F & T \\ T & F & F & T & T & F & F & T & F & F \\ T & T & T & T & T & T & T & T & T & T \\ \hline \end{array}$

$\blacksquare$


Sources

Retrieved from "http://www.proofwiki.org/w/index.php?title=Material_Equivalence&oldid=62318"
Personal tools
Namespaces
Variants
Actions
Navigation
ProofWiki.org
ToDo
Toolbox
Google AdSense