Formal Foundations

Syntax

In first-order logic, one constructs formulas that are statements about individuals in some domain of discourse and their relationships. Many-sorted logic adds the possibility of talking about multiple, separate domains.

Semantics

For each signature \(\Sigma\), the meaning of \(\sigma\)-terms is provided by mathematical structures called interpretations. A \(\Sigma\)-interpretation \(\mathcal{I}\) maps:

• each sort \(\sigma\) of \(\Sigma\) to a non-empty set \(\sigma^\mathcal{I}\), the domain of \(\sigma\) in \(\mathcal{I}\), with \(\mathsf{Bool}^\mathcal{I}\) being the binary set \(\{\mathsf{true},\mathsf{false}\}\);

• each variable \(x \in\) X of sort \(\sigma\) to an element \(x^\mathcal{I} \in \sigma^\mathcal{I}\);

• each function symbol \(f\) of rank \(\sigma_1\cdots\sigma_n\sigma\) to a total function \(f^\mathcal{I}\) of type \(\sigma_1^\mathcal{I} \times \cdots \times \sigma_n^\mathcal{I} \to \sigma^\mathcal{I}\) (and, in particular, each constant symbol \(c\) of sort \(\sigma\) to an element \(c^\mathcal{I} \in \sigma^\mathcal{I}\)).

We say that \(\sigma\) (resp. \(x\), \(f\)) denotes the set \(\sigma^\mathcal{I}\) (element \(x^\mathcal{I}\), function \(f^\mathcal{I}\)) in \(\mathcal{I}\). Every \(\Sigma\)-interpretation \(\mathcal{I}\) extends from variables and function symbols to \(\Sigma\)-terms \(t\) as follows: \((i)\) a term \(f(t_1,\ldots,t_n)\) evaluates in \(\mathcal{I}\) to \(f^\mathcal{I}(t_1^\mathcal{I},\ldots,t_n^\mathcal{I})\), the value returned by function \(f^\mathcal{I}\) when applied to the elements denoted by \(t_1,\ldots,t_n\); \((ii)\) an existentially quantified formula \(\exists\, x : \sigma. \varphi\) evaluates to \(\mathsf{true}\) in \(\mathcal{I}\) if and only if \(\varphi\) evaluates to \(\mathsf{true}\) in an interpretation \(\mathcal{I}[x \mapsto a]\) that maps \(x\) to some suitable \(a \in \sigma^\mathcal{I}\) and is otherwise identical to \(\mathcal{I}\); \((iii)\) a universally quantified formula \(\forall\, x : \sigma. \varphi\) evaluates to \(\mathsf{true}\) in \(\mathcal{I}\) if and only if \(\varphi\) evaluates to \(\mathsf{true}\) in \(\mathcal{I}[x \mapsto a]\) for all possible choices of values for \(x\) in \(\sigma^\mathcal{I}\).

An interpretation \(\mathcal{I}\) satisfies a formula \(\varphi\) if \(\varphi^\mathcal{I} = \mathsf{true}\) and falsifies it if \(\varphi^\mathcal{I} = \mathsf{false}\). In the former case, we also say that \(\mathcal{I}\) is a model of \(\varphi\).

The reduct of an \(\Omega\)-interpretation \(\mathcal{I}\) to a subsignature \(\Sigma\) of \(\Omega\) is the (unique) \(\Sigma\)-interpretation that interprets the symbols of \(\Sigma\) exactly as \(\mathcal{I}\). Intuitively, the reduct is obtained by forgetting the symbols of \(\Omega\) that are not in \(\Sigma\).

In the definition of interpretation above, we have not provided a meaning for the usual Boolean connectives such as \(\lnot, \land, \lor, \Rightarrow\) and so on. In SMT, specific interpretations of function symbols are provided by a theory, as explained next.

Theories

In general, we are not interested in arbitrary interpretations of terms and formulas in a signature \(\Sigma\) but in interpretations belonging to a specific theory \(T\) that constrain the meaning of the symbols in \(\Sigma\); for instance, that interpret \(\lnot\) and \(\land\) as logical negation and conjunction, \(0, 1, 2, \ldots\) as the natural numbers, and so on. Traditionally in logic, a theory is defined by a set of formulas, called axioms: one considers only \(\Sigma\)-interpretations that satisfy all the axioms. In SMT, a theory is, more generally, a class of interpretations that can be specified axiomatically or in other ways. More precisely, a \(\Sigma\)-theory \(T\) is a pair \((\Sigma, \mathbf{I})\) where \(\Sigma\) is a signature and \(\mathbf{I}\) is a class of \(\Sigma\)-interpretations, however specified. We describe and discuss several examples of theories commonly used in SMT in the next section.

Given a theory \(T\) \(= (\Sigma, \mathbf{I})\), we consider not just \(\Sigma\)-formulas but \(\Omega\)-formulas for some supersignature \(\Omega\) of \(\Sigma\).

In the context of \(T\), we refer to the symbols of \(\Sigma\) as theory symbols and to the additional symbols in \(\Omega\) as uninterpreted symbols. For instance, in the theory of reals, we may write a formula of the form \(a + 1 > b\) where \(a\) and \(b\) are uninterpreted, or symbolic, constants of sort \(\mathsf{Real}\). Intuitively, while the meaning of \(+\) and \(1\) is fixed by the theory, the meaning of \(a\) and \(b\) is not. Hence, we consider the formula satisfiable if there are real values for \(a\) and \(b\) which make the formula evaluate to \(\mathsf{true}\). This idea is formalized in the notion of satisfiability in \(T\).