\( \newcommand{\matr}[1] {\mathbf{#1}} \newcommand{\vertbar} {\rule[-1ex]{0.5pt}{2.5ex}} \newcommand{\horzbar} {\rule[.5ex]{2.5ex}{0.5pt}} \)
deepdream of a sidewalk
Show Answer
\( \newcommand{\cat}[1] {\mathrm{#1}} \newcommand{\catobj}[1] {\operatorname{Obj}(\mathrm{#1})} \newcommand{\cathom}[1] {\operatorname{Hom}_{\cat{#1}}} \newcommand{\multiBetaReduction}[0] {\twoheadrightarrow_{\beta}} \newcommand{\betaReduction}[0] {\rightarrow_{\beta}} \newcommand{\betaEq}[0] {=_{\beta}} \newcommand{\string}[1] {\texttt{"}\mathtt{#1}\texttt{"}} \newcommand{\symbolq}[1] {\texttt{`}\mathtt{#1}\texttt{'}} \)
Math and science::Theory of Computation::Modal theory

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:

  1. a variable symbol or a constant symbol, or
  2. 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:

  1. A sequence of symbols where [condition 1], and [condition 2]. [condition 3].
  2. [\( \;\; ?_1 \; (?_2) \;\;  \)] for some formula \( \alpha \).
  3. [\(  \;\; ( ?_1 \; ?_2 \; ?_3) \;\; \)] for some formulas \( \alpha \) and \( \beta \).
  4. [\( \;\; ?_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.