Theories and models In propositional logic, a theory $T$ consists of a set of logical symbols and statements which we call axioms. A logical statement $A$ can be proven by $T$ if there is a proof of $A$ using the standard deduction rules for logic and assuming the axioms of $T$.
Next we defined the model $M$ of a theory $T$.
Given the tuple $(B,v)$ where $B$ is a Boolean algebra and $v:X \mapsto B$ is the so called valuation function mapping symbols $X$ to elements of $B$. The meaning of a statement $A$ is defined as $[A] \in B$ in the natural inductive way:

*

*$[\perp] = 0$, $[\top] = 1$


*$[p] = v(p)$ if $p$ is a logical symbol


*$[A \vee B] = [A] \vee_B [B]$ (here $\vee_B$ denotes the respective operation asociated with $B$)


*and so on.....
A statement $A$ is valid if $[A]= 1$ so the meaning of $A$ wrt. a model $M$ is the element $1$ of the Boolean algebra in $M.$  A model of the theory $T$ is any $(B,v)$ in which the axioms of $T$ have meaning 1.
After that, many theorems followed relating the validity of a statement $A$ in the model $M$ of a theory $T$ and the provability of that statement in $T$. Here is where I get lost. What exactly is going on? Why are we even introducing models? This new level of abstraction when dealing with theories confuses me completely. How do this models arise in dealing with "practical" mathematical proof working? Is there a dumb example?
 A: Here's an example: take your language to be the group language $L_G = \{ e, \cdot \}$ and your theory to be the three group axioms:
$$ (i) \exists e \in G: \forall g \in G: eg = ge = g$$
$$ (ii) \forall g \in G \exists g^{-1} \in G: gg^{-1} = g^{-1}g = e$$
$$ (iii) \forall a,b,c \in G: a(bc) = (ab)c$$
Then every group is a model of that theory. 
As for why we are introducing models: that might be because it makes it easier to think about a given theory.
A: I'll try to clarify your confusion. 
Basically in logic there are formulas, which are sequences of symbols, and interpretations, that give meaning to formulas. This meaning usually is a truth value, i.e. a value in $\{0, 1\}$. Your case is more general, the meaning is a value in some boolean algebra. The interpretation is said to be a model of the formula if the meaning of the formula is $1$. The interpretation is said to be a model of a set of formulas if it is a model of each formula.
The central notion in logic is the notion of logical consequence. It is defined as follows the formula (set of formulas) $G$ is said to be a logical consequence of the formula (set of formulas) $F$ (in symbols $F \models G$) if every model of $F$ is a model of $G$. Now the definition of $\models$ is usually highly non-constructive. That is it requires one to examine all models of the given formula. To fix this, deduction systems are introduced. The fact that $G$ is deducible from $F$ is usually denoted as $F \vdash G$. Ideally the deduction system should be complete ($F \models G \implies F \vdash G$) and consistent ($F \vdash G \implies F \models G$).
To sum up, I think that the relation $\models$ of logical consequence is the central relation in logic (and it is defined through models) and the relation $\vdash$ of deductibility is complementing it.
A: Intuitively you might want to think of a model $M$ of a theory $T$ as an example. 
Say $\mathcal L$ is a PL-1 language, $T$ is a set of $\mathcal L$ sentences then a $T$-model $M$ is defined as an $\mathcal L$-structure making the sentences in $T$ true when interpreted in $M$.
Lets assume $T$ is the set of group axioms. Then the general linear group $GL_n(\Bbb R)$ and the special linear group $SL_n(\Bbb R)$ each with matrice multiplication are examples for groups or u can say models of the group axioms, aswell as all turing machines with concatenation satisfy the group axioms and thus is a group / model of the theory of groups.
A: My impression of this goes that in propositional calculus, with only proof theory, there exist ways to derive formulas which intuitively have meanings which either surpass a person's understanding or come as ridiculously difficult to see.  This implies that more mathematics can get formed than possible with proofs just from ordinary mathematics, since more connections exist between mathematical statements than ordinary mathematics takes for granted.  Hence, these new levels of abstraction help to inform you of what else can get done mathematically than you might believe.  This also helps to inform you when proposed new connections aren't valid or need validated differently than an author proposed.
