We study the status of preservation theorems such as the Łoś-Tarski theorem and the homomorphism preservation theorem in the context of semiring semantics. Semiring semantics has its origins in the provenance analysis of database queries. Depending on the underlying semiring, it allows us to track which atomic facts are responsible for the truth of a statement or practical information about the evaluation such as costs or confidence. The systematic development of semiring semantics for first-order logic and other logical systems raises the question to what extent classical model-theoretic results can be generalised to this setting and how such results depend on the underlying semiring. The definitions of semantic properties such as preservation under extensions, substructures, or homomorphisms naturally generalise to the setting of semiring semantics. However, the status of the corresponding preservation theorem strongly depends on the algebraic properties of the particular semirings. We prove that these preservation theorems do indeed hold for all lattice semirings (a quite large class, encompassing practically relevant semirings and in particular all min-max semirings). The proofs combine adaptations of the classical compactness and amalgamation methods with specific reduction methods for logical entailment that have been developed in semiring semantics. On the other side, variants of the existential preservation theorem fail for many other semirings, including the tropical semiring, the Viterbi semiring, the Łukasiewicz semiring, and the natural semiring. Surprisingly, the existential preservation theorem does hold for finite interpretations in a number of semirings, including all lattice semirings. Thus, the situation for these semirings is in sharp contrast to the Boolean case, where the Łoś-Tarski theorem holds in general, but not in the finite.
翻译:我们研究半环语义背景下Łoś-Tarski定理和同态保存定理等保存定理的成立情况。半环语义源于数据库查询的溯源分析。根据底层半环的不同,它允许我们追踪哪些原子事实导致语句的真值,或关于评估的实用信息(如成本或置信度)。一阶逻辑及其他逻辑系统中半环语义的系统性发展提出了两个问题:经典模型论结果能在多大程度上推广至此框架,以及此类结果如何依赖于底层半环。语义性质(如扩展下保持、子结构下保持或同态下保持)的定义可自然推广至半环语义框架。然而,相应保存定理的成立情况强烈依赖于特定半环的代数性质。我们证明:对于所有格半环(一个相当广泛的类,涵盖实际相关的半环,特别是所有min-max半环),这些保存定理确实成立。证明结合了经典紧致性和融合方法的改造,以及半环语义中发展的逻辑蕴涵特定约简方法。另一方面,存在性保存定理的变体对于许多其他半环(包括热带半环、维特比半环、Łukasiewicz半环和自然半环)均不成立。令人惊讶的是,存在性保存定理在有限解释下对包含所有格半环在内的多种半环成立。因此,这些半环的情形与布尔情况形成鲜明对比——后者中Łoś-Tarski定理在一般情形成立,但在有限情形不成立。