A note on frameworks for computational logics

A fundamentional computational assumption

SMT-based verification techniques such as [1,..] make fundamental assumptions about an background structure $\mathfrak{S}$, an r.e. universe $U$, and an r.e. set $\Phi$ of quantifier-free formulas such that
1. All elements of $U$ can be named by ground terms in the language of $\mathfrak{S}$.
2. All quantifier-free formulas in the language of $\mathfrak{S}$ are in $\Phi$.
3. If $a\in U$ and $\varphi \in \Phi$, then $\varphi[a/x]\in \Phi$.
4. If $\varphi_1, \varphi_2 \in \Phi$, then $\varphi_1\vee \varphi_2$, $\varphi_1\wedge \varphi_2$, and $\neg \varphi_1$ are all in $\Phi$.
5. Satisfiability of formulas in $\Phi$ is decidable.
Expressiveness. The above formalism does not capture all decidable languages. For example, it cannot express context-free languages as they are not closed under intersection. However, the formalism does embody the basic properties of the theories supported by any state-of-the-art SMT solver.
Working with a solver. The specialisation on quantifier-free formulas is important for SMT solvers, since theory combination in SMT solvers use quanti er free formulas and becomes undecidable when quantifiers are allowed. This fact limits what we are allowed to express in $\mathfrak{S}$ without sacrificing decidability – in general, only positive existential quantifiers are allowed, while other quantifiers are not.
Computation of witness. The assumption that $U$ is r.e. allows us to effectively compute a witness whenever a formula is satisfiable. Here effectiveness means that we have a solver which decides satisfiability and finds a witness in a finite number of steps.

Multi-typed universe & structure

In [2, 3], the background universe $U$ is an r.e. multi-typed carrier set. For each type $\tau,$ $U$ contains a sub-universe $U^\tau$ of elements of type $\tau$. For example, $U^{Bool} = \{⊥, ⊤\}$ and $U^{Int} = ℤ$. Terms are defined by induction over the language of $𝔖$ and are assumed to be well-typed. In a multi-typed structure, formulas are simply terms of type $Bool$, i.e., no distinction is made between formulas and Boolean terms. As before, we assume that all elements in $U$ can be named by the ground terms in the language.
Interpretations. An uninterpreted function symbol of arity n ≥ 1 is a function symbol $f$ with a domain sort $\sigma_1 × ⋯ × \sigma_n$ and a range sort $\sigma$. An interpretation for $f$ is a function from $U^{\sigma_1} × ⋯ × U^{\sigma_n}$ to $U^\sigma$. An interpretation of a variable of sort $\tau$ is an element in $U^\tau$. A constant is also called a function symbol of arity 0.
Semantics. The Tarski semantics of a closed term $t : \tau$ is denoted by $[\![ t ]\!] ∈ U^\tau$. For example, given a $\lambda $-term $\lambda x. t : \tau → \sigma$, $[\![ \lambda x. t ]\!]$ denotes a function mapping $a ∈ U^\tau$ to $[\![ t[x/a] ]\!] ∈ U^\sigma$. A $\lambda $-term $φ : \tau → Bool$ is called a $\tau$-predicate. Note that the semantics of $\tau$-predicates is defined differently than other $\lambda $-terms: given a $\tau$-predicate $φ$, we shall use $[\![ φ ]\!]$ to denote the set $\{ a ∈ U^\tau ∣ [\![ φ ]\!](a) = ⊤ \}$. Hence $\tau$-predicates are closed under Boolean operations, e.g., $[\![ φ ∧ ψ ]\!] = [\![ φ ]\!] ∩ [\![ ψ ]\!]$, $[\![ ¬φ ]\!] = U^\tau \setminus [\![ φ ]\!]$, etc. Under the previous assumption, satisfiability for $\tau$-predicates is decidable and a witness is computable. Hence we can assume for $\tau$-predicates an effective function $w_\tau$ such that $w_\tau(φ) ∈ [\![ φ ]\!] ∪ \{ ⊥ \}$.

References

1. Monadic Decomposition, Journal of ACM, 2017.
2. Symbolic Transducers, Microsoft Technical Report, 2011
3. Symbolic Finite State Transducers: Algorithms and Applications, POPL 2012.