Definition:Formal Semantics

From ProofWiki
Jump to navigation Jump to search


Let $\LL$ be a formal language.

A formal semantics for $\LL$ comprises:

  • A collection of objects called structures;
  • A notion of validity of $\LL$-WFFs in these structures.

Often, a formal semantics provides these by using a lot of auxiliary definitions.


Part of specifying a formal semantics $\mathscr M$ for $\LL$ is to specify structures $\MM$ 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 $\LL$.

It is common that structures are sets, often endowed with a number of relations or functions.


Part of specifying a formal semantics $\mathscr M$ for $\LL$ is to define a notion of validity.

Concretely, a precise meaning needs to be assigned to the phrase:

"The $\LL$-WFF $\phi$ is valid in the $\mathscr M$-structure $\MM$."

It can be expressed symbolically as:

$\MM \models_{\mathscr M} \phi$


Boolean Interpretations

Let $\LL_0$ be the language of propositional logic.

The boolean interpretations for $\LL_0$ can be interpreted as a formal semantics for $\LL_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$ if and only if:

$\map v \phi = \T$

Symbolically, this can be expressed as:

$v \models_{\mathrm{BI}} \phi$

Constructed Semantics

Let $\LL$ be a formal language.

A constructed semantics for $\LL$ is a formal semantics which is invented solely for proving a property about $\LL$ or other entities related to $\LL$.

Also see

  • Results about formal semantics can be found here.