# Definition:Formal Semantics/Valid

*This page is about validity in the context of formal systems. For other uses, see Definition:Valid.*

## Definition

Let $\mathcal L$ be a formal language.

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$

## Also denoted as

When the formal semantics in use is clear from the context, $\mathcal M \models \phi$ is commonly seen in place of $\mathcal M \models_{\mathscr M} \phi$.

## Also defined as

The notion of **valid** is also often taken as synonymous with **tautology**.

That is, instead of in the context of a given structure, for all structures at once.

Although the two notions are often easily distinguished from context, it pays off to pay close attention to the exact definition being used.