Horizons of Logic, Computation and Definability: Symposium in Honour of Lauri Hella's 60th birthday

The motivation for this talk will take us back to my doctoral work under the supervision of Stephan Foldes and Lauri Hella. One of the many topics that were investigated was normal form systems for representing Boolean functions. There are several was to formalize this intuitive notion of normal form system (NFS). Our first proposal was essentially to consider (NFS) of Boolean functions as factorizations of the class of all Boolean functions into a composition of clones. This formalism enabled a preordering of NFSs that led to a classification of NFSs. In particular, it shows that the median NFS (that uses a single nontrivial connective, the ternary median or majority function) is more "efficient" than classical CNF, DNF and the polynomial NFSs. However, this formalism failed to take into account other natural NFSs nor to structural properties of terms and connectives.

Recently, we revisited this topic with my doctoral student Pierre Mercuriali and reconsidered NFSs as being sets of stratified terms over a fixed set of term connectives. For a fixed NFS A, the complexity of a Boolean function f with respect to A is the minimum of the sizes of terms in A that represent f. This induces a preordering of NFSs that includes the latter one: an NFS A is polynomially as efficient as an NFS B if there is a polynomial P with integer coefficients such that the complexity of any Boolean function f with respect to A is at most the value of P in the complexity of f with respect to B.

In this talk we will describe those NFSs that are optimal, i.e., that are minimal with respect to the latter preorder, and we will show that these minimal NFSs are all polynomially equivalent to the median NFS. Moreover, we will address some natural questions, e.g.: Does optimality depend on the arity of connectives? Does it depend on the number of connectives used? We will provide (perhaps surprising) answers to these questions and, if time allows, we will discuss the complexity of some inherent problems such as that of finding minimal representations for a given optimal NFS.

The results presented were obtained in joint works with S. Foldes, E. Lehtonen, P. Mercuriali, R. Péchoux and A. Saffidine. Talk (pdf)

Formulas in logic, defining properties of finite structures, can be translated to families of circuits which satisfy a natural symmetry condition. In joint work with Matt Anderson I showed that the expressive power of fixed-point logic with counting is exactly characterized by polynommially-uniform families of symmetric circuits in a basis of gates including the Boolean functions and majority functions. The technical proofs rely heavily on the fact that the Boolean functions and the majority function are all *symmetric* functions in the sense of being invariant to all permutations of the input. In this talk I consider extensions with gates that are not necessarily symmetric and show how to relate them to logics with operators (such as generalized quantifiers) which define the corresponding operations.

This is joint work with Gregory Wilsenach. Talk (pdf)

I will present game-theoretic semantics (GTS) for the branching time temporal logic CTL. I will compare that semantics with the traditional, compositional semantics for CTL and will show how the GTS naturally generates alternative 'time-bounded' semantics, where time limits are imposed on players to demonstrate the truth of the formula they claim to be true. I will then discuss some aspects of CTL with the non-standard finitely-bounded semantics and will present briefly some technical results, including complete tableaux and axiomatic system for it.

The talk is based on a joint work with Antti Kuusisto (University of Bremen) and Raine Rönnholm (University of Tampere). Talk (pdf)

M. Hall introduced free projective planes πⁿ, 4≤n≤ω, in [Ha]. In the talk, we start by looking at the basic concepts around these planes and then we will discuss on the properties of the theory of these planes i.e. the properties of the theory that consists of all first-order sentences true in every free projective plane. This talk is based on an ongoing research with Gianluca Paolini.

Reference
M. Hall, Projective planes, Transactions of American Mathematical Society, vol. 54, 1943, 229-277.

G. Kreisel has suggested that squeezing arguments, originally formulated for the informal concept of first order validity, should be extendable to second order logic, although he points out obvious obstacles. We develop this idea in the light of more recent advances and delineate the difficulties across the spectrum of extensions of first order logics by generalised quantifiers and infinitary logics. In particular we argue that if the relevant informal concept is read as informal in the precise sense of being untethered to a particular semantics, then the squeezing argument goes through in the second order case. Consideration of weak forms of Kreisel's squeezing argument leads naturally to reflection principles of set theory.

