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$

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

  • 2
    $\begingroup$ 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)$? $\endgroup$ – Johannes Kloos Apr 18 '12 at 12:33
  • $\begingroup$ Also $\rightarrow$ is to mean the implication i guess? ($\Rightarrow$) and $\sim\sim\sim$ is.... just a placeholder? ($a\quad\quad\quad b$) $\endgroup$ – example Apr 18 '12 at 12:35
  • $\begingroup$ 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$. $\endgroup$ – Johannes Kloos Apr 18 '12 at 12:43
  • $\begingroup$ 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? $\endgroup$ – CornSmith Apr 18 '12 at 13:01
  • 3
    $\begingroup$ @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. $\endgroup$ – 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).


% 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.



(((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.


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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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