Fagin's seminal result characterizing NP in terms of existential second-order logic started the fruitful field of descriptive complexity theory. In recent years, there has been much interest in the investigation of quantitative (weighted) models of computations. In this paper, we start the study of descriptive complexity based on weighted Turing machines over arbitrary semirings. We provide machine-independent characterizations (over ordered structures) of the weighted complexity classes NP[S], L[S], FP[S], FPLOG[S], FPSPACE[S], and FPSPACEpoly[S] in terms of definability in suitable weighted logics for an arbitrary semiring S. In particular, we state and prove weighted versions of Fagin's theorem (even for arbitrary structures, not necessarily ordered, provided that the semiring is idempotent and commutative), the Immerman-Vardi's theorem (originally for P) and the Abiteboul-Vianu-Vardi's theorem (originally for PS PACE). We also discuss a recent open problem proposed by Eiter and Kiesel. Recently, the above mentioned weighted complexity classes have been investigated in connection to classical counting complexity classes. Furthermore, several classical counting complexity classes have been characterized in terms of particular weighted logics over the semiring & Nopf; of natural numbers. In this work, we cover several of these classes and obtain new results for others such as NPMV, (R) P, or the collection of real-valued languages realized by nondeterministic polynomial-time real-valued Turing machines. Furthermore, our results apply to classes based on many other important semirings, such as the max-plus and the min-plus semirings over the natural numbers which correspond to the classical classes MaxP[O(log n)] and MinP[O(log n)], respectively.

Abstract This paper studies which truth-values are most likely to be taken on finite models by arbitrary sentences of a many-valued predicate logic. The classical zero-one law (independently proved by Fagin and Glebskiĭ et al.) states that every sentence in a purely relational language is almost surely false or almost surely true, meaning that the probability that the formula is true in a randomly chosen finite structures of cardinal n is asymptotically $0$ or $1$ as n grows to infinity. We obtain generalizations of this result for any logic with values in a finite lattice-ordered algebra, and for some infinitely valued logics, including Łukasiewicz logic. The finitely valued case is reduced to the classical one through a uniform translation and Oberschelp’s generalization of the zero-one law. Moreover, it is shown that the complexity of determining the almost sure value of a given sentence is PSPACE-complete (generalizing Grandjean’s result for the classical case), and for some logics we describe completely the set of truth-values that can be taken by sentences almost surely.

Codd's Theorem, a fundamental result of database theory, asserts that relational algebra and relational calculus have the same expressive power on relational databases. We explore Codd's Theorem for databases over semirings and establish two different versions of this result for such databases: the first version involves the five basic operations of relational algebra, while in the second version the division operation is added to the five basic operations of relational algebra. In both versions, the difference operation of relations is given semantics using semirings with monus, while on the side of relational calculus a limited form of negation is used. The reason for considering these two different versions of Codd's theorem is that, unlike the case of ordinary relational databases, the division operation need not be expressible in terms of the five basic operations of relational algebra for databases over an arbitrary positive semiring; in fact, we show that this inexpressibility result holds for bag databases, as well as for databases over the tropical semiring.

Ehrenfeucht-Fraïssé games provide means to characterize elementary equivalence for first-order logic, and by standard translation also for modal logics. We propose a novel generalization of Ehrenfeucht-Fraïssé games to hybrid-dynamic logics which is direct and fully modular: parameterized by the features of the hybrid language we wish to include, for instance, the modal and hybrid language operators as well as first-order existential quantification. We use these games to establish a new modular Fraïssé-Hintikka theorem for hybrid-dynamic propositional logic and its various fragments. We study the relationship between countable game equivalence (determined by countable Ehrenfeucht-Fraïssé games) and bisimulation (determined by countable back-and-forth systems). In general, the former turns out to be weaker than the latter, but under certain conditions on the language, the two coincide. As a corollary we obtain an analogue of the Hennessy-Milner theorem. We also prove that for reachable image-finite Kripke structures elementary equivalence implies isomorphism.

