Many-valued models generalise the structures from classical model theory by defining truth values for a model with an arbitrary algebra. Just as algebraic varieties provide semantics for many non-classical propositional logics, models defined over algebras in a variety provide the semantics for the corresponding non-classical predicate logics. In particular, models defined over varieties of residuated lattices represent the model theory for first-order substructural logics. In this paper we study the extent to which the classical locality theorems from Hanf and Gaifman hold true in the residuated lattice setting. We demonstrate that the answer is sensitive both to how locality is understood in the generalised context and the behaviour of the truth-defining algebra. In the case of Hanf's theorem, we will show that the theorem fails for the natural understanding of local neighbourhoods, but is recoverable with an alternative understanding for well-connected residuated lattices. For Gaifman's theorem, rather than consider Gaifman normal forms directly we focus on the main lemma of the theorem from textbook proofs - that models which satisfy the same basic local sentences are elementarily equivalent. We prove that for a number of different understandings of locality, provided the algebra is well-behaved enough to express locality in its syntax, this main lemma can be recovered. In each case we will see the importance of an order-interpreting connective which creates a link between the modelling relation for models and formulas and the valuation function from formulas into the algebra. This link enables a syntactic encoding of back-and-forth systems providing the main technical ingredient to proofs of the main locality results.

A canonical result in model theory is the homomorphism preservation theorem (h.p.t.) which states that a first-order formula is preserved under homomorphisms on all structures if and only if it is equivalent to an existential-positive formula, standardly proved via a compactness argument. Rossman (2008) established that the h.p.t. remains valid when restricted to finite structures. This is a significant result in the field of finite model theory. It stands in contrast to the other preservation theorems proved via compactness where the failure of the latter also results in the failure of the former (Ajtai, Gurevich (1987) and Tait (1959)). Moreover, almost all results from traditional model theory that do survive to the finite are those whose proofs work just as well when considering finite structures. Rossman’s result is interesting as an example of a result which remains true in the finite but whose proof uses entirely different methods. It is also of importance to the field of constraint satisfaction due to the equivalence of existential-positive formulas and unions of conjunctive queries (Chandra and Merlin (1977)). Adjacently, Dellunde and Vidal (2019) established a version of the h.p.t. holds for a collection of first-order many-valued logics, namely those whose structures (finite and infinite) are defined over a fixed finite MTL-chain. In this article, we unite these two strands. We show how one can extend Rossman’s proof of a finite h.p.t. to a very wide collection of many-valued predicate logics. In doing so, we establish a finite variant to Dellunde and Vidal’s result, one which not only applies to structures defined over algebras more general than MTL-chains but also where we allow for those algebras to vary between models. We identify the fairly minimal critical features of classical logic that enable Rossman’s proof from a model-theoretic point of view, and demonstrate how any non-classical logic satisfying them will inherit an appropriate finite h.p.t. This investigation provides a starting point in a wider development of finite model theory for many-valued logics and, just as the classical finite h.p.t. has implications for constraint satisfaction, the many-valued finite h.p.t. has implications for valued constraint satisfaction problems.

StereoBit is an embedded application for the SpaceCube family of hybrid onboard processors developed by NASA's Goddard Space Flight Center under sponsorship of the Earth Science Technology Office. StereoBit applies structure from motion algorithms to measure disparities between clouds being tracked from multiple angles to enable 3D resolution of atmospheric motion, which is an important Decadal Survey objective. Our Advanced Information Systems Technology project has the objectives of developing and demonstrating StereoBit for a future mission architecture employing a constellation of CubeSats and to mature the capabilities of the community to program the SpaceCube- family of processors for science applications.