About

The Seminar on Applied Mathematical Logic (a.k.a. the Hájek Seminar) usually takes place on Wednesdays 4pm in the lecture room 318 of the Institute of Computer Science (Pod Vodárenskou věží 2, Prague 8. See the map). The seminar hosts talks on recent work in mathematical logic and applications by members of the Prague logic community and guests.

For more information on ICS seminars, take a look at the seminar section of the ICS webpages.

Upcoming talks

• 11. 12. 2019
  Amanda Vidal (ICS CAS): Axiomatic systems of Gödel Modal Logics
  Abstract: In this seminar we will go over the main results from the literature concerning Gödel modal logics, understood as the logics arising from prominent distinguished classes of Kripke models valued over the standard Gödel algebra. Known results cover axiomatizing the box and the diamond fragments of the logic both over the most general class of valued models (MG), and over the ones where the underlying frame is classical, and the logic with both modal operators over the class MG. We will then approach the problem of axiomatizing the bi-modal logic over the class of models with underlying classical frames, and propose an axiomatization relying in Dunn's axiom of positive modal logic. We will see some consequences that arise from the technical details of the completeness proof, and if time allows, the relation of these logics with some modal Intuitionistic logics from the literature.


• 04. 12. 2019
  Martin Blicha (Charles University), Craig interpolation in software verification
  Abstract: Craig interpolation is a logical concept popularized in formal verification community by McMillan (2003). Since then, several successful verification techniques based on interpolation have been developed and interpolation remains one of the dominant approaches for proving safety. We will outline the use of interpolants for computing invariants of program loops, show how interpolants are computed in modern SMT solvers from proof of unsatisfiability, and finally present our recent result regarding computation of interpolants for systems of linear inequalities over rational numbers.

Recent talks