Abstract Lindström’s theorem obviously fails as a characterization of first-order logic without identity ( $\mathcal {L}_{\omega \omega }^{-} $ ). In this note, we provide a fix: we show that $\mathcal {L}_{\omega \omega }^{-} $ is a maximal abstract logic satisfying a weak form of the isomorphism property (suitable for identity-free languages and studied in [11]), the Löwenheim–Skolem property, and compactness. Furthermore, we show that compactness can be replaced by being recursively enumerable for validity under certain conditions. In the proofs, we use a form of strong upwards Löwenheim–Skolem theorem not available in the framework with identity.

Abstract By limiting the range of the predicate variables in a second-order language, one may obtain restricted versions of second-order logic such as weak second-order logic or definable subset logic. In this note, we provide an infinitary strongly complete axiomatization for several systems of this kind having the range of the predicate variables as a parameter. The completeness argument uses simple techniques from the theory of Boolean algebras. This article is dedicated to our friend John N. Crossley on the occasion of his 86th birthday.

In this paper we study frame definability in finitely valued modal logics and establish two main results via suitable translations: (1) in finitely valued modal logics one cannot define more classes of frames than are already definable in classical modal logic (cf. [27, Thm. 8]), and (2) a large family of finitely valued modal logics define exactly the same classes of frames as classical modal logic (including modal logics based on finite Heyting and MV-algebras, or even BL-algebras). In this way one may observe, for example, that the celebrated Goldblatt–Thomason theorem applies immediately to these logics. In particular, we obtain the central result from [26] with a much simpler proof and answer one of the open questions left in that paper. Moreover, the proposed translations allow us to determine the computational complexity of a big class of finitely valued modal logics.

Abstract In the style of Lindström’s theorem for classical first-order logic, this article characterizes propositional bi-intuitionistic logic as the maximal (with respect to expressive power) abstract logic satisfying a certain form of compactness, the Tarski union property and preservation under bi-asimulations. Since bi-intuitionistic logic introduces new complexities in the intuitionistic setting by adding the analogue of a backwards looking modality, the present paper constitutes a non-trivial modification of the previous work done by the authors for intuitionistic logic (Badia and Olkhovikov, 2020, Notre Dame Journal of Formal Logic, 61, 11–30).

This article continues the theoretical study of weighted structures in mathematical fuzzy logic focusing on the finite model theory of fuzzy logics valued on arbitrary finite$\mathrm{MTL}$-chains. We show that for any first-order (or infinitary with finitely many variables) formula$\varphi$, there is a truth-value that$\varphi$takes almost surely in every finite many-valued model and such that every other truth-value is almost surely not taken. This generalizes a theorem in the fuzzy setting due to Robert Kosik and Christian G. Fermüller.

This article is a contribution to the theoretical study of weighted structures in fuzzy logic. We consider an important item from classical model theory: the construction of models that do not have any collection satisfying certain prescribed properties, that is, an omitting types theorem. We generalize the work done by Cintula and Diaconescu (Omitting Types Theorem for Fuzzy Logics, IEEE Transactions on Fuzzy Systems 27(2):273-277, 2019), who solved the problem for standard one-sided types. Instead, we introduce types for fuzzy structures as pairs of sets of formulas with free variables (expressing, respectively, properties to be satisfied and those to be avoided) and prove the corresponding omitting types theorem in the framework of uninorm-based logics.

This paper is a contribution to graded model theory, in the context of mathematical fuzzy logic. We study characterizations of classes of graded structures in terms of the syntactic form of their first-order axiomatization. We focus on classes given by universal and universal-existential sentences. In particular, we prove two amalgamation results using the technique of diagrams in the setting of structures valued on a finite MTL-algebra, from which analogues of the Łoś-Tarski and the Chang-Łoś-Suszko preservation theorems follow.