LLAMA Seminar
Logo by Andreas Weiermann.
Logo by Andreas Weiermann.
This page concerns the Lectures on Logic and its Mathematical Aspects (LLAMA) seminar series at the Institute for Logic, Language & Computation (ILLC) of the University of Amsterdam.
Click to reveal the abstract.
Starting from the Thirties, Bruno de Finetti layed the ground for the development of subjective probability (also called Bayesian) in form of a betting game: In his setting, the probability of an event is the amount that a rational agent is willing to bet on it. de Finetti also proved that this point of view on probability is consistent with the widely used axiomatic approach. Indeed, it is possible to define a notion of coherence for the choices of the bets on the events and to prove that a book is coherent if, and only if, it can be extended to a probability measure on the Boolean algebra generated by the events. Coherence is therefore a bridge between subjective and objective, axiomatic, probability.
Another point of view on probability theory is the so-called frequentist approach. In this case, the probability of an event is defined by the frequency of that event based on previous observations. In this setting, it is common to define a statistical model that fits the observed data, and to derive the properties of the hidden probability distribution in this way. Perhaps surprisingly, subjective probability is related to frequentist probability again via de Finetti’s work, and in particular via the notion of exchangeability that, loosely speaking, shows how statistical models appear in a Bayesian framework, and how probabilities can come from statistics.
In this talk, we discuss the results of [1, 2]. In particular, we discuss the notion of coherence and exchangeability, and give a version of the celebrated de Finetti's theorems in a peculiar infinitary logic that expands the well known Lukasiewicz logic.
The Goldblatt-Thomason theorem provides a characterization of modally definable classes of Kripke frames. There is a version of this theorem for topological spaces with respect to the topological semantics interpreting the modal diamond as the closure operator. In this talk, we investigate the definability problems for topological spaces with respect to the topological derived-set operator. This is joint work with N. Bezhanishvili and D. Fernandez Duque.
The Dutch Association for Logic (VvL) will hold an annual in-person joint seminar organized by the University of Groningen. The event is inspired by the departmental logic seminars that are organized at each university, and aims to unify the universities for a collaborative seminar. Besides hosting a main speaker, the seminar will also be the location of the award ceremony of the VvL MSc Thesis Prize winners, who will give a short presentation of their thesis.
Uniform interpolation is a strengthening of interpolation in which the interpolant only depends on the premise or the conclusion of the implication. There are well-known logics with uniform interpolation, such as K and IPC. But not in all logics does interpolation imply this stronger version. The modal logics K4 and S4 are examples of this.
Why some logics with interpolation have the stronger property while others that seem quite similar do not is not quite clear, neither technically nor conceptually. Especially in proof theory there is the phenomenon of logics for which there is a perfectly constructive proof-theoretic proof of interpolation that does not extend to a proof of uniform interpolation. In this talk it will be shown how for reductive sequent calculi a proof-theoretic proof of interpolation does imply that the corresponding logic has uniform interpolation. Here a calculus is reductive if proof search in the calculus is terminating and it has some other desirable properties.
The motivation behind this research in universal proof theory is the search for methods to establish which logics do and which do not have good sequent calculi, meaning calculi with good structural properties. In the talk the connection between the technical part and this general aim will be explained.
The “happened-before” relation is an order relation over events playing a special role in formal verification. Pomset logic handles this relation logically, that is, as a proper connective of the logic. However, the proof-theoretical tools developed for this logic are limited to series-parallel orders.
In this talk I will present proof systems operating on graphs instead of formulas to overcome the restrictions coming from the use of in-line formulas. To this aim, I will recall some notions from graph theory and explain the proof theoretical methodologies required to prove analyticity and conservativity in this formalism.
Uniform interpolation is a property of logics that is stronger than the well-known Craig interpolation property, in the sense that a uniform interpolant only depends on the antecedent or the conclusion of the implication. It has close connections to so-called bisimulation quantification in Kripke models. Proof-theoretic methods proving uniform interpolation have been successfully applied to logics described by terminating sequent calculi. In this talk we turn to nested sequents. We reprove the uniform interpolation property for normal modal logics K, D, and T via terminating nested sequents. While our method of defining the interpolants is proof-theoretic, we use semantic notions including bisimulation modulo propositional variables to prove their correctness. We are also able to adjust our method to provide a direct proof of uniform interpolation for S5 using hypersequents.
This is joint work with Raheleh Jalali and Roman Kuznets.
A surprising result of Pitts (1992) says that propositional quantifiers are definable internally in intuitionistic propositional logic (IPC) - this result is commonly known as the uniform interpolation theorem for IPC. We recently completed a formalization of Pitts' result in the Coq proof assistant, and thus a verified implementation of the propositional quantifiers. Our Coq formalization in addition allowed us to extract an OCaml program that computes propositional formulas that realize intuitionistic versions of ∃p φ and ∀p φ from p and φ, and runs quickly on examples.
In this talk I will give some background for the result, and I will make some points about its proof that we clarified during its implementation, which also give some new insights about the "pen-and-paper" proof. In our implementation, as in Pitts' original proof, the propositional quantifiers are defined by a mutual induction based on Dyckhoff's proof calculus LJT. The correctness of the construction is then proved by an induction on the size of an LJT-proof. The techniques used and lessons learned from our implementation may also be of more general interest for verified implementations of other proof-theoretic results.
This is joint work with Hugo Férée (IRIF, Université Paris Cité).
The states of a deterministic finite automaton can be identified with collections of words, each state corresponding to the words arriving to the state, when computed by the automaton. But words can be ordered and among the many possible orders; a very natural one is the co-lexicographic one because it suggests a transfer of the order from words to the automaton’s states. This suggestion is, in fact, concrete and in a number of papers. Automata admitting a total ordering of states coherent with the co-lex ordering of the set of words reaching them have been proposed, studied, and implemented. Such a class of ordered automata—the Wheeler automata—turned out to be efficiently stored/searched; moreover, the set of words reaching each of their states have been proved to be intervals of the co-lexicographic order, implying some nice properties on languages accepted, determinization and the like.
Unfortunately not all automata can be totally ordered as previously outlined. However, automata can always be partially ordered using the co-lexicographic order over words, and an intrinsic measure of their complexity can be defined and effectively determined, as the minimum width of one of their admissible partial orders. We will show that this new concept of width of an automaton has useful consequences.
This talk is an overview of several work done in collaboration with
Transitive Closure Logic (TCL) enriches the language of first order logic with a recursive operator, expressing the transitive closure of a binary relation. Cyclic sequent calculi proofs for this logic have been introduced in the literature. In this talk, I will present a new cyclic proof system for TCL, which employs hypersequents. The main motivation behind this work is that, differently from sequent TCL proofs, hypersequent proofs for TCL successfully simulate cyclic proofs in the transitive fragment of Propositional Dynamic Logic (PDL+), without using the non-analytic rule of cut.
After introducing the cyclic hypersequent calculus for TCL, I will present two main results. First, I will sketch a proof of soundness for the calculus, which requires a more involved argument than the one used in traditional cyclic proofs. Second, I will show how PDL+ cyclic proofs can be translated into TCL hypersequent proofs. This result allows to lift the completeness result for cyclic PDL+ to the hypersequent calculus.
This talk is based on joint work with Anupam Das.
Cyclic proof systems permit derivations that are finite graphs rather than conventional derivation trees. The soundness of such proofs is ensured by a condition on the infinite paths through the derivation graph, known as the global trace condition. The usual proof strategy for showing soundness of a cyclic proof system is highly classical. If the cyclic proof system is that of an intuitionistic theory, such as Heyting arithmetic, a constructive soundness proof would be preferable.
We present ongoing work on a procedure which translates proofs in a cyclic proof system of Heyting arithmetic to proofs in a standard proof system of the same. We believe that this procedure is not only effective but also that its correctness can be verified constructively. If this is the case, combining it with the standard soundness proof for Heyting arithmetic would yield a constructive soundness proof for the cyclic proof system of Heyting arithmetic. Much of the procedure deals with combinatorial aspects of cyclic proofs, rather than Heyting arithmetic specifically, and should thus be transferable to other theories to obtain analogous results.
One of the foundational results of (classical) finite model theory, due to Ronald Fagin, shows that every formula of a finite relational language is either almost surely true or almost surely false over finite structures. This has been called a 0-1 law. This talk intends to contribute to the finite model theory of many-valued logics by generalizing this 0-1 law to first-order finite models valued over finite MTL-chains. We will prove that for any first-order (or infinitary with finitely many variables) formula Phi, there is a truth-value that Phi takes almost surely in every finite many-valued model and such that every other truth-value is almost surely not taken. This result also generalizes a theorem for Lukasiewicz logic due to Robert Kosik and Christian G. Fermüller. (This talk is based on joint work with Guillermo Badia.)
Stone’s representation theorem for Boolean algebras gives a bridge between algebra and topology in the form of a categorical duality. In his PhD thesis, de Vries generalized this duality to a duality between compact Hausdorff spaces and what are nowadays called de Vries algebras, which are structures that encode the set of regular open sets of a given compact Hausdorff space. One drawback of the category of de Vries algebras is that the composition of morphisms is not function composition. We propose to work with relations (rather than functions) as morphisms between de Vries algebras: this has the advantage that the composition of morphisms is usual relation composition. Moreover, this approach allows for an extension of de Vries duality to a duality for the category of compact Hausdorff spaces and closed relations between them.
We consider generalisations of Kripke's semantics for Intuitionistic logic adequate for a range of constructive, contractionless logics. These same are obtained partly thru algebraic insights gleaned from Jipsen-Montagna's work on poset products, as well as more recent work by others, including e.g. Castiglioni and Zuluaga. We compare these approaches to other so-called "relational" approaches from the literature, and consider some problems left open in this line of research.
We introduce a cut-free sequent calculus for the alternation-free fragment of the modal mu-calculus. This system allows both for infinite and for finite, circular proofs and uses a simple focus mechanism to control the unravelling of fixpoints along infinite branches. We show that the proof system is sound and complete for the set of valid guarded formulas of the alternation-free mu-calculus. As an application we use the system to show that the alternation-free mu-calculus is closed under Craig interpolation.
(joint work with Yde Venema)
In this talk, I discuss Kleene algebra as a framework for program verification, and in particular focus on a concurrent extension of NetKAT (CNetKAT). NetKAT is an algebraic theory used to describe network behaviour, and CNetKAT extends that with operators for specifying and reasoning about concurrency in scenarios where multiple packets interact through state. More generally, CNetKAT can be understood as an algebraic framework for reasoning about programs with both local state (in packets) and global state (in a global store). The talk will cover some of the syntax and semantics of CNetKAT through an example, and present a soundness and completeness result. The remaining time will be spent on highlighting some of the issues that were encountered creating CNetKAT, and in particular the general issues surrounding extensions of KA with concurrency.
In this talk, I will try to present several results concerning the monadic second-order (MSO) theory of (labelled) countable linear orders. This theory is known to be decidable since the results of Rabin (69) and Shelah (75). After setting up the more recent algebraic framework of countable monoids, I will give a high level intuition on how it can be used to answer several questions:
Propositional provability logics capture in a sense the always provable or always true principles that concern the formalised provability predicate. Since Solovay we know that all sound theories of some minimal strength have the same logic: the PSPACE complete logic GL (Gödel-Löb). The hope arose that something similar could be obtained for predicate provability logics. Through beautiful results by Montagna, Artemov, Vardanyan and McGee, among others, it turned out that the situation is as ghastly as it could possibly be and the resulting logics are highly undecidable or even non-arithmetical. Furthermore, various results by Vardanyan, Berarducci and Visser-de Jonge have shown that, in a sense, this wild behaviour is pretty stable as the influential paper “No escape from Vardanyan’s Theorem” indeed suggests.
Recently we wrote a paper “An escape from Vardanyan’s Theorem” where we carve out a decidable fragment of quantified provability logic that is sound and complete in a certain sense. The key move is switching to so-called strictly positive fragments. In these fragments, we consider statements of the form “A entails B” where A and B allow only for predicate symbols, the logical constant true, conjunctions, universal quantifications and consistency statements. It was a known phenomenon that strictly positive fragments typically lower the complexity of the logic, mostly from PSPACE to PTIME. In our case we fall from Π2 complete all the way back to decidable. We will expose the results and comment on some proof techniques. Near the end of the talk we will comment on work in progress where instead of one consistency statement we wish to allow for an arbitrary sequence of consistency statements of increasing strength.
This is joint work with Ana de Almeida Borges: https://arxiv.org/abs/2102.13091
Composing monads via distributive laws is tricky business, as too often small mistakes are overlooked. After failing to find a distributive law for the list monad over itself, I started proving that finding such a distributive law is impossible. At the same time, Dan Marsden was studying the famous counterexample by Gordon Plotkin that probability does not distribute over non-determinism. Together we developed an algebraic method to find and generalise such counterexamples, resulting in our no-go theorems. In this talk I will explain the main ideas behind our method, illustrated by a proof that 'plus does not distribute over times'. Then, I will highlight some crucial steps in our method, which tell us which type of monads are "high risk" in failing to compose with other monads. Lastly (time permitting), I will say a few words about my current research on combining monads with guarded recursion.
It is well-known that for any regular language there exists a unique minimal DFA accepting it. Establishing a similar result for NFA is more difficult, but of great practical importance, as NFA can be exponentially more succinct than DFA. The main issue is that a regular language can be accepted by several size-minimal NFA that are not isomorphic. A number of sub-classes of NFA have been identified in the literature to tackle this issue, which all admit canonical representatives. In this paper we provide a general categorical framework based on distributive laws that unifies constructions of canonical NFA and unveils new ones.
I present a generic partition refinement algorithm that quotients coalgebraic systems by behavioural equivalence, an important task in system analysis and verification. Coalgebraic generality allows to cover not only classical relational systems but also, e.g. various forms of weighted systems and furthermore to flexibly combine existing system types. Under assumptions on the type functor that allow representing its coalgebras in terms of nodes and edges, the algorithm runs in time O(m log n) for input coalgebras with n states and m edges. The generic complexity result and the possibility of combining system types yields a toolbox for efficient partition refinement algorithms. Instances of our generic algorithm match the run-time of the best known algorithms for unlabelled transition systems, Markov chains, deterministic automata, Segala systems, and for color refinement. For weighted tree automata, the instance of the generic algorithm even improves the best run-time known. The algorithm is implemented in a tool (CoPaR) in full generality and allows the composition of existing systems types at run-time.
We consider Horn formula equations, which are special existential second-order formulas. Our main result states that Horn formula equations are valid iff there are solutions expressible in least fixed-point logic. These canonical solutions correspond to the least and greatest solution in the Horn and dual-Horn case, respectively. As applications and corollaries of the fixed-point theorem we obtain new results and simpler proofs of existing results in second-order quantifier elimination, program verification and proof theory.
This is joint work with Stefan Hetzl, see also https://arxiv.org/abs/2109.04633.
Recently, Baltag & van Benthem introduced a logic of functional dependence LFD with atomic dependence statements and dependence quantifiers that is interpreted over generalised assignment models. Indeed, the logic is closely related to the logic of Cylindrical Relativized Set Algebras (CRS); CRS quantifiers and dependence quantifiers are interdefinable. It follows that LFD can be seen as an extension of CRS with dependence atoms. Decidability was shown by Baltag & van Benthem by a detour via quasi-models. However, this essentially involved an infinite construction, leaving the finite model property (fmp) as an open problem. We solve this by showing that LFD has the fmp, using Herwig's theorem on extending partial isomorphisms. Furthermore, we introduce dependence bisimulations and prove a van Benthem-characterization theorem, characterizing LFD as the largest fragment FOL invariant under this notion.
(These results are the culmination of a project I did under the supervision of Alexandru Baltag.)
https://link.springer.com/article/10.1007/s10992-020-09588-z
https://arxiv.org/abs/2109.08313
I will first explain STV counting and the parlous state of computer-counting code implemented by various Election Commissions from around Australia. I will then explain how we used Coq to specify a "vanilla" version of STV as a proof-calculus and used it to extract a computer program which not only counts votes according to this specification but also produces a certificate during the count. The specification of the certificate is derived from the counting rules. We have proved, in Coq, that if the certificate is correct with respect to its specification, then the result it encapsulates must be correct with respect to the relevant specification of STV. The certificate is designed so that an average third-year computer science student could write a computer program to check the correctness of the certificate. In particular, each political party could hire their own programmer to easily scrutiny the count produced by any computer program, including our own, that produces such certificates. The only caveat is that we require the publication of all ballots.
In this talk, we propose a general method to "decode" (propositional) intuitionistic logic and various intermediate logics as (dynamic) epistemic logics of knowing how. Our approach is inspired by some scattered ideas hidden in the vast literature of math, philosophy, CS, and linguistics about intuitionistic logic in the past 100 years, which echoed Heyting's initial (but forgotten?) conception about intuitionistic truth as "knowing how to prove". The core technical idea is to use a bundled know-how modality to unify the formalized Brouwer–Heyting–Kolmogorov interpretation and the Kripke semantics of intuitionistic logic. As we will see, this approach can reveal the hidden complicated dynamic-epistemic information behind the innocent-looking connectives but makes intuitionistic logic intuitive. With the natural but precise epistemic readings of intuitionistic formulas, various technical results about intuitionistic logic and intermediate logics become transparent, if not trivial. If time permits, we show how to decode inquisitive logic and some version of dependence logic as epistemic logics in order to demonstrate the power of this general approach, which could also be a meeting point of various research themes at ILLC.
(The talk is partly based on the joint work with Haoyu Wang and Yunsong Wang)
I will present recent results establishing decidability and complexity upper bounds for many axiomatic extensions of FLec and FLew. The substructural logics FLec and FLew are obtained from the sequent calculus for intuitionistic propositional logic (FLecw) by omitting the weakening rule and contraction rule respectively. This work can be seen as extending Kripke's decidability argument (1959) and Urquhart's upper bound (1999) for FLec. A notable consequence is a first upper bound for the basic fuzzy logic MTL.
Joint work with A. R. Balasubramanian and Timo Lang. See https://arxiv.org/abs/2104.09716 for details.
While modal logics are robustly decidable, first order modal logics (FOML) are notoriously undecidable, in the sense that modal extensions of decidable fragments of first order logic are undecidable. For example, the two-variable fragment of FOML is undecidable.
Despite such discouragement, this century has seen several positive results on new fragments, such as the monodic fragment, bundled fragment, term-modal logic etc. We give an overview of this exciting area of research, including our own results.
The results presented are joint with Anantha Padmanabha.
Various problems arising in the context of example-driven approaches to conjunctive query discovery turns out to be intimately related to basic structural properties of the homomorphism lattice of finite structures, such as density, or the existence of duals. I will discuss some of these connections, and highlight relevant results from recent work together with Victor Dalmau. See also https://arxiv.org/abs/2008.06824.
Cyclic and non-well-founded proofs have turned out to be very useful tools in the proof theory of modal fixpoint logics. However, most of the known results in this area only treat a particular modal fixpoint logic at once. This is in contrast to basic modal logic, where much more general proof-theoretic methods exist. In this talk I will outline a first attempt to combine these existing general methods with non-well-founded proof theory in order to uniformly treat multiple modal fixpoint logics.
More precisely, I will build on a technique presented by Ori Lahav (LICS 2013) for constructing cut-free hypersequent calculi for basic modal logics characterised by frames satisfying so-called 'simple' first-order conditions. I investigate the generalisation of this technique to a relatively inexpressive modal fixpoint language, namely unimodal logic with the master modality (a.k.a. the reflexive-transitive closure modality). Soundness is obtained for all simple frame conditions, completeness only for those that will be called 'equable'.
Talks from 2020 and earlier can also be found on the Algebra|Coalgebra seminar website.
The seminar is currently organized by Bahareh Afshari, Benno van den Berg, Nick Bezhanishvili, Tobias Kappé and Yde Venema. If you're interested in giving a talk at the seminar or have any questions regarding the seminar please contact Tobias at t.w.j.kappe@uva.nl.
If you want to subscribe to or unsubscribe from the LLAMA seminar mailing list, you can do so here. Please heed the warning about not re-using a valuable password.
The LLAMA seminar, under the Institute for Logic, Language and Computing (ILLC), located at Science Park 107, 1098 XG Amsterdam, is responsible for the processing of personal data as shown in this privacy statement.
The LLAMA seminar does not process personal data via this website (https://events.illc.uva.nl/llama), because it is not possible to leave personal data behind. We also do not use social media plugins.
The LLAMA seminar does not take decisions based on automated processing related to this website on matters that can have (significant) consequences for individuals, e.g., decisions taken by computer programs or systems, without involving a person (for example an organiser of the LLAMA seminar).
The LLAMA seminar does not use cookies or similar techniques on this website.