I don't mean to come across as rude, but there's a lot you've got wrong in your answer. Main point, AT test for validity is a Semantic method, and, weirdly given your answer, it breaks formulae down into component parts and assigns Truth values in all the relevant ways Truth values can be assigned - we just read up from the end of a branch. The only thing it doesn't do is provide a specific IQLI if an open branch exists. To be valid there can't exist any open branch - any way to have true premises and a false conclusion. As a proof method it uses completeness. (1/2)

"Formal" is likely to be confusing because it means different things in logic and maths. More importantly, semantics is about assigning truth. The meaning that is carried in QL, though relative to an interpretation, is truth. More, to be a valid form, it has to be valid across all aprt domains. IMO your "arbitrary choice", tho not wrong in result, buries this. Last, the OP basically asked for the validity decision procedure for QL, which is definitely AT, and this fact will be reflected in any textbook the OP goes onto read. It's important, IMO, that they can find more info on their own (2/2)

@Mees de Vries, the OP asked for the decision procedure for deciding Semantic validity in predicate logic, they literally give a truth table as an example of what they're looking for. Furthermore, this answer wrongly states that Semantic Tableux is a syntactic method, then goes on to basically use ST - umsu.de/trees/…

OP nowhere asked for an algorithmic decision procedure, they asked for an example of a proof.

One could argue about how directly "semantic" the truth table method and the tableau method are as opposed to e.g. natural deduction, but the tableau method definitely can be classified as a calculus in the sense that it is a fully formalized system with a fixed set of rules operating purely on symbols without making explicit reference to structures. Yes, one neat thing about tableaus is that we can read off counter models from open branches, and of course the truth conditions are reflected in the rules, that's why it's sound, but that doesn't make it a purely semantic/non-syntactic method.

@lemontree, they didn't ask for a proof - they asked how to prove, in general, that a sequent is semantically valid/invalid in QL, and gave an example of a decision procedure as the sort of thing they were looking for. ST

Yes, and this proof can be carried out either informally or formally. I gave the first and you gave the second; both are kinds of proofs, and hence also why I clarified in my answer what is meant by "formal" and "informal" proof.

And I absolutely did not "go on to basically use ST", my answer has nothing to do with tableaus apart from the fact that I mentioned one could achieve the same results with it. The fact that the tableau calculus exists and is sound and complete doesn't make a purely argument-based proof wrong at all.

@Lemontree, first, b/c of the shortness of the comments I feel I'm coming off as really rude here, and I don't mean to be, but you're still wrong. The dev rules for ST are for breaking down sequents into component parts and assigning truth to those parts w/o a specific interpretation - it does what you've done in your answer in a mechanical way (I linked to the ST ver of your first ex in a prev comment). Syntactic methods otoh are grammar rules for changing the form - semantic truth isn't a part of it. A Truth Tree also doesn't take a formula and transform it into another 1

@lemontree, I haven't said your proof was wrong. I said that ST isn't a semantic method. Also, umsu.de/trees/… - how isn't this basically a diagram of your first example? UIN gives an arbitrary name, dev rules for disjunction give proof by cases, leads to it being impossible for premises to be true and conclusion false, can read off model.

@lemontree, a syntactic proof would have taken the premise only and transformed it via inference rules - grammar rules. It doesn't matter if we did it formally or informally. It doesn't take the whole argument and decide if its valid or not

I know very well what the tableau calculus is, and I know for sure that I didn't use it. A tableau does the argumentation mechanically, I did not, that's precisely why my answer is not about some algorithmic decision procedure, and that dosen't make me wrong in any way. An informal proof is a proof, period. None of our answers is wrong, the only thing to argue about is whether this is the answer that OP is looking for, and since nothing in their post clearly indicates that they is only interested in one of them or is even aware of the distinction, ...

... I would like to end this discussion here and wait for the OP to decide which of our answers (if not both) is useful to them.

@lemontree, again - claiming that ST is a syntactic method is incorrect, but we're just talking past each other at this point.

@Lemotree, would you be OK if I asked what others think about whether Semantic Tableux is a Semantic method? I'd like to use your comment if that's OK? But I don't want it to come across as some silly game of one-upmanship, I just want to see what others think.

Sure, go ahead. (As I said, I do think one can view tableaus as more semantic, in a way, than other proof methods; the distinction "syntactic"/"semantic" is common but not very precise in various respects.)

Test to see if I can post

It wasn't letting me post :( This is the question I'm going to ask - pastebin.com/ZQhCFiW3 As its got so long, would it be possible for you to post what you've written as an answer? I've got a really busy day today, so I'm not sure I'll be able to post it today. I can also just link to the question and the chat if you'd prefer?