ABSTRACT. Emile Borel defined normality more than one hundred years ago to formalize a basic form of randomness for real numbers Many of his questions are still open, such as whether pi, e or square root of 2 are normal to some base, as well as his conjecture that the irrational algebraic numbers are absolutely normal. In this talk I will highlight some theorems on normal numbers proved with tools from computability theory, automata theory and descriptive set theory, and I will point out some open questions.

ABSTRACT. Determinacy of infinite two-player games is a topic of descriptive set theory that has triggered intensive research in theoretical computer science since 1957 when A. Church formulated his “synthesis problem” (regarding the construction of circuits with infinite behavior from logical specifications). In the first part of the lecture we review the fascinating development of the algorithmic theory of infinite games that was started by Church’s problem, that enriched automata theory and related fields, and that led to interesting applications in verification and program synthesis. In the second part we turn to the question how to lift this theory from the case of the Cantor space (where a play is a sequence of bits) to the case of the Baire space (where a play is a sequence of natural numbers). While this step does not involve difficulties in classical descriptive set theory, the algorithmic approach raises non-trivial questions since it requires to consider automata that work over infinite alphabets. We present recent results (joint work with B. Brütsch) that provide a solution of Church’s synthesis problem in this context, and we point to numerous questions that are still open.

ABSTRACT. Model theory studies combinatorial tameness properties of mathematical structures. As such it has an ever growing ambition to offer new tools and new approaches to many different areas of mathematics. In the last few decades, its range of applications has greatly expanded, at times in unexpected directions. So much so that the subject looks nothing like what it was 30 or 40 years ago.

In this talk—meant to be accessible to a wide audience---I will present a couple of themes of present research in model theory and try to give a feel for the area, what has been achieved and what might lie ahead.

ABSTRACT. Schema mapping is a high-level specification of the relationship between two database schemas. For the past fifteen years, schema mappings have played an essential role in the modeling and analysis of important data inter-operability tasks, such as data exchange and data integration. Syntactically, schema mappings are expressed in some schema-mapping language, which, typically, is a fragment of first-order logic or second-order logic. In the first part of the talk, we will introduce the main schema-mapping languages, will discuss the fundamental structural properties of these languages, and will then use these structural properties to obtain characterizations of various schema-mapping languages in the spirit of abstract model theory. In the second part of the talk, we will examine schema mappings from a dynamic viewpoint by considering sequences of schema mappings and studying the convergence properties of such sequences. To this effect, we will introduce a metric space that is based on a natural notion of distance between sets of database instances and will investigate pointwise limits and uniform limits of sequences of schema mappings. Among other findings, it will turn out that the completion of this metric space can be described in terms of graph limits arising from converging sequences of homomorphism densities.

ABSTRACT. Homomorphisms between relational structures play a central role in finite model theory, constraint satisfaction and database theory. What could it mean to quantize these structures? A central theme in quantum computation is to show how quantum resources can be used to gain advantage in information processing tasks. In particular, non-local games have been used to exhibit quantum advantage in boolean constraint satisfaction, and to obtain quantum versions of graph invariants such as the chromatic number. We show how quantum strategies for homomorphism games between relational structures can be viewed as Kleisli morphisms for a quantum monad on the (classical) category of relational structures and homomorphisms. We show a general connection between these notions and state-independent quantum realizations of strong contextuality in the Abramsky-Brandenburger formulation of contextuality. We use these results to exhibit a wide range of examples of contextuality-powered quantum advantage, and to unify several apparently diverse strands of previous work.

ABSTRACT. In this short presentation, I'd like to give a synthetic overview of the main constructive proof, due to Durand, Lautemann and More, that first-order can count up to a polylogarithmic number. In doing so, we will see how it can be generalized to derive minimal requirements for sublogarithmic counting. Our goal, so far unfulfilled, is to answer the following question: Can a logic count beyond a constant, but not up to polylog?

ABSTRACT. In general, quantification of first-order variables leads to dependencies between quantified variables. Such dependencies become explicit when Skolemization is applied. This talk presents recent research concerning syntactic properties of first-order formulas that entail a certain degree of independence of existentially quantified variables from universally quantified ones (we assume positive polarity of the respective quantifier occurrences). The discovered patterns of (in)dependence are more subtle than a strict classification into full dependence vs. full independence as encouraged by Henkin-style quantification.

One application of the gained insights is the definition of novel decidable classes of first-order sentences that syntactically extend already known classes, such as the Bernays-Schönfinkel-Ramsey fragment (relational $\exists^* \forall^*$ sentences with equality), the monadic first-order fragment, and the Ackermann fragment (relational $\exists^* \forall \exists^*$ sentences). One such extended class is the separated fragment, which has recently been introduced. Its defining principle is that universally and existentially quantified variables may not occur together in atoms.

