When I first encountered the double turnstile ($\models$) in the context of an intro to logic class it was presented to me as expressing semantic validity where this was cashed out model-theoretically as truth in all models.
Are there other interpretations of the double turnstile that are not model theoretic? Are there non-model-theoretic accounts of semantic validity?
Update: In the comments to this question user18921 pointed me to game semantics. These sorts of alternative, non-model-theoretic, semantics for formal languages are the sorts of things I'm interested in here.
I think we can interpret the notion of ⊨ in a traditional philosophical manner as just meaning that the truth of the premises guarantee the truth of the conclusion. In other words, {a, ..., y}⊨z just means the truth value of {a, ..., z} gets preserved when inferring to z. If ⊨z, then the truth z holds for the theory regardless.
That might seem like an inconsequential shift in meaning. However, if a logical system has soundness, the rules of inference preserve truth with respect to the semantics of the system, and its axioms are tautologies, then any formula derivable from the axioms will not only qualify as a theorem, but also qualify as valid. Checking all interpretations model-theoretically via truth tables can get problematic at some point even in logic with only two truth values. In multi-valued and infinite-valued logic, checking all interpretations model-theoretically can become even more difficult. However, formal proofs will tell you if a formula is semantically valid given the above conditions, and you can even generate theorems from other theorems mechanically without knowing what you will prove in systems which have modus ponens via rules of inference like condensed detachment. Additionally, there often exist several different truth sets which have the same theorem, and you might not know an appropriate domain that you want to check for semantic validity (pick axiom sets of even propositional logic and imagine trying to find all possible sets of truth values which satisfy them).
So, even if what I proposed in the first paragraph isn't well-developed, I will say that I think your question has much merit to it.