<p>Here is one possibility, but other people might use different words. I will use first-order logic as a running example.</p>

<h3>Language</h3>

<p>The language is a collection of expressions, which are syntactic entities, i.e., finite configurations without any a priori meaning. A language is described by the <strong>grammar</strong>, which determines which finite configurations are valid expressions.</p>

<p>A language may have several kinds of expressions, for instance terms and formulas, each obeying their own grammar.</p>

<p>The expressions of a language may be represented in different ways. When they are written as strings of characters that is called <strong>concrete syntax</strong>. When the expressions are represented as abstract mathematical configurations (usually trees of some sort) that is called <strong>abstract syntax</strong>. The process of passing from the concrete to the abstract syntax is <strong>parsing</strong>.</p>

<p>When we manipulate the language in a mathematical way it is best to use the abstract syntax so we do not have to deal with silly things like parentheses and spaces.</p>

<p>It may happen in certain situations that the language is so complicated that simple grammatical rules do not suffice to describe the valid expressions. For example, in type theory you may have to <em>prove</em> that a certain expression is valid, and the proof can be arbitrarily complex. In such situations people may speak of "pre-expressions" or "pre-terms" described by the grammar.</p>

<p><strong>First-order logic:</strong> there are two kinds of expressions, the terms and the formulas. In each particular situation we also have a list of chosen constant symbols, function symbols, and relation symbols. For instance, the first-order language of an ordered fields has (in addition to the usual logical connectives, $=$, and variables) the constant symbols $0$ and $1$, the function symbols $+$, $\times$, $-$, and the relation symbol $&lt;$.</p>

<h3>Structure</h3>

<p>It is our intention to give the language a mathematical meaning. For this purpose we first need to describe the mathematical objects that parts of the language map to. Such a mathematical object, or collection of objects, or a category, is called a <strong>structure</strong>. The structures have to be sufficiently rich to support the interpretation of all the parts of the language.</p>

<p><strong>First-order structure:</strong> is a <em>carrier set</em> $S$ together with a list of constants (elements of $S$), functions (mapping from $S^n \to S$) and relations (subsets of $S^n$).</p>

<h3>Interpretation</h3>

<p>An interpretation is the mapping of the language into the structure. It may be called the "interpretation function".</p>

<p>In complicated situations one might provide an interpretation in several layers, in which case you could the first layer pre-interpretation, etc.</p>

<p><strong>First-order interpretation:</strong> The terms are mapped to the elements of the carrier set $S$, the formulas are mapped to propositional functions (mapping from $S^n$ to truth values). A formula is <strong>valid</strong> in a given interpretation if it is mapped to the propositional function which always gives the value "true".</p>

<h3>Formal system</h3>

<p>A formal system consists of a language and rules for deriving <strong>judgements</strong>.</p>

<p><strong>First-order logic:</strong> In first-order logic there is just one kind of judgement, $$\phi_1, \ldots, \phi_n \vdash \phi$$ whose intuitive meaning is "$\phi$ is proved from hypotheses $\phi_1, \ldots, \phi_n$".</p>

<p>Just to give you another kind of judgement: in programming languages a typical judgement might be $e \Downarrow v$ with the intuitive meaning "program $e$ computes to value $v$".</p>

<h3>Theory</h3>

<p>The notion of a theory is somewhat specific to logic (it makes less sense when we speak about programming languages or type theory) where we have a notion of a logical formula.</p>

<p>Given a specific language, say that a set $T$ of logical formulas is <em>deductively closed</em> if any formula that can be derived from formulas in $T$ is again an element of $T$.</p>

<p>Every set of formulas $T_0$ has the <em>deductive closure</em>, which is the least set $T$ that contains $T_0$ and is deductively closed. We get $T$ from $T_0$ by adding to $T_0$ all of its consequences, and consequences of consequences, and so on.</p>

<p>A <strong>theory</strong> is a deductively closed set of formulas. It is <em>usually</em> (but not necessarily) gives as the deductive closure of a chosen set of formulas called the <strong>axioms</strong>.</p>

<h3>Model</h3>

<p>Given a theory $T$ and a structure $S$, a model is an interpretation of the language of $T$ into $S$ such that every formula in $T$ is valid in $S$.</p>

CC BY-SA 3.0
2016-05-21T08:45:39.900Z
2016-05-25T21:43:24.147Z
2016-05-25T21:43:24.147Z
Andrej Bauer
<p>I am trying to give a formal presentation of the model-theoretical semantics of a language and I am a bit lost in the terminology. In particular, could somebody clarify the exact definitions of model-structures or pre-interpretations, interpretations and interpretation functions ? It would be great if you could point me to a standard reference.</p>

<p>The way I see it, a "pre-intepretation structure" is defined for the signature of a particular language/logic as regrouping a domain and a mapping ("interpretation function" ?) of constants and predicates to that domain.  Next, one has to assign particular truth values to each of the constructs of the language, according to a specific "interpretation" and valuation. Is this the standard terminology ? Thank you !</p>

