Is There an Optimal Generic Semantics for First-Order Equations?

Abstract

Apt [1] has proposed a denotational semantics for first-order logic with equality, which is an instance of the computation as deduction paradigm: given a language $\mathcal L$ together with an interpretation $\mathcal I$ and a formula φ in $\mathcal L$, the semantics consists of a (possibly empty) set of substitutions θ such that φθ is true in $\mathcal I$, or it may contain error to indicate that there might be further such substitutions, but that they could not be computed. The definition of the semantics is generic in that it assumes no knowledge about $\mathcal I$ except that a ground term can effectively be evaluated. We propose here an improvement of this semantics, using an algorithm based on syntactic unification. Although one can argue for the optimality of this semantics informally, it is not optimal in any formal sense, since there seems to be no satisfactory formalisation of what it means to have “no knowledge about $\mathcal I$ except that a ground term can effectively be evaluated”. It is always possible to “improve” a semantics in a formal sense, but such semantics become more and more contrived.