For my logic class I am proving the following by natural deduction: ∃x∃yPxy ⊢ ∃y∃xPxy
It is done like this. (I am not yet allowed to embed images). Please note the usage of an operator is indicated with an G.
However, my question is in the universal quantifier. I know that the deduction ∃x∃yPxy ⊢ ∀y∀xPxy is wrong, I just can't figure out why the "proof" for this doesn't hold. Can anyone explain this further?
Edit: I figured out it is due to the a and b terms being substituted also being in the assumption block. I am still a bit iffy to what this exactly means, but I will figure this out. No further answers needed.
It is due to the a and b terms being substituted on line 4 and 5 are still in assumption, as shown on line 3. Only if this assumption has been proven, the universal quantifier can be introduced (I think).