= Solution
Apply the <propositional substitution> simultaneously to the atomic variables:
$$
\varphi S=\bigl((X\lor Y)\land(X\lor\neg Y)\bigr)
\lor\bigl((Y\to X)\to\neg X\bigr).
$$
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 \b[$\varphi S\equiv X\lor\neg X\equiv\top$], a <tautology>.
Back to article page
