Definition:Formal Semantics/Structure

From ProofWiki
Jump to: navigation, search

This page is about structures in the context of formal systems. For other uses, see Definition:Structure.


Let $\mathcal L$ be a formal language.

Part of specifying a formal semantics $\mathscr M$ for $\mathcal L$ is to specify structures $\mathcal M$ 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 $\mathcal L$.

It is common that structures are sets, often endowed with a number of relations or functions.

Structure for Predicate Logic

Let $\mathcal L_1$ be the language of predicate logic.

A structure $\mathcal A$ for $\mathcal L_1$ comprises:

$(1):$ A non-empty set $A$;
$(2):$ For each function symbol $f$ of arity $n$, a mapping $f_{\mathcal A}: A^n \to A$;
$(3):$ For each predicate symbol $p$ of arity $n$, a mapping $p_{\mathcal A}: A^n \to \Bbb B$

where $\Bbb B$ denotes the set of truth values.

$A$ is called the underlying set of $\mathcal A$.

$f_{\mathcal A}$ and $p_{\mathcal A}$ are called the interpretations of $f$ and $p$ in $\mathcal A$, respectively.

Also see