Proving the negation of universal quantification

Question

Consider the following argument

∀x(R(x) ∨ S(x)), ∃x(¬R(x)) ⊦ ¬∀x(¬S(x))

My strategy is to try to prove that ∀x(¬S(x)) is a contradiction, and therefore ¬∀x(¬S(x)) must be true.

My solution so far

1. ∀x(R(x) ∨ S(x)) Premise

2. ∃x(¬R(x)) Premise

3. ¬∀x(¬S(x)) Assumption

assumption block 1

4. X0 ¬R(x0) ∃e 2
5. R(x0) ∨ S(x0) ∀e 1
6. ¬¬S(x0) ∀e 3

assumption block 2

7. R(x0) Assumption
8. ⊥ ¬e 4, 7
9. ¬S(x) ⊥e 8

end assumption block 2

Here I am stuck. I believe that it is because I don't fully grasp how the negation of quantifiers work. I know that ¬∀(¬S(x)) is equivalent to ∃xS(x), and using this equivalence I can prove the above, but as far as I am aware equivalences cannot be used in proofs.

How would one go about working with negations of quantifiers in scenarios as the one above?

Answer 1

You made a mistake in step 6. Nr. 3 is not a universal quantification, it's a negation (the ¬ is outside the ∀). Therefore, you cannot eliminate the ∀.

What you instead need to do is to eliminate the ¬. If you want to eliminate ¬ from ¬p, you assume p and then work towards a contradiction. So you get:

6. Assume ∀x(¬S(x))

Now you may eliminate ∀ on x0:

7. ¬S(x0)

This in combination with 5 gives us

8. R(x0)

But this is in contradiction with 4. Hence, the assumption in 6 was incorrect, and therefore it must hold that ¬∀x(¬S(x)).

Answer 2

Consider the following argument

∀x(R(x) ∨ S(x)), ∃x(¬R(x)) ⊦ ¬∀x(¬S(x))

My strategy is to try to prove that ∀x(¬S(x)) is a contradiction, and therefore ¬∀x(¬S(x)) must be true.

Good strategy! A Proof by Negation.

My solution so far

1. | ∀x(R(x) ∨ S(x)) Premise

2. |_ ∃x(¬R(x)) Premise

3. | |_ ¬∀x(¬S(x)) Assumption

What happened to your strategy of assuming ∀x(¬S(x)) ? This is where you should do so. Also this is where you raise the first assumption. (The first two are premises.)

3. | |_ ∀x(¬S(x)) Assumption

4. | | |_ x0 ¬R(x0) ∃e 2
5. | | | R(x0) ∨ S(x0) ∀e 1
6. | | | ¬¬S(x0) ∀e 3

No, you cannot eliminate the universal quantifier in ¬∀x(¬S(x)) to get ¬¬S(x0). Negation has precedence. That aside, since anyway, you should have assumed ∀x(¬S(x)) in line , we'll just correct line 6, and it really should have been the assumption on the block: its the witness for the universal we seek to negate.

4. | | |_ [x0] ¬S(x0) ∀e 3
5. | | | ¬R(x0) ∃e 2
6. | | | R(x0) ∨ S(x0) ∀e 1

7. | | | |_ R(x0) Assumption
8. | | | | ⊥ ¬e 5, 7
9. | | | | ¬S(x) ⊥e 8

Okay. You are setting things up for a disjunction elimination. Just leave it at line eight.

7. | | | |_ R(x0) Assumption
8. | | | | ⊥ :¬e 5, 7
9. | | | R(x0) → ⊥ :→i 7-8
10. | | | |_ S(x0) :Assumption
11. | | | | ⊥ :¬e 4, 10
12. | | | S(x0) → ⊥ : →i 10-11
13. | | | ⊥ :∨e 6, 9, 12
14. | | ⊥ :[]e 4-13
15. | ¬∀x (¬S(x)) :¬i 3-14

Answer 3

The question is: "How would one go about working with negations of quantifiers in scenarios as the one above?"

I will provide two proofs which may help answer the question. The first will be an indirect proof similar to the attempt in the OP. The second will be more direct.

Here is the first proof:

The premises are on the first two lines. On the third line I assume the negation of what I want to show to get a contradiction. I reach the desired contradiction on line 9 which leads to the completion of the proof on line 10.

On line 4 I use the second premise. On line 5 I use the first premise. These quickly generate a contradiction.

The second proof is more direct.

The first two lines are the premise. In line 3 I start the process to complete existential elimination. To do that I have to make an assumption which will be discharged on line 15 allowing existential elimination.

Using the first premise I consider the two cases "Ra" and "Sa". I want both cases to give me (1) the same result and (2) a result I can use. The result I want is "¬¬Sa". Having those double negatives allows me to introduce an existential quantifier and then with a conversion of quantifiers move one of those negations to the outside of a universal quantifier.

For more information on how these rules work, associated with the proof checker I used, see forall x: Calgary Remix.

---

References

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, Winter 2018. http://forallx.openlogicproject.org/