CC BY-SA 3.0
2016-05-20T19:45:36.030Z
I don't think there is any common terminology because seldom one needs to distinguish between them. You can use structure, model, interpretation, valuation, context, ... Just be consistent with some previous work in the area and state the definitions and you should be fine.
Kaveh
CC BY-SA 3.0
2016-05-21T08:12:18.340Z
There is a broad range of possibilities. If this is about first-order logic then one kind of terminology is appropriate, but if it is about type theory then another kind is more common. Can you be a bit more specific about what kind of languages you have in mind? It looks like it might be first-order logic.
Andrej Bauer
<lo.logic><semantics><finite-model-theory><model-theory><definitions>
Standard reference for basic model theory definitions
AnaK
# Standard reference for basic model theory definitions

(Asked by: username_0 on 2016-05-20)

I am trying to give a formal presentation of the model-theoretical semantics of a language and I am a bit lost in the terminology. In particular, could somebody clarify the exact definitions of model-structures or pre-interpretations, interpretations and interpretation functions ? It would be great if you could point me to a standard reference.

The way I see it, a "pre-intepretation structure" is defined for the signature of a particular language/logic as regrouping a domain and a mapping ("interpretation function" ?) of constants and predicates to that domain. Next, one has to assign particular truth values to each of the constructs of the language, according to a specific "interpretation" and valuation. Is this the standard terminology ? Thank you !

**Tags:** lo.logic, semantics, finite-model-theory, model-theory, definitions
> **Comments:**
> **username_1**: I don't think there is any common terminology because seldom one needs to distinguish between them. You can use structure, model, interpretation, valuation, context, ... Just be consistent with some previous work in the area and state the definitions and you should be fine.  
> **username_2**: There is a broad range of possibilities. If this is about first-order logic then one kind of terminology is appropriate, but if it is about type theory then another kind is more common. Can you be a bit more specific about what kind of languages you have in mind? It looks like it might be first-order logic.  

---

## 1 answers

### Answer by username_2 on 2016-05-21. Score: 11 | Accepted answer

Here is one possibility, but other people might use different words. I will use first-order logic as a running example.

### Language

The language is a collection of expressions, which are syntactic entities, i.e., finite configurations without any a priori meaning. A language is described by the **grammar**, which determines which finite configurations are valid expressions.

A language may have several kinds of expressions, for instance terms and formulas, each obeying their own grammar.

The expressions of a language may be represented in different ways. When they are written as strings of characters that is called **concrete syntax**. When the expressions are represented as abstract mathematical configurations (usually trees of some sort) that is called **abstract syntax**. The process of passing from the concrete to the abstract syntax is **parsing**.

When we manipulate the language in a mathematical way it is best to use the abstract syntax so we do not have to deal with silly things like parentheses and spaces.

It may happen in certain situations that the language is so complicated that simple grammatical rules do not suffice to describe the valid expressions. For example, in type theory you may have to *prove* that a certain expression is valid, and the proof can be arbitrarily complex. In such situations people may speak of "pre-expressions" or "pre-terms" described by the grammar.

**First-order logic:** there are two kinds of expressions, the terms and the formulas. In each particular situation we also have a list of chosen constant symbols, function symbols, and relation symbols. For instance, the first-order language of an ordered fields has (in addition to the usual logical connectives, $=$, and variables) the constant symbols $0$ and $1$, the function symbols $+$, $\times$, $-$, and the relation symbol $<$.

### Structure

It is our intention to give the language a mathematical meaning. For this purpose we first need to describe the mathematical objects that parts of the language map to. Such a mathematical object, or collection of objects, or a category, is called a **structure**. The structures have to be sufficiently rich to support the interpretation of all the parts of the language.

**First-order structure:** is a *carrier set* $S$ together with a list of constants (elements of $S$), functions (mapping from $S^n \to S$) and relations (subsets of $S^n$).

### Interpretation

An interpretation is the mapping of the language into the structure. It may be called the "interpretation function".

In complicated situations one might provide an interpretation in several layers, in which case you could the first layer pre-interpretation, etc.

**First-order interpretation:** The terms are mapped to the elements of the carrier set $S$, the formulas are mapped to propositional functions (mapping from $S^n$ to truth values). A formula is **valid** in a given interpretation if it is mapped to the propositional function which always gives the value "true".

### Formal system

A formal system consists of a language and rules for deriving **judgements**.

**First-order logic:** In first-order logic there is just one kind of judgement, $$\phi\_1, \ldots, \phi\_n \vdash \phi$$ whose intuitive meaning is "$\phi$ is proved from hypotheses $\phi\_1, \ldots, \phi\_n$".

Just to give you another kind of judgement: in programming languages a typical judgement might be $e \Downarrow v$ with the intuitive meaning "program $e$ computes to value $v$".

### Theory

The notion of a theory is somewhat specific to logic (it makes less sense when we speak about programming languages or type theory) where we have a notion of a logical formula.

Given a specific language, say that a set $T$ of logical formulas is *deductively closed* if any formula that can be derived from formulas in $T$ is again an element of $T$.

Every set of formulas $T\_0$ has the *deductive closure*, which is the least set $T$ that contains $T\_0$ and is deductively closed. We get $T$ from $T\_0$ by adding to $T\_0$ all of its consequences, and consequences of consequences, and so on.

A **theory** is a deductively closed set of formulas. It is *usually* (but not necessarily) gives as the deductive closure of a chosen set of formulas called the **axioms**.

### Model

Given a theory $T$ and a structure $S$, a model is an interpretation of the language of $T$ into $S$ such that every formula in $T$ is valid in $S$.


---

