Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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?

share|improve this question
    
See if item 1 helps: math.ucsd.edu/~mshulman/math109/reviewsheetsolutions.pdf –  Amzoti Sep 21 '12 at 3:57

3 Answers 3

up vote 6 down vote accepted

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$).

share|improve this answer

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.

share|improve this answer

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.

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.