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.

Note: The seminar will resume in September 2020.

---

Recent talks

• 27.05.2020
  Vít Punčochář (FLU CAS and ICS CAS): Inquisitive Heyting algebras
  In my talk I will explore a class of inquisitive Heyting algebras as algebraic structures that are isomorphic to algebras of finite antichains of bounded implicative meet semilattices. I will show that these structures are suitable for algebraic semantics of inquisitive superintuitionistic logics, i.e. logics of questions based on intuitionistic logic and its extensions. I will explain how questions are represented in these structures (prime elements represent declarative propositions, non-prime elements represent questions, join is a question-forming operation) and provide several alternative characterizations of these algebras. For instance, it will be shown that a Heyting algebra is inquisitive if and only if its prime filters and filters generated by sets of prime elements coincide and prime elements are closed under relative pseudocomplement. We prove that the weakest inquisitive superintuitionistic logic is sound with respect to a Heyting algebra iff the algebra is what we call a homomorphic p-image of some inquisitive Heyting algebra. It is also shown that a logic is inquisitive iff its Lindenbaum-Tarski algebra is an inquisitive Heyting algebra.


• 13.05.2020
  Petr Cintula (ICS CAS): How much Propositional Logic Suffices for Rosser’s Essential Undecidability Theorem?
  Abstract: In this talk we explore the following question: how weak can a logic be for Rosser's essential undecidability result to be provable for a weak arithmetical theory? It it well known for intuitionistic logic and Robinson's Q, and Petr H\'{a}jek proved it in fuzzy logic BL for Grzegorczyk's variant of Q which interprets the arithmetic operations as non-total non-functional relations. We present a proof of essential undecidability in a much weaker substructural logic and for much weaker arithmetic theory, a version of Robinson's R (with arithmetic operations also interpreted as mere relations). Our result is based on structural version of the undecidability argument introduced by Kleene and we show that it goes well beyond the scope of the Boolean, intuitionistic, or fuzzy logic.


• 29.04.2020
  Igor Sedlár (ICS CAS): Finitely-valued Propositional Dynamic Logic (online)
  Absstract: We study a many-valued generalization of Propositional Dynamic Logic where both formulas in states and accessibility relations between states of a Kripke model are evaluated in a finite residuated lattice. One natural interpretation of this framework is related to reasoning about costs of performing structured actions. We prove that PDL over any finite residuated lattice is decidable. We also establish a general completeness proof for a class of PDLs based on commutative integral residuated lattices.


• 26.02.2020
  Sajad Nazari (Laboratoire d'Informatique Fondamentale d'Orléans): Rough Concepts
  Abstract: In this talk, we discuss a logical and algebraic framework unifying Rough Set Theory and Formal Concept Analysis, two influential theories in information science. We also discuss some applications and extensions of this framework to the analysis of vagueness and uncertainty in categorization.


• 12.02.2020
  Michał Stronkowski (Warsaw University of Technology): Admissibility in the multi-conclusion setting
  Abstract: Let $\vdash$ be a (finitary, structural) consequence relation. An inference rule $\Gamma/\varphi$ is admissible for $\vdash$ if adding $\Gamma/\varphi$ to $\vdash$ does not change the set of theorems. The notion of admissibility in the single-conclusion setting is already well understood and its characterizations are known. The situation changes in the multi-conclusion setting. There inference rules with a finite set of formulas in the conclusion are allowed. It appears that then the notion of admissibility splits into a number of nonequivalent ones. I will discuss them and provide their algebraic characterizations. (This work is parallel to Iemhoff's proof-theoretic investigation on admissibility.)


• 22. 01. 2020
  Guillermo Badia (University of Queensland): Ehrenfeucht-Fraisse methods in the model theory of L-topological spaces over finite MTL-chains
  Abstract:Lattice-valued topological spaces were introduced by Goguen in the 1970s, as a generalization of Chang's fuzzy topological spaces. The intuitive idea is simply to study topologies where the open sets are "fuzzy" or lattice-valued, instead of crisp. Second-order languages to study topological spaces have been studied for classical logic in the past, so in this talk I'll introduce a second-order language over lattice-valued structures to study lattice-valued topological spaces. I will present some of the model-theoretic properties of said language, focusing on characterizations of expressivity via an Ehrenfeucht-Fraisse theorem. Some technical restrictions are necessary to get a well-behaved general model theory here: the lattice must be finite. In this talk, I consider only MTL algebras, but it is possible that this further restriction can be relaxed.


• 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.


• 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).

Archive

The seminar archive can be found here.