Biconditional elimination and implication elimination rules canceling statement out

artificial intelligencelogicpropositional-calculus

I'm learning about propositional logic and converting statements to conjunctive normal form. If I have a statement such as $t \leftrightarrow q$, a biconditional statement,
and I apply apply biconditional elimination to get:

$$(t \to q) \land (q \to t)$$

Then through implication elimination I get:

$$(\neg t \lor q) \land (\neg q \lor t)$$

Would I be able to eliminate both $t$ and $q$? I have $\neg t$ and $t$, which would cancel out, and same with $q$ and $\neg q$. How can I simplify this last statement further?

Best Answer

The literals you mention are in different clauses of the formula, hence they cannot be eliminated; at no point is there a conjunction of the form $a \land \neg a (\equiv 0)$ or a disjunction of the form $a \lor \neg a (\equiv 1)$.

Also, your formula cannot be simplified any further. If you were to "simplify" one of the clauses (if you simplified both, the resulting formula would only have 1 satisfying assignment while your original one had 2) by somehow replacing it with a literal, the resulting formula would be monotone (while the original one is not) and if you got rid of one of the clauses entirely the resulting formula could be satisfied by only setting one of the variables to some value and not caring about the other one (which is in contrast to the original formula which can only be satisfied by setting $t$ and $q$ to the same value).

Related Question