How to prove the following using logical connectivities laws?
((A or B) and (A or ~C) and (~B or ~C)) <=> ((A or B) and (~B or ~C))3 Answers
$\begingroup$Here is a direct proof where we basically keep simplifying: \begin{align} & (A \lor B) \land (A \lor \lnot C) \land (\lnot B \lor \lnot C) \;\equiv\; (A \lor B) \land (\lnot B \lor \lnot C) \\ \equiv & \;\;\;\;\;\text{"simplify $\;P \equiv P \land Q\;$ to $\;P \Rightarrow Q\;$"} \\ & (A \lor B) \land (\lnot B \lor \lnot C) \;\Rightarrow\; A \lor \lnot C \\ \equiv & \;\;\;\;\;\text{"rewrite $\;P \Rightarrow Q\;$ to $\;\lnot P \lor Q\;$, using DeMorgan"} \\ & (\lnot A \land \lnot B) \lor (B \land C) \lor A \lor \lnot C \\ \equiv & \;\;\;\;\;\text{"use negation of $\;A\;$ and $\;\lnot C\;$ on other side of $\;\lor\;$"} \\ & (\text{true} \land \lnot B) \lor (B \land \text{true}) \lor A \lor \lnot C \\ \equiv & \;\;\;\;\;\text{"simplify"} \\ & \lnot B \lor B \lor A \lor \lnot C \\ \equiv & \;\;\;\;\;\text{"excluded middle"} \\ & \text{true} \lor A \lor \lnot C \\ \equiv & \;\;\;\;\;\text{"simplify"} \\ & \text{true} \\ \end{align} Normally I would do this in three steps, but I've written it out a bit more for clarity.
$\endgroup$ $\begingroup$There are two related questions here. The first is to show that each side of the double arrow implies the other, following rules of deduction. In this interpretation, the forward direction follows immediately from the fact that $(X \wedge Y) \implies X$. For the backwards direction, it suffices, as Trevor Wilson suggests in the comments, to prove $(A \vee B) \wedge (\neg B \vee \neg C) \implies (A \vee \neg C)$. For this, note that $(X \vee \neg Y)$ is equivalent to the sentence $(Y \rightarrow X)$; then the problem to prove is equivalent to $(B \rightarrow \neg A) \wedge (C \rightarrow B) \implies (C \rightarrow A)$, which is almost surely either one of your axioms or something you proved early on.
A second interpretation is to find a series of algebraic manipulations that identify the two sides. After some toying, I don't see a clever way to do this. One non-clever way is the following. You can treat $\vee$ as "multiplication" in a ring of characteristic $2$ (meaning $+$ and $-$ are the same), and $X \wedge Y = X + Y + XY = (X+1)(Y+1)+1$. Finally, $X^2 = X$ and $\neg X = 1+X$. Substituting $D = 1+C$, the LHS is:
$ (AB + AD + ABD) + (1+B)D + (AB + AD + ABD)(1+B)D = AB + AD + ABD + D + BD + (1+B)(ABD + AD + ABD) = AB + AD + ABD + D + BD + (1+B)AD = AB + AD + ABD + D + BD + AD + ABD = AB + D + BD $
whereas the RHS is:
$ AB + (1+B)D + AB(1+B)D = AB + D + BD + ABD + ABD = AB + D + BD$.
Anyway, unpacking this final equality will in principal give you a direct proof, but it won't be short.
$\endgroup$ $\begingroup$Here is a proof using a Fitch-style proof checker:
Note that I added parentheses to the left hand side to disambiguate how the conjuncts were joined. This is not totally trivial. It put a constraint on how I would have to put these conjuncts together and remove them in constructing the proof.
The definitions of the inference rules can be found on the proof checker's page. The only one that is not an introduction or elimination rule is disjunctive syllogism (DS).
Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker
$\endgroup$
