First order logic: is this tableau correct?

85 Views Asked by At

I have to show that the following formula $(∀x∀y(Px→Py)→(∀xPx∨∀x¬Px))$ is valid in the first order logic using the tableau's system. I included a picture with my attempt.

Is it correct?

Thank you.

enter image description here