I can prove it all the way to:
What is the proof for those two equaling?
So far I have:
(p ∨ q) = (p ^ p) ∨ (q ^ q)
Negate it…
~((p ^ p) ∨ (q ^ q))
You get…
~(p ^ p) ^ ~(q ^ q) = (p NAND p) ^ (q NAND q)
SO CLOSE! How do I continue from here?
I can prove it all the way to:
What is the proof for those two equaling?
So far I have:
(p ∨ q) = (p ^ p) ∨ (q ^ q)
Negate it…
~((p ^ p) ∨ (q ^ q))
You get…
~(p ^ p) ^ ~(q ^ q) = (p NAND p) ^ (q NAND q)
SO CLOSE! How do I continue from here?
For starters, do note that
$\text{NAND} (p_1, p_2) = \neg (p_1 \land p_2)$
Hence $\text{NAND} (p, p) = \neg (p \land p) \equiv \neg p$ because $p \land p \equiv p$. Therefore,
$ \text{NAND} (\text{NAND} (p, p), \text{NAND} (q, q)) = \text{NAND} (\neg p, \neg q) = \neg (\neg p \land \neg q) \equiv \neg\neg p \lor \neg\neg q \equiv p \lor q$
where I used one of De Morgan's laws and elimination of the double negation (i.e., $\neg \neg p \equiv p$).
Write down the truth table for $p\lor q$.
Then find the truth table for $(p\:\text{NAND}\:p)\:\text{NAND}\:(q\:\text{NAND}\:q)$ and compare. The end.
Here's a proof via the automated theorem prover Prover9: Firstly, we input the assumptions (standard Boolean logic, and define a function as NAND):
formulas(assumptions). % associativity of "or" and "and" x v (y v z) = (x v y) v z. x ^ (y ^ z) = (x ^ y) ^ z. % commutativity of "or" and "and" x v y = y v x. x ^ y = y ^ x. % distributivity x ^ (y v z) = (x ^ y) v (x ^ z). x v (y ^ z) = (x v y) ^ (x v z). % idempotence x v x = x. x ^ x = x. % absorption x ^ (x v y) = x. x v (x ^ y) = x. % a = false; b = true x v a = x. x v b = b. x ^ b = x. x ^ a = a. % negation laws x ^ (-x) = a. x v -x = b. -(-x) = x. % De Morgan's laws (-x) ^ (-y) = -(x v y). (-x) v (-y) = -(x ^ y). % define * = NAND x * y = -(x ^ y). end_of_list. formulas(goals). x v y = (x * x) * (y * y). end_of_list.
And input this into Prover9, which outputs:
============================== PROOF ================================= % Proof 1 at 0.01 (+ 0.00) seconds. % Length of proof is 9. % Level of proof is 3. % Maximum clause weight is 10. % Given clauses 0. 1 x v y = (x * x) * (y * y) # label(non_clause) # label(goal). [goal]. 11 x v x = x. [assumption]. 21 --x = x. [assumption]. 24 -x v -y = -(x ^ y). [assumption]. 25 -(x ^ y) = -x v -y. [copy(24),flip(a)]. 26 x * y = -(x ^ y). [assumption]. 27 x * y = -x v -y. [copy(26),rewrite([25(3)])]. 28 c1 v c2 != (c1 * c1) * (c2 * c2). [deny(1)]. 29 $F. [copy(28),rewrite([27(6),11(8),27(8),11(10),27(8),21(6),21(7)]),xx(a)]. ============================== end of proof ==========================
Which recovers Rod Carvalho's proof. Note: It didn't actually use most of the Boolean axioms.
On your second line, you should have double negated it to keep it the same.
~[~[(p $\wedge$ p) $\vee$ (q $\wedge$ q)]] = ~[~(p $\wedge$ p) $\wedge$ ~(q $\wedge$ q)]=~[pNANDp $\wedge$ qNANDq]
like what Rod mentioned, $p_1$ NAND $p_2$ = ~($x$ $\wedge$ $y$).
Thus,
~[pNANDp $\wedge$ qNANDq]= (pNANDp) NAND (qNANDq).