Definition:Formal Semantics/Valid

From ProofWiki
Jump to: navigation, search

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.


Also see