Definition:Formal Semantics/Valid

From ProofWiki
Jump to navigation Jump to search

This page is about Valid in the context of Formal System. For other uses, see Valid.


Let $\LL$ be a formal language.

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$

Also denoted as

When the formal semantics in use is clear from the context, $\MM \models \phi$ is commonly seen in place of $\MM \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

Linguistic Note

The word valid ultimately derives from the same root as the word value.

Thus valid can be taken to mean having value.