# Where is my mistake in this proof? $(A \lor B) \land (A \rightarrow C) \lor (B \rightarrow D) \rightarrow (C \lor D)$

Here is what I finished with, although the problem states that it is a tautology and not a contingency.

$$For :(A \lor B) \land (A \rightarrow C) \lor (B \rightarrow D) \rightarrow (C \lor D)$$

$W(A/true)$ $= (True \lor B) \land (True \rightarrow C) \lor (B \rightarrow D) \rightarrow (C \lor D)$ --- First condition
$\equiv True \land (True \rightarrow C) \lor (B \rightarrow D) \rightarrow (C \lor D)$ ~~~~~~ $True \lor B \equiv True$
$\equiv True \land (C) \lor (B \rightarrow D) \rightarrow (C \lor D)$ ~~~~~~ $True \rightarrow C \equiv C$
$\equiv C \lor (B \rightarrow D) \rightarrow (C \lor D)$ ~~~~~~ $True \land C \equiv C$

$X1(D/True)$ $\equiv C \lor (B \rightarrow True) \rightarrow (C \lor True)$ ~~~~~~ First condition
$\equiv C \lor (B \rightarrow True) \rightarrow True$ ~~~~~~ $C \lor True \equiv True$
$\equiv C \lor True \rightarrow True$ ~~~~~~ $B \rightarrow True \equiv True$
$\equiv True \rightarrow True$ ~~~~~~ $C \lor True \equiv True$
$\equiv True$ ~~~~~~ $True \rightarrow True \equiv True$

$X1(D/False)$ $\equiv C \lor (B \rightarrow False) \rightarrow (C \lor False)$ ~~~ ~~~ First condition
$\equiv C \lor B \rightarrow (C \lor False)$~~~~~~$B \rightarrow False \equiv \neg B$
$\equiv C \lor B \rightarrow C$~~~~~~$C \lor False \equiv C$
$\equiv C \rightarrow C$~~~~~~$C \lor B \rightarrow C \equiv C \rightarrow C$
$\equiv True$~~~~~~$C \rightarrow C \equiv True$

$W(A/False)$ $= (False \lor B) \land (False \rightarrow C) \lor (B \rightarrow D) \rightarrow (C \lor D)$ ~~~ First condition
$\equiv B \land (False \rightarrow C) \lor (B \rightarrow D) \rightarrow (C \lor D)$~~~~~~$False \lor B \equiv B$
$\equiv B \land True \lor (B \rightarrow D) \rightarrow (C \lor D)$~~~~~~$False \rightarrow C \equiv True$
$\equiv B \lor (B \rightarrow D) \rightarrow (C \lor D)$~~~~~~$B \land True \equiv B$

$X2(D/True)$ $= B \lor (B \rightarrow True) \rightarrow (C \lor True)$ ~~~ ~~~ First Condition
$\equiv B \lor True \rightarrow (C \lor True)$~~~~~~$B \rightarrow True \equiv True$
$\equiv (B \lor True) \rightarrow True$~~~~~~$C \lor True \equiv True$
$\equiv True \rightarrow True$~~~~~~$B \lor True \equiv True$
$\equiv True$ Because $True \rightarrow True \equiv True$

$X2(D/False)$ $= B \lor (B \rightarrow False) \rightarrow (C \lor False)$ ~~~ ~~~ First Condition
$\equiv B \lor (\neg B) \rightarrow (C \lor False)$~~~~~~$B \rightarrow False \equiv \neg B$
$\equiv True \rightarrow (C \lor False)$~~~~~~$B \lor (\neg B) \equiv True$
$\equiv True \rightarrow C$~~~~~~$C \lor False \equiv C$
$\equiv C$~~~~~~$True \rightarrow C \equiv C$
Contingency!?

It is supposed to come out as a tautology. I'm using Quine's method of substitution.
Edit: cleaned up

-
The priority of operators in your formula is not clear: Do you mean $((A \vee B) \wedge ((A \to C)\vee(B \to D))) \to (C \vee D)$? – Johannes Kloos Apr 18 '12 at 12:33
Also $\rightarrow$ is to mean the implication i guess? ($\Rightarrow$) and $\sim\sim\sim$ is.... just a placeholder? ($a\quad\quad\quad b$) – example Apr 18 '12 at 12:35
By the way, that formula is not a tautology: witness the assignment $A = D = 0, B = 1$. Then the resulting formula is $((0 \vee 1) \wedge ((0 \to C) \vee (1 \to 0))) \to (C \vee 0) \equiv (\neg C \to C)$, which is obviously not a tautology. Edit: It is, on the other hand, satisfiable using $C = 1$. – Johannes Kloos Apr 18 '12 at 12:43
Thanks Johannes, so it was a contingency after all! And yes, ~~~~~~ was a placeholder since I didn't know how to put it in a nice, separated format. As for the priority, that's exactly how the problem is formatted, and I just followed the order of operations, did I miss something? – CornSmith Apr 18 '12 at 13:01
@CornSmith: The priority of operations should have been defined in the book you are reading or class you are attending. Since I have seen several different contradictory standards, I would rather know which order you are using before making statements. About your calculation: You seem to be treating $\vee$ and $\wedge$ as having the same priority, which is usually not the case. Hence, your fourth calculation step (last step for W(A/true)) is incorrect; I haven't checked any further so far. – Johannes Kloos Apr 18 '12 at 13:23

There are 5 ways to unambiguously bracket the expression, as follows:

\begin{array}{cc} \text{Case 1:} & (((w \vee x) \wedge (w \rightarrow y)) \vee (x \rightarrow z)) \rightarrow (y \vee z), \\ \text{Case 2:} & ((w \vee x) \wedge ((w \rightarrow y) \vee (x \rightarrow z))) \rightarrow (y \vee z), \\ \text{Case 3:} & ((w \vee x) \wedge (w \rightarrow y)) \vee ((x \rightarrow z) \rightarrow (y \vee z)), \\ \text{Case 4:} & (w \vee x) \wedge (((w \rightarrow y) \vee (x \rightarrow z)) \rightarrow (y \vee z)), \\ \text{Case 5:} & (w \vee x) \wedge ((w \rightarrow y) \vee ((x \rightarrow z) \rightarrow (y \vee z))). \\ \end{array}

None of these are tautologies. They are FALSE precisely in the following cases:

        wxyz wxyz wxyz wxyz wxyz wxyz
Case 1: 0000 0100 1000
Case 2: 0100 1000
Case 3: 0000 1000
Case 4: 0000 0001 0010 0011 0100 1000
Case 5: 0000 0001 0010 0011 1000


where 0=FALSE and 1=TRUE.

This is a complete list of counter-examples, and they were found by Mace4 with the following code:

assign(max_models, -1).
assign(domain_size, 2).

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 * = IMPLIES
x * y = (-x) v y.

end_of_list.

formulas(goals).

(((w v x) ^ (w * y)) v (x * z)) * (y v z) = b.
% ((w v x) ^ ((w * y) v (x * z))) * (y v z) = b.
% ((w v x) ^ (w * y)) v ((x * z) * (y v z)) = b.
% (w v x) ^ (((w * y) v (x * z)) * (y v z)) = b.
% (w v x) ^ ((w * y) v ((x * z) * (y v z))) = b.

end_of_list.


I un-remarked out the case I wished to find a counter-example to, and ran Mace4 five times.

-