What is a model of a formal system? 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:


*

*$\forall x(\lnot(x<x))\land\forall x\forall y\forall z(z<x\land x<y\rightarrow z<y)\land\forall x\forall y(x=y\lor x<y\lor y<x)$, The relation $<$ is a strict total order relation;

*$\forall x(c<x)$ the constant $c$ is the $<$-minimum element;

*$\forall x\exists y(x<y)$ the order $<$ has no maximal element.


We can interpret this system in the model $N$ which we define as:


*

*$|N|=\mathbb N$, that is the element of the model $N$ are the natural numbers.

*$<^N$, the interpretation of $<$ is going to be the "usual" interpretation, what does that mean? It means that $0<1<2<3<\ldots$, as we are used to think informally.

*$c^N=0$, we interpret the constant $c$ as our minimal element, that is $0$.

*$=^N$ is interpreted, as anywhere else in mathematics as equality. $x=y$ if and only if they are the same number.


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.