• 20. 11. 2019
  Andrew Tedder (ICS CAS): Information Flow in Logics in the Vicinity of BB
  Abstract: B is the basic logic of the Routley-Meyer semantic framework, and BB that of the `neighbourhood style' RM semantics. The RM semantics invites a number of motivational stories, the one of interest here being that of situation semantics along with a channel-theoretic reading of the central ternary relation - according to this reading, a situation supports some conditional information when it facilitates information flow between situations supporting the antecedent of the conditional and situations supporting the consequent. With this story it is easy to make sense of the use of the ternary relation in the truth conditions of conditional formulas in terms of the application of a channel to some input, yielding some output. Part and parcel with the channel-theoretic reading of the RM semantics, however, are some natural actions performable on channels, and some constraints on those actions. The key action of interest here is the serial composition of channels. Elsewhere I have motivated a particular method for cooking up composites out of pairs of channels, and have shown that a simple fragment of B is complete w.r.t. the class of models in which such points exist (so the logic supports a robust channel-theoretic reading). In this talk, I refine that argument a bit by working in the neighbourhood style RM semantics, and discuss some extensions of my previous results, and some (more or less severe) limitations on the use of the method for further logics. I end with some further questions, and some reflections on situation theoretic interpretations of the RM semantics more generally.


• 13. 11. 2019 [Room 419]
  Sabine Frittella (Laboratoire d’Informatique Fondamentale d’Orléans): Probabilistic Dynamic Epistemic Logic
  Abstract: First, I will present a paper on Probabilistic Epistemic Updates on Algebras (joint work with Willem Conradie, Alessandra Palmigiano, Apostolos Tzimoulis and Nachoem Wijnberg, link: https://arxiv.org/abs/1612.05267). This paper contributes to the development of the mathematical theory of epistemic updates using the tools of duality theory. Here we focus on Probabilistic Dynamic Epistemic Logic (PDEL). We dually characterize the product update construction of PDEL-models as a certain construction transforming the complex algebras associated with the given model into the complex algebra associated with the updated model. Thanks to this construction, an interpretation of the language of PDEL can be defined on algebraic models based on Heyting algebras. This justifies our proposal for the axiomatization of the intuitionistic counterpart of PDEL, of which we prove soundness and completeness with respect to algebraic probabilistic epistemic models.
  Then, I will present a starting research project on Dynamic Epistemic Logic applied to privacy. In a nutshell, we aim at characterising the knowledge an attacker can infer on a user/client/citizen given its prior knowledge on the world and the personal data he collects on the user. Since a large part of the relevant knowledge the attacker can infer is based on statistical knowledge on the population, one big challenge is to describe statistical knowledge and reasoning based on that type of knowledge.


• 06. 11. 2019
  Neil Thapen (Math. CAS): Random resolution and approximate counting
  Abstract: Resolution is a propositional proof system that is bad at formalizing arguments involving counting, even approximately. I will discuss some upper and lower bounds on random resolution, a system which, roughly speaking, adds to resolution the ability to use any axiom, as long as it is true most of the time. This is connected to a result about a related first-order proof system of bounded arithmetic with approximate counting.


• 30. 10. 2019
  Tommaso Moraschini (ICS CAS): Profinite Heyting algebras and the representation problem for Esakia spaces
  Abstract: A poset is said to be "representable" if it can be endowed with an Esakia topology. Gratzer's classical representation problem asks for a description of representable posets which - unfortunately - is not expected to take a simple form, as these do not form an elementary class. As at the moment a solution to the representation problem seems out of reach, we address a simpler version of the problem which, roughly speaking, asks to determine the posets that may occur as top parts of Esakia spaces. Crossing the mirror between algebra and topology, this task amounts to characterize the profinite Heyting algebras that are also profinite completions. We shall report on the on-going effort to solve this problem by understanding the structure of varieties of Heyting algebras whose profinite members are profinite completions. This talk is based on joint work with G. Bezhanishvili, N. Bezhanishvili, and M. Stronkowski.


• 23. 10. 2019
  Michał M. Stronkowski (Warsaw Uni. of Technology): Profiniteness and finitely generated varieties
  Abstract: Profinite algebras are exactly those that are isomorphic to inverse limits of finite algebras. Such algebras are naturally equipped with Boolean topologies. A variety V of algebras is standard if every Boolean topological algebra with the algebraic reduct in V is profinite. We show that there is no algorithm that takes as input a finite algebra A (of a finite type) and decides whether the variety generated by A is standard. We also show the undecidability of some related properties. In particular, we solve the problem posed by Clark, Davey, Freese, and Jackson about finitely determined syntactic congruences in finitely generated varieties. Our work is based on Moore's theorem about undecidability of having definable principal subcongruences for finitely generated varieties. Joint work with Anvar M. Nurakunov.


• 9. 10. 2019
  Tadeusz Litak (Friedrich-Alexander Uni. Erlangen-Nürnberg): Loeb constructively meets μ
  Abstract: A famous result of Solovay identifies the classical modal Loeb system (KL) as the provability logic of Peano Arithmetic. Under this perspective, Goedel’s Second Incompleteness Theorem and Loeb’s Theorem leave an algebraic trace in the form of explicit definability of fixpoints of modalized formulas in KL. Van Benthem has observed that this definability of fixpoints entails that adding standard fixpoint operators of positive formulas does not increase the expressive power of KL. Visser has analyzed this observation syntactically and extended it to a proof that KL is a retract of the modal μ-calculus in a suitably defined category of interpretations. A fully polished theory of such embeddings and translations involving the fixpoint operator and similar binders is yet to be developed (it would have to marry AAL with HOAS and/or HRS).
  Furthermore, we face some interesting problems when studying intuitionistic analogs of such results. First, while the fixpoint theorem for modalized formulas works in intuitionistic KL (iKL), the propositional reasoning underlying derivations of van Benthem and Visser is essentially classical. Deep results about the intuitionistic propositional calculus (IPC) established by Pitts or Ruitenburg can be used to overcome this limitation.
  Second, over IPC (and sometimes even classically) it is for several reasons natural to look at a more general syntactic setup replacing the box with Lewis arrow, which arithmetically is standardly interpreted in terms of preservativity (although it does admit many other interpretations). As it turns out, there are two major incompatible ways of computing explicit fixpoints for formulas whose principal connective is the strict implication, each requiring a different base logic. Our approach here can be described as the first study of reverse mathematics of explicit fixpoints. This is obviously a joint work with Albert Visser (Utrecht).


• 12.6.2019
  Sebastian Sequoiah-Grayson (Uni. Sydney): Modelling epistemic actions: From aggregations to combinations
  Abstract: Examples of epistemic actions are given most commonly as observations and announcements. In such frameworks, logical omniscience, or something close to inferential optimisation, is assumed often. In this talk I want to do several things. Firstly, I want to propose and defend a view of inferences themselves as epistemic actions of a psychological, information-handling sort. I shall introduce two varieties of such actions, aggregations and combinations. Secondly, I want to explain why it is that I think that nearly everything said about logical omniscience and epistemic closure is wrong. Then finally I shall introduce a new type of substructural epistemic logic that I think I think is a promising start to saying something important and non-trivial about the properties and nature of the inferential epistemic actions in question.


• 5.6.2019
  Joan Gispert (Uni. Barcelona): Structural completeness and quasivariety lattices in many-valued logics
  Abstract: Admissible rules of a logic are those rules under which the set of theorems are closed. A logic is said to be structurally complete when every admissible rule is a derivable rule. A logic is almost structurally complete when every rule is either derivable or passive (there is no substitution that turns all premisses into theorems). Gödel logic and Product logic are structurally complete and moreover every axiomatic extension is structurally complete; finite-valued Łukasiewicz logics turn to be almost structurally complete and the infinite valued Łukasiewicz logic is not structurally complete, nor almost structurally complete. In this talk we will algebraically investigate structural completeness, almost structural completeness for some cases of algebraizable many-valued logics, and we try, if possible, to describe the quasivariety lattice of its associated algebraic class.


• 29.5.2019
  Adam Přenosil (Vanderbilt Uni.): Algebras of fractions: bimonoids and bimodules
  Abstract: A classical result due essentially to Steinitz (1910) states that each cancellative commutative monoid can be embedded into an Abelian group. This was later improved by Ore (1931): each so-called right reversible cancellative monoid can be embedded into a group of right fractions, i.e. a group where each element has the form a · b−1 for some a; b in the original monoid. In this talk we show how to define and construct algebras of fractions for other classes of algebras, such as Heyting algebras. These algebras of fractions will be involutive residuated lattices into which a given residuated lattice has a suitable embedding. We sketch two approaches to this problem: one based on bimonoids (one-sorted structures with two compatible monoidal operations) and one based on bimodules (in this context, two-sorted structures consisting of a monoid acting on another monoid). The talk is based on joint work with Nick Galatos and Costas Tsinakis.


• 15.5.2019
  Radek Honzík (FF CUNI): A small ultrafilter number on uncountable regular cardinals
  Abstract: We will review the notion of compactness for infinitary logics, discuss the basic properties of compactness (limitations of Zorn’s lemma, construction of models using compactness). We will mention some original results related to the existence of a normal measure on uncountable kappa with small base and its compatibility with more compactness principles.


• 24.4.2019
  Tommaso Moraschini (ICS CAS): The poset of all logics
  Abstract: A notion of interpretability between arbitrary propositional logics is introduced, and shown to be a preorder on the class of all logics. Accordingly, we refer to its associated poset as to the "poset of all logics". In this talk we shall explore the structure of this poset. In particular, we observe that that it has infima of arbitrarily large sets, but even finite suprema may fail to exist. This should not come as a surprise, since the universe of the poset of all logics is indeed a proper class. The formalism of interpretability is subsequently exploited to introduce the notion of a Leibniz class of logics, and we refer to the complete lattice of Leibniz class as to the Leibniz hierarchy. This order-theoretic perspective allows us to address in mathematical terms the following foundational question: do the classes traditionally associated to the Leibniz hierarchy (e.g. that of protoalgebraic logics) capture "fundamental" concepts?


• 10.4.2019
  Zuzana Haniková (ICS CAS): Computing the validity degree in Łukasiewicz logic
  Abstract: This talk will consider provability/validity degrees in propositional Łukasiewicz logic in the context of other optimization problems. In order to define provability degrees of propositional formulas, rational constants are employed, so one in fact works in a conservative extension called Rational Pavelka logic (RPL). On the other hand, no constants are necessary to introduce the validity degree; for a formula F, its validity degree under a theory T is the infimum of values of F under assignments that make T true in the standard MV-algebra on [0,1]. Pavelka completeness states that in RPL the provability degree coincides with the validity degree. For T and F to be even considered as a computational problem, T needs to be finite, whereupon the provability/validity degree becomes rational; one can moreover show that the size of the denominator of this rational is polynomial in the sizes of T and F. I will discuss how the optimization problem relates to finite consequence in RPL taken as a decision problem (shown to be coNP-complete by Hájek), which can be viewed as an upper bound. Further, I will try to provide a lower bound using the taxonomy of optimization problems provided by [M. Krentel, The complexity of optimization problems].


• 27.3.2019
  Igor Sedlár (ICS CAS): Two approaches to non-classical modal logic
  Abstract: Two prominent approaches to non-classical modal logic are the lattice-valued one, using Kripke frames and valuation functions mapping formula-state pairs to a lattice of truthvalues, and the relational one, extending frame semantics for non-classical logics--usually given by means of so-called Routley-Meyer frames--by additional accessibility relations corresponding to modal operators. In this talk, I outline some preliminary results on the relationship between these two approaches. Using elementary dualities between residuated lattices and Routley-Meyer frames, I show that the logic of all modal associative Routley-Meyer frames is the logic of all Kripke frames with valuations in complete distributive FL-algebras.


• 20.3.2019
  Joan Betran-San Millán (FLU CAS): Frege's Begriffsschrift and second-order logic
  Abstract: Gottlob Frege developed in Begriffsschrift (1879) the concept-script, the fi rst formal system in the history of modern logic. The similarities between Frege's system and some contemporary formal systems have been taken for granted as evidence for a contemporary interpretation of the concept-script. In fact, the most common and traditional interpretation of Begriffsschrift's concept-script claims that it consists of a formal language of second-order logic and a deductive system for that language. In this talk, I offer a detailed analysis of Begriffsschrift's deductive system and justify that it must not be interpreted as a formal system of second-order logic. Specifically, I defend that a reformulation of the calculus of the concept-script in terms of a second-order calculus distorts its nature and, moreover, that some proofs of Begriffsschrift are not reproducible by means of this reformulation.


• 13.3.2019
  Pavel Hrubeš (MI CAS): Compression schemes and the Continuum Hypothesis
  Abstract: The Continuum Hypothesis is a conjecture about the cardinality of the set of real numbers. As such, it is a classical problem known to be undecidable from the usual ZFC axioms. We will show that some problems arising in the context of machine learning are equivalent to variants of CH - and hence undecidable over ZFC. We will focus on the problem of compressing finite strings of real numbers. (Based on joint work with S. Ben-David, S.Moran, A. Shpilka, A. Yehudayoff)


• 27.2.2019
  Ansten Klev (FLU CAS): Identity and definition in natural deduction
  Abstract: Recall that in natural deduction each primitive constant is equipped with introduction and elimination rules. Such rules can be given not only for the logical connectives and the quantifiers, but also for the identity predicate: its introduction rule is the reflexivity axiom, t = t, and its elimination rule is the indiscernibility of identicals. Although a normalization theorem can be proved for the resulting system, one might not be entirely satisfied with this treatment of identity, especially if one adheres to the idea - going back to Gentzen - that the meaning of a primitive constant is determined by its introduction rule(s). Firstly, it is not obvious that the introduction rule for the identity predicate is strong enough to justify its elimination rule. Secondly, it is not clear what to say about definitions taking the form of equations. Such definitions are usually regarded as axioms, hence they must be additional introduction rules for the identity predicate. Since definitions are particular to theories, it follows that the meaning of the identity predicate changes from one theory to the other. I will show that by enriching natural deduction with a theory of definitional identity we can answer both of these worries: we can justify the elimination rule on the basis of the introduction rule, and we can extend any theory with definitions while keeping the reflexivity axiom as the only introduction rule for the identity predicate.


• 20.2.2019
  Luca Reggio (ICS CAS): Uniform interpolation for IPC via an open mapping theorem for Esakia spaces
  Abstract: The uniform interpolation property of the intuitionistic propositional calculus (IPC) wasfirst proved by Pitts in 1992 by means of proof-theoretic methods. We prove an open mapping theorem for the topological spaces dual to finitely resented Heyting algebras. In turn, this yields a short, self-contained semantic proof of Pitts result. Our proof is based on the methods of Ghilardi & Zawadowski. However, it does not require sheaves nor games, only basic duality theory for Heyting algebras. This is joint work with Sam van Gool.


• 6.2.2019
  Marco Abbadini (Universita degli Studi di Milano): The dual of compact ordered spaces is a variety
  Abstract: Last year (2018), Hofmann, Neves and Nora proved that the dual of the category of partially ordered compact spaces and monotone continuous maps is an infinitary quasi-variety. One of the open questions was: is it also a variety? We show that the answer is: yes, it is an infinitary variety.

Archive

The seminar archive can be found here.