# Languages, terms and formulas

This page defines languages, first order languages, terms, formulas and sentences as used in modal theory.

### Language

A language is [what?].

A *language* in model theory is similar to an [what?] in
computation theory. They are both collections of symbols; however, model theory
[differs in what way?].

The reverse side discusses the encoding of a language.

### First-order language

A first-order language is a language with the following symbols:

- 1 a. Parentheses
- \( \symbolq{(}, \symbolq{)} \)
- 1 b. Connectives
- \( \symbolq{\land}, \symbolq{\lnot} \)
- 1 c. Quantifier
- \( \symbolq{\forall} \)
- 2. Variables
- countable symbols \( \symbolq{v_1}, \symbolq{v_2}, \symbolq{v_3}, ... \)
- 3. Constant symbols
- zero or more (at most countable) symbols \( \symbolq{c_1}, \symbolq{c_2}, ...\)
- 4. Function symbols
- for every natural \( n > 0 \), zero or more (at most countable) \( n \)-arity symbols \( \symbolq{f_1^{n}}, \symbolq{f_2^{n}}, ... \)
- 5. Relation symbols
- for every natural \( n > 0 \), zero or more (at most countable) \( n \)-arity symbols \( \symbolq{R_1^{n}}, \symbolq{R_2^{n}}, ... \)

This definition is a slight alteration of that given by Leary and Kristiansen. There is much to say about this definition in terms of its encoding (covered on the back side).

Modal theory doesn't pause to give a definition for the set of all possible
strings formed from symbols of a model theory language. This would
be the *language* in computation theory terms. Instead we go straight to
carving out this space to form much smaller sets of strings: *terms*
and *formula*.

### Terms of a first-order language

Let \( \mathcal{L} \) be a first-order language. A *term* of
\( \mathcal{L} \) is defined recursively as:

- a variable symbol or a constant symbol, or
- a sequence of symbols where the first symbol is [condition 1] and the remaining symbols are [condition 2]. The number of [what?] must match the [what?].

To be percise, the above definition is an algorithm for checking if a symbol or sequence of symbols is a term. If instead we wished for a set definition, we could define it as the union of recursively defined sets.

Another recursive definition is employed to define the *formulas* of a first-order language.

### Formulas of a first-order language

Let \( \mathcal{L} \) be a first-order language. A *formula* of \(
\mathcal{L} \) is a sequence of symbols of \( \mathcal{L} \) defined
recursively. Each formula must be one of the following:

- A sequence of symbols where [condition 1], and [condition 2]. [condition 3].
- [\( \;\; ?_1 \; (?_2) \;\; \)] for some formula \( \alpha \).
- [\( \;\; ( ?_1 \; ?_2 \; ?_3) \;\; \)] for some formulas \( \alpha \) and \( \beta \).
- [\( \;\; ?_1 \; ?_2 \; (?_3) \;\; \)] for some variable symbol \( v \) and some formula \( \alpha \).

Similar to the definition of terms, the definition for a language reads as an algorithm for checking if a sequence of symbols of \( \mathcal{L} \) is a formula.