Constraint satisfaction comprises a broad class of fundamental algorithmic problems that are encountered across several different areas of computer science and artificial intelligence. In 1978, Schaefer characterized the computational complexity of all constraint satisfaction problems over the Boolean domain, a result that has become known as Schaefer's Dichotomy Theorem. We investigate an algebraization of Schaefer's framework in which the Fourier transform is used to represent constraints by multilinear polynomials. The polynomial representation of constraints gives rise to a relaxation of the notion of satisfiability for constraint satisfaction problems in which the values to variables are linear operators on some Hilbert space. For constraints given by a system of linear equations over the two-element field, this relaxation has received considerable attention in the foundations of quantum information, where such constructions as Mermin's magic square show that there are systems that have no solutions in the Boolean domain, but have solutions via operator assignments on some finite-dimensional Hilbert space. We completely characterize the classes of Boolean relations for which there is a gap between satisfiability in the Boolean domain and the relaxation of satisfiability via operator assignments. Our main result is established via the systematic use of primitive-positive definability and logical reductions that preserve satisfiability gaps.

This is joint work with Albert Atserias at the Polytechnic University of Catalonia (UPC) and Simone Severini at University College London (UCL). Talk (pdf)

Model counting problems offer a general, logic-based approach to enumerative combinatorics. The model counting problem of a first-order sentence takes as input an integer n---typically given in unary---and outputs the number of n-element models of the sentence; the domain of the models is taken to be {0,...,n-1}. It has recently been shown that this problem is in polynomial time for all sentences of two-variable logic. We extend this result to some relevant extensions of two-variable logic, and we also provide a complete classification of the first-order prefix classes according to the complexities of the associated model counting problems.

One of the central research fields of Finnish logicians, which has also been quite a distinctive feature of Finnish logic, has been the study of generalized quantifiers. I shall survey some contributions to this field from the point of view how Lauri's ideas affected my own research, and the research of quantifiers in general. Natural topics are thus games of the Ehrenfeucht–Fraïssé type, quantifiers hierarchies and definability theory of quantifiers. My survey starts from 1980's and ends in the results of this decade; time permitting I shall discuss the future of the quantifier theory.

In early 2010, a group of logicians and computer scientists from Tampere and Helsinki joined forces and started to explore connections between modal logic and weak models of distributed computing. Our collaboration initiated the study of distributed computing from the perspective of descriptive complexity theory.

The field is still at its infancy, but others are already following. In 2017, Fabian Reiter defended his doctoral thesis at Paris Diderot. To my knowledge, this is the first PhD thesis about the logical characterisations of models of distributed computing; it builds on the foundations of the work that we did here in Finland, and extends it in new exciting directions, far beyond what I envisioned to be possible in the near future.

In this talk I will give an overview of the development of the descriptive complexity theory for distributed computing, and in particular on the impact this has had on our understanding of the foundations of distributed computing. I will also explore some new ideas that arose from this line of research, such as the introduction of alternation (cf. alternating Turing machines) in models of distributed computing. Talk (pdf)

We define new fragments of higher-order logics of order three and above, and investigate their expressive power over finite models. The key unifying property of these fragments is that they all admit inexpensive algorithmic translations of their formulae to equivalent second-order logic formulae. That is, within these fragments we can make use of third- and higher-order quantification without paying the extremely high complexity price associated with them. The main fragment, denoted HO^i,P, is defined by restricting the size of the valuating i-th (and lower) order relations for the i-th order variables to be of a polynomial size w.r.t. the size of the model. Although theoretical in nature, the results reported here are more significant from a practical perspective. We believe that there are many examples of properties of finite models (queries from the perspective of relational databases) which can be simply and elegantly defined by formulae of the higher-order fragments studied in this work. For many of those properties, the equivalent second-order formulae can be very complicated and unintuitive.

