I apologize if my question is not well formed. The reason for it is that I don't understand the concepts enough to be able to ask a completely meaningful question.

In the classes we said that a theory $T$ consists of a set of logical symbols and statements which we call axioms.

Edit: I am only talking about propositional logic here.

We say that 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$.

We defined the meaning of a statement $A$ 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.....

We then said that 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?


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.

  • 2
    $\begingroup$ In most cases, we introduce models because models are the things we care about. They're the whole point of the exercise. We're interested in the logical consequences of the group axioms because we're interested in groups, not the other way around. $\endgroup$ – Chris Eagle Apr 17 '12 at 13:53
  • $\begingroup$ @ChrisEagle Thank you for your comment! $\endgroup$ – Rudy the Reindeer Apr 17 '12 at 14:03
  • $\begingroup$ Can you clarify the sentence "Then every group is a model of that theory."? How exactly is the Boolean algebra from the model of the definition used in this case? $\endgroup$ – Jernej Apr 17 '12 at 14:20
  • $\begingroup$ @Azoo: This answer is about first-order logic and first-order models. $\endgroup$ – Chris Eagle Apr 17 '12 at 14:21
  • $\begingroup$ @Chris: I think your first comment above deserves to be expanded into an answer. $\endgroup$ – Henning Makholm Apr 17 '12 at 16:25

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.

  • $\begingroup$ So the gist of all these theorems relating deductibility and logical consequence is the fact that one loses nothing by fixing a "proper" deduction system? $\endgroup$ – Jernej Apr 18 '12 at 8:36
  • $\begingroup$ Not all theorems of course, but Goedel's completeness theorem for example is about the soundness and completeness of certain deduction systems for first order logic. Also not all logical systems have effective sound and complete deduction systems. $\endgroup$ – Levon Haykazyan Apr 18 '12 at 11:24

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.


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.