Please give the most illuminating example of a model for a formal system, and a simple example of its use. I also wish an example of an interpretation, and what its useful for.
A formal system is a syntactical concept. It includes a language in which there are relation symbols, functions and constant symbols. We can write sentences and we can prove things from assertions written in the language. If we have a collection of such assertions, from which we cannot derive contradiction then we say that this collection is a theory.
A model is a semantical concept. It interprets the language, and through this interpretation we can say whether or not a statement is true in that model .
When we say "Of course $0\neq 1$", we know that this is a true statement, but formally we can define a theory and a model of this theory which interprets $0$ and $1$ the same way, and so in that model $0=1$.
So we first need to understand that a model interprets the language, and is bounded by the assertions of the theory, which we will call axioms.
For example, take the language in which there is one constant $c$ and two relation symbols $=$ and $<$, both are binary relations. We can now write the following axioms:
We can interpret this system in the model $N$ which we define as:
Note that we could not have interpreted $c$ as any other number without altering $<$ too.
It is quite simple to see that this is indeed a model of the formal system. However we could have chosen a different model, we could have defined it to be $Q$ which will be composed of the rational numbers which are not negative, or any other way.
Note that the axioms of this theory cannot be satisfied by a finite model, this is because we require there will be no $<$-maximal element, and a finite ordering always has a maximal element.