# When to Stop Simplifying a Well-Formed Formula?

I mean simplifying a wff(well-formed formula)in which, only $\lor$, $\land$, $()$and $\lnot$ are allowed, as minimizing the occurence of connective symbols( $\land$ and $\lor$).

It's self-evident that there is no need to further simplifying wffs in which each variable only occurs once, say $A \lor B \land C$.

But it seems to me some other cases, like $(\lnot A_1 \land \lnot A_2) \lor(\lnot A_1 \land \lnot A_3) \lor(\lnot A_2 \land \lnot A_3)$ can't be simplified either.

My question is what is the rule determining whether a wff can be simplified?

-
It depends. ${}$ – Qiaochu Yuan Dec 21 '12 at 2:03
You can reduce the number of connectives in that wff: it’s equivalent to $$\Big(\neg A_1\land(\neg A_2\lor\neg A_3)\Big)\lor(\neg A_2\land\neg A_3)\;.$$ – Brian M. Scott Dec 21 '12 at 2:08
@BrianM.Scott: Thank you. That's quite a glaring mistake. – Metta World Peace Dec 21 '12 at 2:13
You’re welcome. And no, I don’t offhand know of an algorithm for determining whether you’ve reached the minimum possible number of connectives. – Brian M. Scott Dec 21 '12 at 2:15
Not an answer, but mildly apropos. In logic design, a broad goal used to be to minimize the number of operators ($\land, \lor$, etc.) involved in a wff as these were 'expensive'. Nowadays, design focuses more on reducing the 'depth' of a wff as speed is more of an issue. Simplicity is in the eye of the beholder. – copper.hat Dec 21 '12 at 2:36