 Solution

ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2023/digital-systems-linear-algebra-and-introduction-to-formal-proof/7/c/solution

Apply the propositional substitution simultaneously to the atomic variables:

φS = ((X \lor Y) \land (X \lor \neg Y)) \lor ((Y \to X) \to \neg X) .

By distributivity and the complementary literals

Y, \neg Y

(X \lor Y) \land (X \lor \neg Y) \equiv X .

The other disjunct simplifies using logical implication and absorption:

(Y \to X) \to \neg X \equiv \neg (\neg Y \lor X) \lor \neg X \equiv (Y \land \neg X) \lor \neg X \equiv \neg X .

Thus $φS \equiv X \lor \neg X \equiv ⊤$ , a tautology.

 New to topics? Read the docs here!