The Schedule

Semiring semantics is based on the idea to evaluate logical statements not just by true or false, but by values in some commutative semiring.

In this context, the standard semantics appears as the special case when the Boolean semiring is used. Valuations in other semirings provide additional information, for instance about the number of succesful strategies, costs, confidence scores, or necessary access levels for evaluating logical statements.

Further, semirings of polynomials or formal power series permit us to track, which atomic facts are used (and how often) to establish the truth of a sentence in a given structure.

Semiring semantics originated in the provenance analysis for (positive) database query languages, such as positive relational algebra or datalog, but in the last years it has been systematically extended to many logical systems, including first-order logic, modal logic, and fixed-point logic.

This raises the question to what extent standard results and techniques of classical logic (and specifically finite model theory) extend to semiring semantics, and how such extensions depend on the choice of the underlying semiring.

We survey some of these results, and specifically focus on the study of 0-1 laws for random semiring interpretations.

(This is joint work with Guillermo Badia and Carles Noguera.)

We obtain asymptotic probabilistic truth-value laws on finite models, analogue of 0-1 laws of classical predicate logic, for any logic with values in a finite lattice-ordered algebra, and for some infinitely valued logics as Lukasiewicz logic. The finite valued case is reduced to the classical one through a uniform translation and Oberschelp's generalization of Fagin's 0-1 law. We address the issue of which truth-values actually arise as almost-sure values of formulas in a given logic. Under some algebraic assumptions it is possible to classify them exactly. For example, all values of Lukasiewicz logic Ln+1 are almost-sure, while for its &,V, ~ fragment, the sets of almost sure values are: {0, 1/2, 1} if n is even and {0, (n-1)/2n, (n+1)/2n, 1} if n is odd. The results may be extended to many valued modal logics.

We approach the study of projective algebras in varieties of (bounded) commutative integral residuated lattices. Our point of view is going to be algebraic, however the reader may keep in mind that projectivity is a categorical concept, and therefore our findings pertain to the corresponding algebraic categories as well. Being projective in a variety of algebras, or in any class containing all of its free objects, corresponds to being a retract of a free algebra, and projective algebras contain relevant information both on their variety and on its lattice of subvarieties.

In particular, as first observed by McKenzie (1972), there is a close connection between projective algebras in a variety and splitting algebrasin its lattice of subvarieties. The notion of splitting algebra comes from lattice theory, and

studying splitting algebras is particularly useful to understand lattices of

subvarieties, since a splitting algebra divides a subvariety lattice in a disjoint

union of a principal filter defined by its generated variety, and a principal

ideal.

The varieties of algebras that are the object of our study are relevant both in the realm

of algebraic logic and from a purely algebraic point of view. In fact, residuated structures arise naturally in the study of many interesting algebraic

