# Natural Deduction Proof with double quantifier (predicate logic) [closed]

Premise: (∃y)(∀x)(Px v Py)

Conclusion: ~(∀y)(~Py)

I'm starting out assuming the negation, i.e., (∀y)(~Py).

But then I'm unsure how to find a contradiction within that subderivation. Here's what I've done so far, i know it's wrong because I can't do ∃E

``````1. (∃y)(∀x)(Px v Py)       Premise
|  2. (∀y)(~Py)            Assume
|  3. ~Pa                  UI 2
|  4. (∃y)(∀x)(Px v Py)    Reiterate
|  b|  5. (∀x)(Px v Pb)    Assume
|   |  6. Pa v Pb          UE 5
|   |  7. Pb               vE 3,6
``````
• In general: for Hw problems, please show your current line of thought first. Mar 18, 2022 at 4:25
• You can expand on step 5 a bit more - think about what it means for Everything to be P, and how b relates to that. Mar 18, 2022 at 6:10
• Assume (∀y)(~Py). From premise you have (∀x)(Px v Pa) from which (Pa v Pa) from which Pa. But from assumption ~Pa. Mar 18, 2022 at 7:39

``````1. (∃y)(∀x)(Px v Py)       Premise
|  2. (∀y)(~Py)            Assume
|  3. ~Pa                  UI 2
|  4. (∃y)(∀x)(Px v Py)    Reiterate
|  b|  5. (∀x)(Px v Pb)    Assume
|   |  6. Pa v Pb          UE 5
|   |  7. Pb               vE 3,6
``````

That is a disjunctive syllogism `vS` rather than disjunction elimination `vE`. Well, if you are allowed to use that rule, you may.

However, as it stands your main issue lies in not being able to derive a contradiction. It would be best to have somehow derived `~Pb`, so...

Do not immediately use UE on an arbitrary variable (`a`). Instead, be patient and wait until you have the witness for an existential (`b`).

``````|_ 1. (∃y)(∀x)(Px v Py)        Premise
|   |_ 2. (∀y)(~Py)            Assume
|   |  3. (∃y)(∀x)(Px v Py)    Reiterate 1
|   |[b]|_ 4. (∀x)(Px v Pb)    Assume
|   |   |  5. (∀y)(~Py)        Reiterate 2
|   |   |  6. ~Pb              UE 5
|   |   |  7. Pb v Pb          UE 4
|   |   |  8. Pb               vS 6,7
:   :   :
``````