Disjunctive normal form of (¬(p → q) → (q ∧ ¬r))

I learning how to convert to disjunctive normal forms, I have the following,

(¬(p → q) → (q ∧ ¬r))


I understand any p→q can be represented as (¬p)∨q, therefore if I image the above as just that I can break each section down, resulting in:

1. p → q == (¬p)∨ q, therefore (¬(p → q) == ¬((¬p) ∨ q
2. ¬((¬p) ∨ q → (q ∧ ¬r)) == ¬(¬((¬p)∨q)) ∨ (q ∧ ¬r )

Therefore the disjunctive form is:
¬(¬((¬p)∨q)) ∨ (q ∧ ¬r )


The truth table for this seems to match, is this correct? I have a feeling I have left a step out, maybe repetition of the NOT could be fixed?

• @RodrigodeAzevedo from my textbook "Any logical expression can be written as the sequence of or's of its min-terms. A min-term is an and of all the input variables. An expression written in this form is said to be in disjunctive normal form." – Ari Victor May 12 at 8:09
• Yes, the repetition of two NOTs can be cancelled : $\lnot (\lnot \varphi) \equiv \varphi$. – Mauro ALLEGRANZA May 12 at 8:11

$$\neg(p\Rightarrow q) \Leftrightarrow \neg(\neg p\vee q)$$

and so

$$\neg(p\Rightarrow q) \Rightarrow (q\wedge \neg r)$$

is equivalent to

$$\neg(\neg(\neg p\vee q)) \vee (q\wedge \neg r)$$

is equivalent to

$$(\neg p\vee q)\vee (q\wedge \neg r)$$

is equivalent to

$$\neg p\vee q \vee (q\wedge \neg r)$$.

By absorption $$a\vee (a\wedge b) \Leftrightarrow a$$, it is equivalent to

$$\neg p\vee q$$.

Using SymPy:

>>> from sympy import *
>>> p, q, r = symbols('p q r')
>>> phi = Not(p >> q) >> (q & Not(r))


Converting to DNF and simplifying:

>>> to_dnf(phi, simplify=False)
q | ~p | (q & ~r)
>>> to_dnf(phi, simplify=True)
q | ~p


Hence, we have the DNF formulas

$$q \vee \left(q \wedge \neg r\right) \vee \neg p \equiv q \vee \neg p$$