Theories and models

Question

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?

Answer 1

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.

Answer 2

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.