# What are the legal quantifier negation rules?

Is using Quantifier Negation to flip two quantifiers at once legal in symbolic logic?

Example:

1. ~∀x∀y(Hhx & Hhy)

2. ƎxƎy~(Hhx & Hhy) 1 QN

Or do I need to do this in 2 steps?

Example:

1. ~∀x∀y(Hhx & Hhy)

2. Ǝx~∀y(Hhx & Hhy) 1 QN

3. ƎxƎy~(Hhx & Hhy) 2 QN

• The result of two steps is the same as the result of both in one, so it is correct. How much you have to show your steps depends on your teacher's requirements. Sep 2, 2019 at 2:51
• Right - I knew that they were essentially the same, I just wasn't sure what symbolic logic conventions would typically have me do (as I know many other "step skipping" moves are "illegal" according to conventions, even if they always give the same result). I'm just doing this for fun, not for a class, so I can't ask my teacher what his personal requirements are unfortunately. :)
– Lily
Sep 2, 2019 at 3:38
• There are no universal conventions. When using predicate calculus, people would move negation across all the quantifiers in one step, and sometimes even apply the de Morgan laws inside the formula in the same step. If you are using a particular proof system, like the natural deduction, each step has to correspond to a specific inference rule (although experts might skip obvious steps). But it is unclear what your framework is. Are you following some book? Sep 2, 2019 at 4:04
• Thank you! :D Makes sense. In response to your question, I initially learned Quantifier Negation from the book Introduction to Logic by Richard Arthur, but right now I'm just kind of doing deductions for fun.
– Lily
Sep 2, 2019 at 13:52

The way the inference rules are defined determines how one can use them. For example, in the proof checker associated with the forallx logic textbook, it would take two steps.

The inference rules there are called "conversion of quantifiers", abbreviated "CQ". See chapter 34, pages 279-281 in the text.

If I tried to take both steps at once in the proof checker, I would get this error:

This makes sense because none of the four CQ rules allows me to make that inference.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Fall 2019. http://forallx.openlogicproject.org/forallxyyc.pdf

• Thank you! I will make a habit of doing it the two-step way :)
– Lily
Sep 2, 2019 at 3:42