Definition:Formal Semantics

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 $\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 $\mathcal L_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.
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 category
You can help Proof Wiki by redesigning it.

To discuss this proof in more detail, feel free to use the talk page.

If you are able to fix this proof, then when you have done so you can remove this instance of {{Improve}} from the code.

If you would welcome a second opinion as to whether your improvement is correct, add an invitation to {{Proofread}} the page (see the proofread template for usage).

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

Definition:Model (Logic)

Definition:Proof System

Results about formal semantics can be found here.