# Talk:Negation normal form

WikiProject Mathematics (Rated Stub-class, Low-priority)
This article is within the scope of WikiProject Mathematics, a collaborative effort to improve the coverage of Mathematics on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.
Mathematics rating:
 Stub Class
 Low Priority
Field: Foundations, logic, and set theory

## Syntax

$\lnot (\forall x. G) \to \exists x. \lnot G$
$\lnot (\exists x. G) \to \forall x. \lnot G$

Thank you, --Abdull (talk) 14:00, 19 June 2008 (UTC)

I believe that it means that what is on the left side of the implication ( $\lnot (\forall x. G)$ ) can be rewritten as what is on the right side of the implication ( $\exists x. \lnot G$ ). This is correct, but it took me a lot of time to understand that this is what it means, because I never saw that someone uses implication for that. Usually people use logical equivalence, $\equiv$ for this. I suggest that we change the in the article
$\lnot (\forall x. G) \to \exists x. \lnot G$

into

$\lnot (\forall x. G) \equiv \exists x. \lnot G$

-- Obradović Goran (talk 15:42, 3 September 2008 (UTC)

I would propse $\Rightarrow$ or $\rightsquigarrow$ because we are describing a transformation of the formula, the equivalences you suggest is the reason that this transformation is safe. Taemyr (talk) 13:35, 9 September 2008 (UTC)
Actually, I note that $\to$ is used at term rewriting. It's perhaps best to leave it as is unless a standard is adopted that another symbol should be used. Taemyr (talk) 13:43, 9 September 2008 (UTC)

I think that using $\Rightarrow$ would be really bad, because then it would be virtually impossible to figure out where one formula stops and another starts since $\Rightarrow$ is FOL connective as well (at least, in numerous books that symbol is used for logical implication).

How about using this approach. Look at this Artificial intelligence book (it's in Serbian, but it will illustrate my point). On the page 55 is given the PRENEX algorithm (very similar to the NNF algorithm). Steps 1 and 2 are: As long as possible, apply the following logical equivalences. We could say the same in this article. Mathematician would understand what it means (current solution is confusing), and we could have additional explanation for the non-mathematician.

So, my suggestion is: As long as possible, apply the following logical equivalences (i.e. rewrite left side of the formula with the right side). But then again, if this ($\to$) notation is used in the other articles as well.. -- Obradović Goran (talk 04:44, 15 September 2008 (UTC)