By using the same strategy, it can be shown that for every i ≥ k ≥ j ≥ 4 the fragments of HO^i,exp(j-2) where the size of the valuating k-th order relations for the k-th order variables are restricted to be of size O(exp(j-2)) w.r.t. the size of the model, collapse to HO^j (we denote as exp(m) a function with a stack of m exponents 2, topped by O(n^O(1))).

As an example, we will briefly describe sketches of higher order formulae for some problems where the use of an order higher than the one that corresponds to their respective complexity, makes the formulas more intuitive and clear, and hence less likely to be incorrect.

In-progress joint work with Flavio Ferrarotti and Senén González. Talk (pdf)

Second-order transitive-closure logic, SO(TC), is an expressive declarative language that captures the complexity class PSPACE. Already its monadic fragment, MSO(TC), allows the expression of various NP-hard and even PSPACE-hard problems in a natural and elegant manner. As SO(TC) offers an attractive framework for expressing properties in terms of declaratively specified computations, it is interesting to understand the expressivity of different features of the language. In this talk we focuse on the fragment MSO(TC), as well on the purely existential fragment SO(2TC)(E); in 2TC, the TC operator binds only tuples of relation variables. We show that, with respect to expressive power, SO(2TC)(E) collapses to existential first-order logic. In addition we study the relationship of MSO(TC) to an extension of MSO(TC) with counting features (CMSO(TC)) as well as to order-invariant MSO. We show that the expressive powers of CMSO(TC) and MSO(TC) coincide. Moreover we establish that, over unary vocabularies, MSO(TC) strictly subsumes order-invariant MSO.

This is joint work with Flavio Ferrarotti and Jan Van den Bussche. Talk (pdf)

After a short review of generalized quantifiers in Tarski semantics, we turn to team semantics. Generalized quantifiers can be introduced in team semantics in (at least) three different ways: as atoms, relative atoms (to be defined), and as logical operations. The latter two lead to equivalent logics (at least) in the case of simply unary quantifiers. In this way generalized quantifiers give rise to new atoms. We focus on a particular one which we call the anonymity atom. The intuition behind this atom is the following: Suppose we have data about some individuals and the values of some attributes are publicly known while the values of some other attributes are sensitive personal data that should be protected from becoming public. Anonymity in this context means the impossibility to derive the values of the sensitive attributes from the values of the publicly known attributes, and this impossibility should be true of each individual. After introducing the anonymity atom we give axioms for it and prove an Armstrong-style Completeness Theorem for it.

Most logicians would agree that logical consequence is a central notion in logic. The dual notion of a logical constant has received less attention: one is usually satisfied on pragmatic grounds with a standard set of logical constants and doesn't worry much about why they are so special. Yet consequence depends on constants: as Bolzano and Tarski made precise, every choice of a set X of constants yields a corresponding consequence relation, defined in terms of truth preservation under replacement/reinterpretation of symbols outside X. How to choose X? Both Bolzano and Tarski emphasized the fundamental importance of this question, and admitted they had no answer (at the time: 1837 and 1936, respectively). However, intuitions about 'what follows from what' are stronger than those about constancy, and it makes sense to try to see how constants depend on consequence, by 'extracting' the constants from a given consequence relation. A natural Galois connection establishes the duality between sets of constants and Bolzano/Tarskian consequence relations.

Logical consequence relations are also defined syntactically, via rules. If such a relation coincides with Bolzano/Tarskian semantic consequence relative to the standard logical symbols with their standard interpretation, we have soundness and completeness: syntax matches semantics. But the other side of the coin, that semantics should match syntax in the sense that the meaning of the logical symbols is somehow determined by the relation of logical consequence, seems just as important. Such categoricity results were the main focus of Carnap's 1943 book The Formalization of Logic, but the topic has been rather neglected since. I will present some recent joint work with Denis Bonnay on these issues, applied to familiar logical languages.