I have to prove that using the method of analytic tableaux: {P, Q ∧ R} ⊢ P ∧ Q For that, I did such:
I hope it's understandable, I'm using my textbook syntax. What is making me confused in my proof is that $TR$ is never used, so it seems to me there's something lacking in this proof. Is it correct though? I know that each branch in a tableau has to be closed in order to prove an inference, but can I leave atoms hanging like that?
Yes, if a branch is already closed then it doesn't matter if you didn't even need to make use of everything available to achieve the result. Expanding more lines won't lead to the branch being open again, or closed-er than it already is. Only in the opposite case where you try to demonstrate that a branch can not be closed you need to ensure that you exhausted all applicable rules.