Definition:Formal Semantics
Contents
Definition
Let $\mathcal L$ be a formal language.
A formal semantics for $\mathcal L$ comprises:
- A collection of objects called structures;
- A notion of validity of $\mathcal L$-WFFs in these structures.
Often, a formal semantics provides these by using a lot of auxiliary definitions.
Structure
Part of specifying a formal semantics $\mathscr M$ for $\mathcal L$ is to specify structures $\mathcal M$ for $\mathscr M$.
A structure can in principle be any object one can think of.
However, to get a useful formal semantics, the structures should support a meaningful definition of validity for the WFFs of $\mathcal L$.
It is common that structures are sets, often endowed with a number of relations or functions.
Validity
Part of specifying a formal semantics $\mathscr M$ for $\mathcal L$ is to define a notion of validity.
Concretely, a precise meaning needs to be assigned to the phrase:
- "The $\mathcal L$-WFF $\phi$ is valid in the $\mathscr M$-structure $\mathcal M$."
It can be expressed symbolically as:
- $\mathcal M \models_{\mathscr M} \phi$
Examples
Boolean Interpretations
Let $\mathcal L_0$ be the language of propositional logic.
The boolean interpretations for $\mathcal L_0$ can be interpreted as a formal semantics for $\mathcal L_0$, which we denote by $\mathrm{BI}$.
The structures of $\mathrm{BI}$ are the boolean interpretations.
A WFF $\phi$ is declared ($\mathrm{BI}$-)valid in a boolean interpretation $v$ iff:
- $v \left({\phi}\right) = T$
Symbolically, this can be expressed as:
- $v \models_{\mathrm{BI}} \phi$
Constructed Semantics
Let $\mathcal L$ be a formal language.
A constructed semantics for $\mathcal L$ is a formal semantics which is invented solely for proving a property about $\mathcal L$ or other entities related to $\mathcal L$.
Also see
- Results about formal semantics can be found here.