2.4 Semantica dichiarativa

Una interpretazione I per un linguaggio del primo ordine L è una coppia $< D, V>$ dove D è il dominio (insieme non vuoto) e V è un mapping che mappa:

• ogni costante di L su un elemento di D.
• ogni simbolo di funzione n-ario f in L su una funzione $f_{I}$ da $D_{n}$ in D.
• ogni simbolo di predicato n-ario p in L su una funzione $p_{I}$ da $D_{n}$ in $\{true, false\}$.

Se una formula F è vera nell'interpretazione I scriviamo $I\models F$.

Sia S un insieme di formule. Diciamo che un'interpretazione I è un modello per S se ogni formula di S è vera in I. Se S ha un modello, diciamo che S è soddisfacibile o consistente. Altrimenti, diciamo che S è insoddisfacibile o inconsistente. Quando ogni interpretazione è un modello per S, diciamo che S è valida.