Confusion over the definition of "model" In my question yesterday I asked about the definition and usage of the word "model", for which I was told the following definition:

A formula of propositional logic is true under an interpretation iff
  the interpretation assigns the truth value T to that formula. If a
  formula is true under an interpretation, then that interpretation is
  called a model of that formula.

An interpetation satisfies a formula φ iff it is a model of the formula. Same for a set $\Gamma$ of formulas, if an interpretation satisfies all the formulas in $\Gamma$ then it is a model of $\Gamma$. Then if we say $\Gamma \vDash \varphi$ then $\varphi$ is a semantic consequence of $\Gamma$ / is satisfied in all "models" of $\Gamma$ (true whenever everything in $\Gamma$ is true).
This also matches the definitions for model as seen on the Wiki for Interpretation (Logic) and Propositional calculus.
All good so far. But when I get really confused when I see posts like these where they use "models" as a word meaning "satisfies all the axioms in a theory."
From Asaf's answer:

Models are structures, and structures are models. But when we say
  "model" we mean that there is a particular theory which holds in the
  structure, and when we say "structure" we are mainly interested in an
  arbitrary interpretation of the language.

From Metin's answer:

A structure is a set with some interpretable symbols(constants,
  relations and functions) within a fixed language. You do not ask for
  more from a structure.
However...
A model (of a theory) is a structure which satisfies the axioms of the
  theory. It makes more "structural sense"...

And then from one of Asaf's comments:

When I say "a model of " they also know, immediately, that I am
  talking about a model which satisfies all the axioms of .

So I am unclear on which definition is correct or if this is the same word being used in two different ways or if this is "logical model" versus "semantic model" or something else entirely.
On the one hand we seem to have "model" meaning "any interpretation that satisfies a formula or set of formulas." On the other hand we have "model" meaning "Interpretation that satisfies all the axioms of a theory".
From the Wiki article on Structure (mathematical logic) we see also:

For a given theory in model theory, a structure is called a model, if
  it satisfies the defining axioms of that theory.

So which is it exactly? Does "model" have a different meaning in propositional logic compared to model theory or first-order logic or set theory etc?
 A: We agree that an interpretation is a model of a formula $\varphi$ if the formula is TRUE in that interpretation (i.e. if the interpretation satisfies the formula).
The same for a set $\Gamma$ of formulas.
Consider now a theory $T$ with the collection $\Gamma_T$ of its axioms. 

"A model of the theory is an interpretation that satisfies all the axioms of the theory."

So far, nothing new : the collection of axioms of the theory $T$ is a set of formulas. Thus, a model of the theory is an interpretation that satisfies all those formulas.
Consider for example first order arithmetic, i.e. the f-o version of Peano axioms.
We can call the collection of f-o Peano axioms with $\mathsf {PA}$.
We can prove from it the usual arithmetical laws (or theorems), like e.g. : $1+1=2$.
In symbols, we have : $\mathsf {PA} \vdash (1+1=2)$.
By soundness of the predicate calculus, we have : $\mathsf {PA} \vDash (1+1=2)$.
And again, this is consistent with the above definitions :

the arithemetical theorem $1+1=2$ is a logical consequence of the (first-order) arithmetical axioms, i.e. it is TRUE in every interpretation that satisfies the collection $\mathsf {PA}$ of arithmetical axioms.


In the answer to your previous post we have seen that an interpretation for propositional logic is :

an assignment $v : \text{At} \to \{ \text T, \text F \}$ such that, e.g. $v(p_0)= \text T, v(p_1)= \text F$, etc.

In the case of first-order language an interpretation needs a domain of "objects", like e.g. the set $\mathbb N$ of natural numbers.
Of course, different FOL theories need different domains, while in propositional logic we have only one domain: the boolean one $\{ \text T, \text F \}$.
And then we have to specify how to interpret the new elements of the language (in addition to the connectives) : quantifiers, individual constants, variables, predicate and function symbols.
Having done this, we have to complete our semantics for FOL with the definition of :

satisfaction relation, model, valid formula, logical consequence.

