In one paper I have read a note "Thus, unlike approaches which make use of full first order logic, unprovability of a formulae with respect to a agent specification can be shown by each of two approaches automatically without reliance on modeltheoretic consideration outside the actual proof method".
note means that there are proof methods that use semantic (model theoretic) and not syntactic means. Usually such situation can arise (and is the only possible way forward) when the logic under consideration does not have soundness and completeness properties.
The question is - are there semantic methods (or other non-syntactic methods) that can be used to prove some formulas of non-sound and/or non-complete logics. I can imagine in practice that this can mean the following: logic can have syntax and syntactical proof methods but those methods work for only part of formulae (e.g. for some syntactically specified fragments). If the proof of more complex formulae are required then semantic methods can be used. Such combined approach can be used in practice. So - is there described approach in reality?
p.s. Annals of Mathematics has article 'Proofs without syntax', it is about fact that different sturcutres can be used in place of formal languages - e.g. formal language can be substituted by graph structures. Actually I think that this not big achievement and it is still like having formal language. Semantics usually give far more opportunities than regulated syntactical structures.