# Definition:Formal Semantics

## Definition

Let $\LL$ be a formal language.

A **formal semantics** for $\LL$ comprises:

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

### Structure

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.

### Validity

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$

## Examples

### 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$

Although this article appears correct, it's inelegant. There has to be a better way of doing it.In particular: Extension would be useful to fold the above (see Definition:Tautology/Formal Semantics). But maybe this section should just be a link to an examples categoryYou can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by redesigning it.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Improve}}` from the code.If you would welcome a second opinion as to whether your work is correct, add a call to `{{Proofread}}` the page. |

### 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.