Moreover, the analysis of implicit dependencies between quantified variables may be beneficial for automated reasoning, as the search space theorem provers have to navigate becomes smaller if Skolem functions have lower arity, and since this arity is determined by the dependencies of the represented variables on other variables.

ABSTRACT. This paper revisits the well-established relationship between modal $\mu$ calculus and parity games. It considers whether the descriptive complexity of $L_\mu$ model checking games, previously known to depend on the syntactic complexity of a formula, depends in fact on its semantic complexity.

Indeed, model-checking a $L_\mu$ formula of syntactic index $I$ reduces to solving parity games of the same index; Conversely, a formula of index $I$ suffices to describe the winning regions of parity games of index $I$. This paper shows that this relationship extends to account for the semantic complexity of formulas: if the winning regions of the model-checking games generated by a formula $\Psi$ can be describes by a formula $\Phi$ -- written $\Phi$ interprets $\Psi$ -- then $\Psi$ is equivalent to a formula of the same index as $\Phi$. It then considers the converse problem: if a formula $\Psi$ is semantically of index $I$, that is to say equivalent to some formula of index $I$, then is it interpreted by some formula of index $I$? I show that this is the case for the alternation class $ML$, and for the classes $\Pi^\mu_1$ and $\Sigma^\mu_2$ as long as the input is in disjunctive form, and finally for any disjunctive alternation class, as long as the input formula is in co-disjunctive form.

ABSTRACT. In the study of justification logic, the role played by the proof term operator $ + $ always needs further explication. In this paper we will clarify its function in the project, and propose a variant justification logical system in which $+$ gets the intuitive interpretation of set-theoretical \emph{union} of proof terms. The intended epistemic semantics for the system will be given, followed by the completeness theorem. We will then investigate the formal relation between the variant and the original logical system of justification, and this investigation leads to the \emph{realization theorem} for the new system. Finally, we will discuss the possible arithmetic semantics that can be supplemented to the proposed system.

ABSTRACT. Takeuti and Yasumoto gave a systematic approach for constructing Boolean valued models of bounded arithmetic and proved its connections to the separation problems. We will reformulate it in terms of two-sort bounded arithmetic and reprove some theorems in the new framework. We also show that the Boolean valued method can be applied to other complexity classes by replacing the base Boolean algebra. Finally we will give some open problems concerning the relation between P = NP problem and Takeuti-Yasumoto’s generic model.

ABSTRACT. This paper studies the so-called generalized connectives of multiplicative linear logic (MLL). These general connectives were formerly introduced by Girard but most of the results known after then are due to Danos and Regnier. A multiplicative generalized (or n-ary) connective can be defined by two pointwise orthogonal sets of partitions, P and Q, over the same domain {1, ..., n}. Actually, we can use partitions according two different points of view (i.e., two syntaxes), sequential and parallel, preserving the same notion of orthogonality (P ⊥ Q). However, general connectives are more expressive in the parallel syntax since this allows to represent correct proofs, namely proof nets, containing generalized connectives (n-ary links) that cannot be defined (or decomposed) by means of the basic multiplicative connectives of linear logic, Par and Tensor. Dislike the standard MLL proof nets, some of these generalized proof nets do not correspond (sequentialize) to any sequential proof, if we exclude the trivial axioms. Despite the question appears "per se" surprising, there does not exist at the present time any study that characterizes these non sequentializable proof nets (except few examples). So, in this paper, we make the effort to characterize, at least, an ”elementary“ class of non decomposable connectives: the class of entangled connectives. Actually, entangled connectives are the “smallest” generalized multiplicative connectives (w.r.t. the number of partitions or, equivalently, the number of rules), if we exclude, of course, the basic ones. Moreover, every entangled connective P satisfies the property of being a type i.e., it is equal to its double orthogonal, P = P ⊥⊥ . This fact is crucial in order to precisely identify among the entangled connectives those ones that are not decomposable by means of the basic Par and Tensor. More generally, non decomposable generalized connectives witness a genuine asymmetry between proof nets and sequent proofs since the former ones allow to express a kind of parallelism (of connectives) that the latter ones cannot do.

ABSTRACT. We present a new game semantics for Martin-L\"of type theory (MLTT); our aim is to give a mathematical and intensional explanation of MLTT. Specifically, we propose a category with families (a categorical model of MLTT) of a novel variant of games, which induces an injective (when Id-types are excluded) and surjective interpretation of the intensional variant of MLTT equipped with unit-, empty-, N-, pi-, sigma-, Id-types and the cumulative hierarchy of universes (which in particular formulates the difference between types and terms of universes) for the first time in the literature (as far as we are aware). Our games generalize the existing notion of games, and achieve an interpretation of dependent types and universes in an intuitive yet mathematically precise manner; our strategies can be seen as algorithms underlying programs (or proofs) in MLTT, achieving the research aim except that a more fine-grained interpretation of Id-types is left as future work. As in the case of existing game semantics, this framework would be applicable to a wide range of programming languages with dependent types.