Behind the scenes all formula $\phi$, we must define a model, M = (F, P) over a Universe, where F = set of Functions and P = set of Predicates, on a table of free variables in $\phi$ ? Ie any $\phi$ that i desire to prove i should create a model over a particular universe?
Suppose we want to prove a assertion on the theory of sets. And we have the axioms, theorems, definitions, and all these things. Whenever i want to prove assertions, we should create or use a pre-existing model or they aren't related at all, how it works?
For example, assuming this statement over sets: |A-B| = |A| - |A $\cup$ B| .
And what about an assertion about a behavior of peoples or something else.
No, for proving a formula $\varphi$ it's not suffice to create a model. Because according to soundness theorem if a formula is provable it is valid in all models, and according to completeness theorem for proving a formula it suffices to prove it is valid in all models( Is it possible $?!$ ). I hope I could answer to your question.