Is the following derivation correct for a set of well-formed formulae?

Question

Let $PF$ be the set of well-formed formulae. Define $\operatorname{flip}\colon PF\rightarrow PF$ recursively as follows:

$\operatorname{flip}(\top) = \top; \operatorname{flip}(\bot) = \bot;$

$\operatorname{flip}(p) = \lnot p$ for all $p \in PF$

$\operatorname{flip}(\lnot \phi) = \lnot \operatorname{flip}(\phi)$

$\operatorname{flip}(\phi \land \psi) = (\operatorname{flip}(\phi) \land \operatorname{flip}(\psi))$

$\operatorname{flip}(\phi \lor \psi) = (\operatorname{flip}(\phi) \lor \operatorname{flip}(\psi))$

---

Let $\phi = ((p\land \lnot q) \lor \top)$

What is $\operatorname{flip}(\phi)$?

Here's what I've done:

$\operatorname{flip}(\phi) = (\operatorname{flip}(p \land \lnot q) \lor \operatorname{flip}(\top))$

$= (\operatorname{flip}(p\land \lnot q) \lor \top)$

$= ((\operatorname{flip}(p) \land \operatorname{flip}(\lnot q)) \lor \top)$

$= ((\lnot p \land \lnot \operatorname{flip}(q)) \lor \top)$

$= ((\lnot p \land \lnot \lnot q) \lor \top)$

$= ((\lnot p \land q) \lor \top)$

Is this derivation correct? A bit unsure about the end there.

Answer 1

The end is indeed not quite correct. The formula you should end up with is $((\neg p \lor \neg \neg q) \land \top )$, i.e. the second to last formula of your derivation.

You should not have taken that last step. While removing the double negation gives you a logically equivalent formula, it is not the same formula.