Language: consider propositional logic over the connectives $\land$, $\lor$, and $\lnot$.
Consider a propositional formula $\phi$ which contains at least one negation symbol and is neither a contradiction nor a tautology. We are also given that no negation symbols can be cancelled in $\phi$ by any valid biconditional such as $$\alpha \land (\lnot \alpha \lor \beta) \iff \alpha \land \beta$$ $$\lnot \lnot \alpha \iff \alpha$$
Now let's push negation inward to reduce $\phi$ to negation normal form and call that normal form $\phi'$. Just to be clear, $\phi \iff \phi'$.
Can we conclude that $\phi'$ also contains at least one negation symbol? If not, please provide a counterexample.
EDIT: The allowable biconditionals were clarified to include any valid biconditional that would cancel a negation. The intention is to capture the notion that $\phi$ contains no cancellable negations.
Sorry to be snarky, but if the original contains at least one negation, and if you are not allowed to cancel negations using any equivalence laws, then yes, the result will have at least one negation.
So, it's either that simple .... or you should really clear up what you mean by 'no negation symbols can be cancelled by [some equivalence principles] and the like'
I mean, $A \land ( B \lor \neg B)$ is equivalent to $A$, so it is neither a tautology nor a contradiction ... but clearly one has to use an equivalence that 'cancels a negation'. So, does this equivalence fall under 'the like'? When, indeed, would some equivalence not fall under 'the like'? What, in sum, is one allowed to use and what not?
Now, one clue may be when you say that you 'push in negation' to get it to NNF ... now, typically one only uses DeMorgans and Double Negations to do so ... and since Double Negations were explicitly rules out, that leaves us with DeMorgans. So, is the question whether or not we can eliminate all negations if we only can use DeMorgans to push negations inside? If so, the answer is clearly no: when we push the negation inside it doesn't disappear.