systems, such as ideals of rings or lattice-ordered groups, besides encompassing the equivalent algebraic semantics (in the sense of Blok-Pigozzi (1989) of substructural logics. The Blok-Pigozzi notion of algebraizability entails

that the logical deducibility relation is fully and faithfully represented by the

algebraic equational consequence of the corresponding algebraic semantics,

and therefore logical properties can be studied algebraically, and viceversa.

Substructural logics are a large framework and include most of the interesting non-classical logics: intuitionistic logics, relevance logics, and fuzzy logics

to name a few, besides including classical logic as a special case. Therefore,

substructural logics on one side, and residuated lattices on the other, constitute a wide unifying framework in which very different structures can be

studied uniformly.

This is joint work with Sara Ugolini.

Modal logics are well-known formalisms that account for representing and reasoning about notions such as necessity, belief, uncertainty, knowledge, similarity, obligations, time, etc. For instance Halpern in his book "Reasoning about Uncertainty" discusses a large family of modal logics to reason about uncertainty. On the other hand, many-valued logical systems under the umbrella of the so-called mathematical fuzzy logic (in the sense of H\'ajek and followers) appear as suitable logical frameworks to formalize reasoning with gradual properties, i.e. notions whose satisfaction is a matter of degree. Therefore, if one is interested in reasoning involving both gradual concepts and some sort of modalities one is led to consider systems of many-valued modal logic. In this talk I will survey some two-layer many-valued modal systems to reason about different models of uncertainty, including probability, belief functions, necessities and imprecise probabilities, both in a qualitatively and quantitatively way. In these systems, the inner logic deals with the objects (events) over we quantify the uncertainty (that can be classical logic or other modal or many-valued logic), and an outer (many-valued) modal logic is used to reason about the involved modal notion itself (e.g. probabilistic or possibilistic uncertainty). They are relatively simple to axiomatise as they allow neither nested modalities nor mixed propositional and modal formulas. Typical and initial developments of these systems were fuzzy probability logics due to H\'ajek and colleagues where the outer logic is $[0, 1]$-valued {\L}ukasiewicz logic.

Acyclic hypergraphs are well known to give rise to database schemas with desirable structural and algorithmic properties. In particular, the sets of attributes of a schema form an acyclic hypergraph if and only if the local-to-global consistency property for relations over that schema holds, which means that every collection of pairwise consistent relations over the schema is globally consistent.

In this talk, we present results about the interplay between local and global consistency for bags (multisets). The first main result asserts that the sets of attributes of a schema form an acyclic hypergraph if and only if the local-to-global consistency property for bags over that schema holds. The second main result is a dichotomy theorem for the computational complexity of the global consistency problem for bags: if the schema is acyclic, then the global consistency problem for bags is solvable in polynomial time, while if the schema is cyclic, then the global consistency problem for bags is NP-complete. The latter result contrasts sharply with the state of affairs for relations, where, for each fixed schema, the global consistency problem for relations is solvable in polynomial time.

This is joint work with Albert Atserias at UPC, Barcelona.

Instead of discussing a particular result, we will present a list of open problems, but also of more fundamental conceptual challenges for many-valued FMT. The list amounts to a personal take on the field, rather than an overview that covers all relevant topics. In particular, we look for research questions where many-valued logics may have to offer new perspectives that are intrinsic to reasoning with graded propositions and predicates over finite models.

By an MV-set we understand a pair (E,X) where X is a set of unit vectors in a Hilbert space E such that the linear span of X is dense in E, and the scalar product of v and w is ≥ 0 for all v, w ∈ X. This scalar product, which always lies in [0,1], is understood as the identity degree of v and w. Building on MV-sets and uniformly continuous functions and relations defined on them, we construct a compact [0,1]-valued first-order Łukasiewicz logic, whose set of unsatisfiable formulas is recursively enumerable. In the particular case when X is an orthonormal basis of E we recover classical Skolem first-order logic with identity, constants, functions and relations. Our main tools are the Kolmogorov dilation theorem for positive semidefinite kernels, and the Tarski–Seidenberg decision method for elementary algebra and geometry. We discuss the finite model properties of this logic.

One can argue that finite model theory (FMT) started with Trakhtenbrot’s theorem, but what people call FMT now arose later and was related to the nascent computer science and complexity theory as well as (mathematical) logic. FMT emerged in database theory which for a long time was the main application of and justification for FMT.

My own entry to FMT is related to Trakhtenbrot’s theorem, which says that the set of finitely valid first-order formulas is not recursively enumerable. In that sense, there is no logic calculus for finite validity. Hence logics tailored for computational complexity.

The database justification of FMT turned out to be flawed to an extent. A query may manipulate numbers that do not even appear in the database, which shows that a numerical structure is involved. Hence metafinite model theory.

Yet, bona fide FMT is useful for computational purposes.

BIO: Yuri Gurevich is Professor Emeritus at the University of Michigan. The last 20 years of his career he was a Principal Researcher at Microsoft Research Redmond. He is a Fellow of AAAS, ACM, EATCS, and Guggenheim, a foreign member of Academia Europaea, and Dr. Honoris Causa of a Belgian and a Russian universities.

Despite an undercurrent of finite algebra focus, much of classical universal algebra has avoided the depth of finite model theoretic consideration that relational signatures have received. We explore some of the exceptions to this, as well as some interesting examples and results that might invigorate further exploration of the finite model theory of universal algebra.

Seese’s conjecture for finite graphs states that monadic second-order

logic (MSO) is undecidable on all graph classes of unbounded

clique-width. It remains open thirty years after it was first

formulated. In this talk, I outline an approach to the conjecture based

on classifying classes of unbounded clique-width.

This is joint work with Abhisekh Sankaran

In this talk I will address many-valued modal logics, understood as the logics arising from Kripke models evaluated over residuated lattices. These logics are defined from their semantics, and formulating corresponding axiomatic systems for these logics is one of the main problems under study up to now. We focus in this presentation on a problem arising from the axiomatization of the modal logic of the Kripke frames with a crisp accessibility relation evaluated over the standard Lukasiewicz algebra. In particular, in previous works, a Hilbert style axiomatic system was defined that is strongly complete with respect to the usual relational semantics (i.e., complete also for infinite sets of premises). This system, however, requires an infinitary inference rule (with countably many premises), and the question of whether its finitary companion can be axiomatized (meaning, as usual, axiomatized by a R.E set of rules), remained open.

We will see that such an axiomatization cannot exist for the global modal logic, by the combination of three properties: undecidability of the global consequence over finite models of the class, decidability of the propositional logic and completeness of the global consequence (over arbitrary models) with respect to so-called witnessed models. As a consequence, it can be proven that the analogous logic over the standard product logic cannot be axiomatized either.

Many generalizations of the basic setting of model theory have been

proposed over the years. One of the more radical departures from the

classical picture was the many-valued generalization of the

interpretation of predicate symbols, where relations are conceived as

functions that assign, to each tuple of elements of the domain, values

from a set that contains more than just the two classical values true

and false.

There are at least three different origins of research on these

structures: Boolean-valued models, continuous model theory, and

semantics of predicate many-valued logics. There are many papers

studying basic and advanced model-theoretic properties of these

structures, mostly focused on particular approaches and sets of problems

with different levels of generality and mathematical sophistication.

In my talk I present variants of basic notions of abstract model theory

tailored to handle graded models and argument that the emerging theory

could serve an abstract framework for study of such models.

A rule is passive for a logic L if there is no substitution making its premises a theorem for L, and L is said to be passively structurally complete if all of its passive rules are derivable in L.

Suppose now that L is algebraizable with equivalent algebraic semantics a quasivariety Q. From a model-theoretic perspective, the passive structural completeness (or PSC) of L corresponds to the fact that the nontrivial members of Q all satisfy the same existential positive sentences (Moraschini et al.). From a different perspective, since a rule is passive exactly when its premises are not unifiable, the study of PSC is connected to the study of unification problems for the logic, or equivalently for its equivalent algebraic semantics, by Ghilardi's algebraic approach to unification.

In joint work with Aglianò, we show a new characterization for PSC in quasivarieties, which has an interesting interpretation in substructural logics in general, and in fuzzy logics in particular. As part of this investigation, we also present new results about the unification type of some relevant fuzzy logics, seen from the algebraic perspective. In particular, we show that product algebras, nilpotent minimum algebras, and the variety generated by perfect MV-algebras, all have strong unitary unification type.

The speaker will talk about applying theory to practice, with a focus on three IBM case studies. In the first case study, the practitioner initiated the interaction. This interaction led to the following problem. Assume that there is a set of “voters” and a set of “candidates”, where each voter assigns a numerical score to each candidate. In the spirit of real-valued logics, there is a scoring function (such as the min or the mean), and a consensus ranking is obtained by applying the scoring function to each candidate’s scores. The problem is to find the top k candidates, while minimizing the number of database accesses. The speaker will present an algorithm that is optimal in an extremely strong sense: not just in the worst case or the average case, but in every case! Even though the algorithm is only 10 lines long (!), the paper containing the algorithm won the 2014 Gödel Prize, the top prize for a paper in theoretical computer science.

The interaction in the second case study was initiated by theoreticians, who wanted to lay the foundations for “data exchange”, in which data is converted from one format to another. Although this problem may sound mundane, the issues that arise are fascinating, and this work made data exchange a new subfield, with special sessions in every major database conference. This work won the 2020 Alonzo Church Award, the highest prize for research in logic and computation.

The third case study, specifically on real-valued logic, arose as part of a large “Logical Neural Nets” (LNN) project at IBM. The inputs to, say, an “and” gate could be any numbers in the interval [0,1]. The system builders of LNN wanted a sound and complete axiomatization for real-valued logic, which this recent work provides for essentially every real-valued logic. It also allows weights, where the importance of some formulas can be greater than that of other formulas.

This talk will be completely self-contained. The talk is aimed at both theoreticians and practitioners, to show them the mutual benefits of working together.

In the traditional so-called Tarski’s Truth Definition the semantics of first order logic is defined with respect to an assignment of values to the free variables. A richer family of semantic concepts can be modelled if semantics is defined with respect to a set (a “team”) of such assignments. This is called team semantics. One, but not the only, possible interpretation of a team is vagueness about the right assignment. Examples of semantic concepts available in team semantics but not in traditional Tarskian semantics are the concepts of dependence and independence. It has emerged that teams appear naturally in several areas of sciences and humanities. In my talk I will give a quantitative analysis of team properties of finite models in terms of dimension.

This is joint work with L. Hella and K. Luosto.

(Joint work with Luca Reggio)

A well-known theorem of classical model theory due to Robinson states that the (first-order) theory of totally ordered abelian groups has a model completion. However, it was proved by Glass and Pierce that this is not the case for the theory of lattice-ordered abelian groups. Similarly, it was proved by Lacava and Saeli that the theory of totally ordered MV-algebras has a model completion, but not the theory of all MV-algebras. In this talk, we will generalize these negative results to see that the theory of a variety of commutative pointed residuated lattices has a model completion if and only if the variety admits uniform deductive interpolation and has equationally definable principal congruences. We will also see how positive model completion results can be rescued for varieties that admit uniform deductive interpolation by adding an additional binary operator.

The probabilistic logic FP(Ł, Ł) was axiomatized with the aim of presenting a formal setting for reasoning about the probability of infinite-valued Łukasiewicz events. Besides several attempts, proving that axiomatic system to be complete with respect to a class of standard models remained an open problem since the first paper on FP(Ł, Ł) was published in 2007. In this talk we present a solution to it. In particular we introduce two semantics for that probabilistic system: a first one based on Łukasiewicz states and a second one based on regular Borel measures and we prove that FP(Ł,Ł) is complete with respect to both these classes of models. Further, we will show that the finite model property holds for FP(Ł,Ł).

The standard approach to algorithm development is to focus on a specific problem and develop for it a specific algorithm. Codd's introduction of the relational model in 1970 included two fundamental ideas: (1) Relations provide a universal data representation formalism, and (2) Relational databases can be queried using first-order logic. Realizing thes ideas required the development of a meta-algorithm, which takes a declarative query and executes it with respect to a database. In this talk, I will describe this approach, which I call Logical Algorithmic, in detail, and explore its profound ramification.

Kleene's logic with its truth values true, false, and unknown is ubiquitous in CS applications, ever since SQL (the third most common programming language according to the latest stackoverflow survey) introduced it all way back in 1986 as a way of handling incomplete data. But have they chosen the right logic? Could they have done without unknown? And if they could have - but didn't- what can we do it about it now? The answers (yes, yes, something) will be elaborated on in the talk.

(This is joint work with Ronald Fagin)

We will study the first-order (as well as modal) logic of multidimensional sentences (generalizing the definition of Fagin et al: Foundations of Reasoning with Uncertainty via Real-valued Logics, arXiv:2008.02429v2, 2021) when the models considered all have the same fixed domain (which may be of any fixed cardinality, either finite or infinite). The key result is a completeness tehorem that follows the strategy of Fagin et al for the propositional case. We will show how our approach leads to uniform axiomatizations of the validities of many prominent first-order real-valued logics (since this includes several logics that are not recursively enumerable for validity, our system in general does not yield a recursive enumeration of theorems). Also we will obtain a 0-1 law for finitely-valued versions of these logics. Finally, we will remove the restriction of a fixed domain and provide a completeness theorem for the first-order logic of multidimensional sentences on arbitrary domains.

I'll talk about how I used finite models to discover the simplest possible axiom system for Boolean algebra, and about how finite models provide a way to investigate features of the space of all possible axiom systems. I'll describe how finite models provide a dual to proofs in metamathematics, and I'll show visual and other examples of how this works. Models can be thought of as defining reference frames in metamathematical space, and I'll talk about how they also relate to reference frames in physics, and in the recently-introduced ruliad formed from the entangled limit of all possible computations.