Seminar on Applied Mathematical Logic

Welcome to the archive of the Seminar on Applied Mathematical Logic.

• 14.12.2022
  
  Zuzana Haniková (Czech Academy of Sciences, Institute of Computer Science): Vopěnka's Alternative Set Theory and its mathematical context

  This talk will be an exposition of Vopěnka's Altenative Set Theory (AST), as first presented in his monograph "Mathematics in the Alternative Set Theory" published by Teubner Verlag in 1979, in relation to some pertinent mathematical developments of the 20th century; namely, Skolem's work in nonstandard models of arithmetic, Vopěnka's nonstandard models of set theory, Robinson's nonstandard analysis, Vopěnka and Hájek's work in the theory of semisets, or Parikh's almost consistent theories. My aim will be to lay out the design choices Vopěnka made for the AST, and to discuss possible inspiration for them. In addition to the Teubner book, I will rely on ``Introduction to Mathematics in the Alternative Set Theory'', published in 1989 in Slovak. This talk is based on my paper "Vopěnkova Alternativní teorie množin v matematickém kánonu 20. století", recently published in Filosofický časopis; English translation available as arXiv:2211.11020.



• 07.12.2022
  
  Chun-Yu Lin (Czech Academy of Sciences, Institute of Computer Science): On Many-Valued Coalgebraic Modal Logic

  A well-known result in coalgebraic modal logic is that its completeness can be determined at the one-step level. We generalize the result to the finitely many-valued case by using the canonical model construction method. We prove the result for coalgebraic modal logics based on three different many-valued algebraic structures, including the finitely-valued {\L}ukasiewicz algebra, the commutative integral Full-Lambek algebra (FL$_{ew}$-algebra) expanded with canonical constants and Baaz Delta, and the FL$_{ew}$-algebra expanded with valuation operations. On the other hands, we also generalize Pattinson's stratification method for colagebraic modal logic to the many-valued setting. In contrast to standard techniques of canonical model construction, this method employs an induction principle to prove the soundness and completeness the logics. This talk is based on joint works with Dr.Churn-Jung Liau in Academia Sinica, Taiwan.



• 30.11.2022
  
  Colin Zwanziger (Czech Academy of Sciences, Institute of Philosophy): S4 Necessity and Comonads

  I will delineate the categorical semantics of S4 necessity operators, in settings ranging from propositional logic up to dependent type theory. In each setting, the semantics of the S4 necessity operator is given by a suitable *comonad*. We will see that S4 modal dependent type theory (Nanevski et al. 2008) has the advantage of subsuming both S4 modal predicate logic and intensional logic, while adding the expressive power of dependent types. The comonadic semantics for this dependent type theory is adapted from Zwanziger (2022).



• 23.11.2022
  
  Thomas M. Ferguson (Czech Academy of Sciences): Beyond Parry: Applications of Intensional Subject-Matter

  A number of philosophers working in logical frameworks that are sensitive to models of topic---like Fine and Berto---have taken note that intensional operators can have a transformative effect on a sentence's overall subject-matter. With its implicit model of topic playing a central role, Parry's logic of analytic implication (PAI) has proven a very fertile setting to explore the topic-theoretic contributions made by intensional operators. Parry's framework thus serves as a satisfactory incubator in which the theory of intensional topics can mature. In this talk, I would like to show how the lessons learned about intensionality and topic within this context can be ported to other settings. In particular, I will review some issues in Berto's theory of topic-sensitive intentional modals (TSIMs) and show how techniques incubated in Parry's context can supply solutions to limitations with several interpretations of TSIMs.



• 09.11.2022
  
  Miguel Martins (University of Barcelona): The Bi-Intuitionistic Logic of Co-Trees

  A bi-Heyting algebra validates the Gödel-Dummett axiom (p \to q) \lor (q \to p) iff the poset of its prime filters is a disjoint union of co-trees (i.e., order duals of trees). Bi-Heyting algebras of this kind are called bi-Gödel algebras and form a variety that algebraizes the extension bi-LC of bi-intuitionistic logic axiomatized by the Gödel-Dummett axiom. In this talk, we will present some of our contributions to the study of the lattice Ext(bi-LC) of extensions of bi-LC. We developed the methods of Jankov-style formulas for bi-Gödel algebras and used them to prove that there are exactly continuum many extensions of bi-LC. We also showed that all these extensions can be uniformly axiomatized by canonical formulas. Our main result is a characterization of the locally tabular extensions of bi-LC. We introduced a sequence of co-trees, called the finite combs, and showed that a logic in Ext(bi-LC) is locally tabular iff it contains at least one of the Jankov formulas associated with the finite combs. It follows that there exists the greatest non-locally tabular extension of bi-LC and consequently, a unique pre-locally tabular extension of bi-LC. These results contrast with the case of the intermediate logic axiomatized by the Gödel-Dummett axiom, which is known to have only countably many extensions, all of which are locally tabular. This is joint work with Nick Bezhanishvili and Tommaso Moraschini.



• 02.11.2022
  
  Daniil Kozhemiachenko (INSA Centre Val de Loire): Crisp bi-Gödel modal logic and its paraconsistent expansion

  We provide a Hilbert-style axiomatisation for the crisp bi-G\"{o}del modal logic $\KbiG$. We prove its completeness w.r.t. crisp Kripke models where formulas at each state are evaluated over bi-G\"{o}del algebra $[0,1]$. We also consider a paraconsistent expansion of $\KbiG$ with a De Morgan negation $\neg$ which we dub $\KGsquare$. We devise a Hilbert-style calculus for it and prove its completeness w.r.t. crisp Kripke models with two valuations over $[0,1]$ as a consequence of a~conservative translation from $\KbiG$ to $\KGsquare$. We also study semantical properties of $\KbiG$ and $\KGsquare$. In particular, we show that Glivenko theorem holds only in finitely branching frames. We also explore the classes of formulas that define the same classes of frames both in $\mathbf{K}$ (the classical modal logic) and $\KG^c$. We show that, among others, all Sahlqvist formulas and all formulas $\phi\rightarrow\chi$ where $\phi$ and $\chi$ are monotone, define the same classes of frames in $\mathbf{K}$ and $\KG^c$. The presentation is based on joint work with Marta Bílková and Sabine Frittella.



• 19.10.2022
  
  Adam Přenosil (Institute of Computer Science, CAS): A module-theoretic approach to multiset consequence relations

  The syntax of abstract algebraic logic (AAL) lives in the powerset of the algebra of formulas, in the sense that logics are defined as structural closure operators on this powerset. While this assumption has served well as the bedrock of AAL, much of the architecture of AAL does not depend on the particular properties of the formula powerset. Blok and Jónsson took the first step in this direction when they replaced the formula powerset in the basic theory of algebraization by the powerset of an M-set (a set with a monoid action). Galatos and Tsinakis then took this abstraction even further, replacing the powerset by a complete lattice. A resource-conscious logician might then wish to take a further step and allow for a different, "multiplicative" way of combining syntactic objects, thus obtaining an abstraction of multiset-based consequence relations. An attempt to stretch the framework of Galatos and Tsinakis in this direction was already made in a 2019 paper by Cintula, Gil-Feréz, Moraschini and Paoli. We provide a different answer to the same problem and explain why we find it preferable to the existing one. (This talk is based on joint work with Constantine Tsinakis.)



• 05.10.2022
  
  Igor Sedlár (Institute of Computer Science, CAS): On the Complexity of *-Continuous Kleene Algebra With Domain

  We prove that the problem of deciding membership in the equational theory of *-continuous Kleene algebra with domain is EXPTIME-complete. Our proof makes essential use of Hollenberg's equational axiomatization of program equations valid in relational test algebra. We also identify a weak version of Kleene algebra with domain, called Kleene algebra with literals, KAL, and we show that the equational theory of this class of algebras is PSPACE-complete.



• 08.06.2022
  
  Michal Botur (Palacký University Olomouc): Perfect pseudo MV-algebra, kite, variety, representation

  We study the structure of perfect residuated lattices, focussing especially on perfect pseudo MV-algebras. We show that perfect pseudo MV-algebras can be represented as a generalised version of Kowalski and Dvurečenskij's kites. We characterise varieties generated by kites and describe the lattice of these varieties as a complete sublattice of the lattice of perfectly generated varieties of perfect pseudo MV-algebras.



• 31.05.2022
  
  Davide Fazio (University of Cagliari): On a logico-algebraic approach to AGM belief contraction theory

  In this talk we investigate an algebraic approach to AGM (Alchourrón, Gärdenfors, Makinson) logic of theory change by using the tools of abstract algebraic logic. Specifically, we generalize the notions involved in the definition of epistemic operators, in particular contraction, to arbitrary finitary propositional logics, and we show how to switch from a syntactic-based approach to a semantic one. This allows to build a solid bridge between the validity of AGM postulates in a propositional logic and specific algebraic properties of its intended algebraic counterpart. Such a connection deserves particular attention when we deal with maxichoice contractions. We close the talk by discussing open problems and further developments of the above framework. Joint work with M. Pra Baldi.



• 18.05.2022
  
  Igor Sedlár (ICS CAS): One-sorted Kleene algebra with tests

  Kleene algebra with tests, KAT, is a simple two-sorted algebraic framework for verifying properties of propositional while programs. One-sorted alternatives to KAT have been explored, mainly in connection with applications in automated program verification. A well known example of this approach is Kleene algebra with domain, KAD. A generalization of KAD called one-sorted Kleene algebra with tests, OneKAT, was recently proposed by the author in collaboration with J. Wannenburg. In this paper we show that KAT can be transformed into a flexible one-sorted framework that retains all natural properties of KAT. This framework, called Kleene algebra with test operators, is based on the idea of extending Kleene algebra with a set of test operators such that the set of images of the multiplicative unit under test operators generates a Boolean algebra of tests.



• 27.04.2022
  
  Rostislav Horčík (Czech Technical University): Homomorphisms of Planning Tasks and Heuristic Search

  Classical planning tasks are modeled in the Planning Domain Description Language (PDDL), a schematic language based on first-order logic. Using a grounding process, most state-of-the-art planners turn this first-order representation into a propositional one. However, grounding may cause an exponential blowup. Therefore, investigating methods for computing plans directly on the first-order level is essential. To build such a first-order planner, one must invent an admissible heuristic navigating the search algorithm like A* without grounding the original planning task. We introduce homomorphisms between PDDL tasks that allow us to transform a PDDL task into a smaller one by reducing the number of its objects. Consequently, one can compute an admissible heuristic for the original task in the smaller one.



• 13.04.2022
  
  Vít Punčochář (FLU CAS): Layers of Propositional Types

  In my talk I will describe a framework that is based on the idea that various logical expressions, e.g. modal adverbs or the conditional ‘if’, generate statements that provide information of different types. This idea is partly inspired by the team semantics for propositional dependence logic but deviates from it in several respects. Most importantly, instead of the two semantic layers used in dependence logic -- possible worlds and teams -- a whole hierarchy of contexts is introduced and different types of formulas are evaluated at different levels of this hierarchy. This leads to a rich stratification of informational types. I will explore the formal aspects of this approach and apply it to a number of puzzling phenomena related to modalities and conditionals.



• 02.03.2022
  
  Martin Suda (CIIRC, Czech Technical University): Integrating Machine Learning into Saturation-based ATPs

  Applying the techniques of machine learning (ML) promises to dramatically improve the performance of modern automatic theorem provers (ATPs) and thus to positively impact their applications. The most successful avenue in this direction explored so far is machine-learned clause selection guidance, where we learn to recognize and prefer for selection clauses that look like those that contributed to a proof in past successful runs. In this talk I present Deepire, an extension of the ATP Vampire where clause selection is guided by a recursive neural network (RvNN) for classifying clauses based solely on their derivation history.



• 23.02.2022
  
  Andrew Tedder (Ruhr University Bochum): Kapsner Complementation

  In this paper I discuss a class of algebras appropriate to model, and, philosophically speaking, also to capture the central commitments of, Kapsner Strongly Connective logics. I introduce this class of logics, and its relation to standard connexive systems, introduce the class of algebras, comparing with some work on algebraic semantics of connexive logics by Storrs McCall, and give some examples. I close with some avenues of future work and open problems.



• 02.02.2022
  
  Nicholas Ferenz (ICS CAS): Conditional FDE-logics

  The logic FDE, especially in its four-valued presentation, and sometimes referred to as the Belnap-Dunn logic due to its origins in the work of both Nuel Belnapand J. Michael Dunn, is typically presented without a conditional connective. Moreover, adding a conditional to FDE is not always straightforward, and sometimes presents interesting problems. An infamous problem shared by many paraconsistent logics is that the standard definitions of the material conditional (via disjunction and negation) result in a conditional for which modus ponens is not valid. While there are several extensions and expansions of FDE with a conditional connective, the present work adds to this list by combining Dunn's two-valued relational approach to FDE with conditionals, where the conditionals are defined (semantically) as in the conditional logics presented by Chellas in his 1975 paper "Basic conditional logic" and in chapter 10 of his 1980 book "Modal Logic". In addition, we present a general frame semantics that, strictly speaking, is only necessary for some of the extensions (quantified or propositional) of the base logics constructed here.



• 19.01.2022
  
  David Cerna (ICS CAS): Learning Higher-Order Logic Programs From Failures

  Learning complex programs through inductive logic programming (ILP) remains a formidable challenge. Existing higher-order enabled ILP systems show improved accuracy and learning performance, though remain hampered by the limitations of the underlying learning mechanism. Experimental results show that our extension of the versatile Learning From Failures paradigm by higher-order definitions significantly improves learning performance without the burdensome human guidance required by existing systems. Furthermore, we provide a theoretical framework capturing the class of higher-order definitions handled by our extension. (Joint work with Stanisław J. Purgał and Cezary Kaliszyk.)



• 10.11.2021
  
  Jamie Wannenburg (ICS CAS): A Generalization of Ultraproducts

  A construction, called ‘prime products’ will be presented that generalizes the ultraproduct construction (which is often used to create non-standard models in universal algebra and model theory). This construction will be tied to ‘positive’ formulas, in a manner that is analogous to how ultraproducts are tied to ‘full’ first order formulas—with negation. In particular, there is an analogue of Łoś’ Theorem, implying that prime products preserve existential positive formula (EPF). Furthermore, one can show that a class K of algebras is axiomatized by ‘coherent sentences’ (universally quantified implications between EPF) iff K is closed under ultraroots and prime products. There is also a limited analogue of the Łoś-Suszko Theorem, which holds for any quasivariety K of finite type with a finite nontrivial member: The nontrivial members of K satisfy the same existential positive sentences iff the nontrivial members of K have isomorphic ‘prime powers’. This condition is known as ‘passive structural completeness’.



• 03.11.2021
  
  Kentaro Yamamoto (ICS CAS): The automorphism groups of ultrahomogeneous lattices

  This is a continuation of the talk the presenter gave last year on the automorphism group Aut(L) of the countable ultrahomogeneous Heyting algebra L universal with respect to all finite Heyting algebras, the smallest model of the model completion of their first-order theory. After reminding ourselves of the relevant definitions, we look at an elementary construction showing that the automorphism group of L is not topologically isomorphic to any of those of better-known ultrahomogeneous lattices. We then go over the notion of independence among finite subsets of L that can be used to establish the simplicity of Aut(L). The notion of independence derives from the superamalgamation property of the age of L. Finally, we will discuss future work regarding the automorphism group of a structure and the superamalgamation property of its age.



• 27.10.2021
  
  Sara Ayhan (Ruhr University Bochum): Reduction procedures and the meaning of proofs

  What are ‘good’ reduction procedures and why is it important to distinguish these from ‘bad’ ones? It has been argued that from a philosophical point of view, or more specifically a standpoint of proof-theoretic semantics, reduction procedures are closely connected to the question about identity of proofs and that accepting certain reductions would lead to a trivialization of identity of proofs in the sense that every derivation of the same conclusion would have to be identified (see Schroeder-Heister, P. & Tranchini, L. (2017). Ekman’s Paradox. Notre Dame Journal of Formal Logic, 58(4), 567-581). Therefore, we need to be careful: We cannot just accept any reduction procedure, i.e. any procedure eliminating some kind of detour in a derivation. I agree with this conclusion, however, I will argue that the question, which reductions we accept in our system, is not only important if we see them as generating a theory of proof identity but is also decisive for the more general question whether a proof has meaningful content. By annotating derivations and reductions with lambda terms in accordance with the Curry-Howard-correspondence, it becomes much clearer what may be wrong with certain reductions. I will give examples of such reductions and show that allowing these would not only trivialize identity of proofs of the same conclusion but that it would allow to reduce a term of one type to the term of an arbitrary other. The lambda calculus and some well-known properties thereof can provide us with directions as to why this happens in these cases but not in the cases of ‘well-behaved’ reductions. If we take reductions as inducing an identity relation then that would force us to dentify proofs of different arbitrary formulas. But even if we reject this assumption about proof identity, I will argue that allowing such reductions would render derivations in such a system meaningless.



• 20.10.2021
  
  David Fernández Duque (ICS CAS and Ghent University): Decidability of some intuitionistic and Gödel modal logics with transitivity

  There are various modal logics in the literature based on intuitionistic or Gödel logic, with the general pattern that very weak logics such as K, or very strong logics such as S5, are known to be decidable, but the decidability of "intermediate" logics such as S4 is or was unknown. We discuss relatively recent techniques that can be used to prove the decidability of many of these logics via finite 'bi-relational' models, and state several results obtained in this way. (Joint work with Philippe Balbiani and Martín Diéguez)



• 26.07.2021
  
  David Fernández Duque (Ghent University): On the adequacy of temporal logics for modelling European transport regulations

  We analyze the expressibility of some articles of the European transport regulations in subsystems of monadic second order logic (MSO), with particular emphasis on linear temporal logic (LTL). We argue that all articles under consideration can be represented in the \Sigma_1 fragment of MSO, although representations in LTL can sometimes be unfeasible if not impossible.



• 23.06.2021
  
  J. J. Wannenburg (Czech Academy of Sciences): Epimorphisms in varieties of semilinear residuated lattices

  We provide sufficient conditions for a variety of residuated lattices to have surjective epimorphisms. The lattices under consideration are square-increasing [involutive] commutative residuated lattices (S[I]RLs) that are semilinear, i.e., that embed into a direct product of totally ordered algebras. We say that an S[I]RL is negatively generated when it is generated by the elements beneath its identity. We shall present a representation of negatively generated semilinear S[I]RLs, and use this representation to show that the class of all such algebras is a locally finite variety. Moreover, we show that in all varieties of negatively generated semilinear S[I]RLs epimorphisms are surjective. On the way to the aformentioned result we show that epimorphisms are surjective in the variety of idempotent semilinear S[I]RLs, from which it follows that this variety has the strong amalgamation property. These results settle natural questions about Beth-style definability of a range of relevance logics.



• 16.06.2021
  
  Norihiro Yamada (University of Minnesota): Dependent types and finite limits in games

  Game semantics is a particular class of mathematical (or denotational) semantics of logic and computation, which interprets types (or formulas) by (debate) games between a prover and a disprover, and terms (or proofs) by strategies for the prover to win the games. By its distinctive intensionality, it has been a highly powerful tool for the study of logic and computation, and recently extended to a mathematical foundation of the dynamic aspects of logic and computation such as normalisation (or cut-elimination), algorithms and higher-order computability. One of the most challenging problems in game semantics is to interpret dependent types (or predicate logic). In fact, there has been no established solution for this problem for more than 25 years. Another, related problem is that existing game semantics does not have all finite limits. In this talk, I sketch my game semantics of dependent types and show that it has all finite limits. Rather than the technical details, I focus on: 1. Why game semantics is useful for the study of logic and computation; 2. Why game semantics of dependent types is difficult; 3. Main idea for the solution; 4. Ongoing and future work. A preprint is available: https://arxiv.org/pdf/1905.00993.pdf.



• 26.05.2021
  
  Grigory Olkhovikov (Ruhr University Bochum): A maximality result for bi-intuitionistic propositional logic

  I will report on a recent Lindström theorem for bi-intuitionistic propositional logic (joint work with Guillermo Badia) showing that this logic is the maximal (with respect to expressive power) abstract logic satisfying a certain form of compactness, the Tarski union property, and preservation under bi-asimulations. The result constitutes an extension of previous work done for the propositional intuitionistic logic in: G. Badia and G. Olkhovikov. A Lindström theorem for intuitionistic propositional logic. Notre Dame Journal of Formal Logic, 61 (1): 11-30 (2020). However, due to the presence of a backwards-looking connective in bi-intuitionistic logic, the current result features a number of non-trivial modifications of the techniques and ideas employed in the previous work.



• 19.05.2021 [Bern-Prague Joint Seminar]
  
  Wesley Fussner (University of Nice Sophia Antipolis): Generalized basic logic from a modal point of view

  Generalized basic logic was introduced through its algebraic semantics (GBL-algebras) in order to provide a natural common generalization of lattice-ordered groups, Heyting algebras, and BL-algebras. When formulated with exchange, weakening, and falsum, generalized basic logic is a fragment of both Hájek's basic logic and propositional intuitionistic logic. In this formulation, the relationship between generalized basic logic and Łukasiewicz logic parallels the thoroughly-studied relationship between intuitionistic logic and classical logic. This talk explores several ways that the latter parallel manifests. First, we illustrate a relational semantics for generalized basic logic where worlds are valued in MV-algebras (analogous to the usual, Boolean-valued Kripke semantics for intuitionistic logic). Second, we present a translation of generalized basic logic into a modal Łukasiewicz logic that is analogous to the Gödel-McKinsey-Tarski translation of intuitionistic logic into the classical modal logic S4. All of these results are obtained with the help of the algebraic theory of GBL-algebras, and we also provide a brief survey of the latter.



• 05.05.2021
  
  Shawn Standefer (Slovak Academy of Sciences): Varieties of necessity in a non-classical setting

  In standard modal logics, there are three common conceptions of necessity:, the universal conception, the equivalence relation conception, and the axiomatic conception. theses provide distinct presentations of the modal logic S5, commonly used in metaphysics and epistemology. In standard settings, these presentations coincide, giving three views of a single, unified logic. I will explore these different conceptions in the context of the relevant logic R, explaining when they come apart and why that matters. This reveals that there are many options for being an S5-ish extension of R. It further reveals a divide between the universal conception of necessity on the one hand, and the axiomatic conception on the other: The latter is consistent with motivations for relevant logics while the former is not. For the committed relevant logician, necessity cannot be truth in all possible worlds.



• 28.04.2021 [Bern-Prague Joint Seminar]
  
  Iris van der Giessen (Utrecht University): The admissible rules of Lax Logic

  Propositional Lax Logic is a fascinating intuitionistic modal logic with a non-standard modality that combines some properties of a ‘Box’ and some properties of a ‘Diamond’. In this talk I will present recent results about its admissible rules. The admissible rules are those rules under which the set of theorems of a logic is closed. Thereby they give insight in the structure of all possible inferences in a logic. Iemhoff (2001) showed that the so-called Visser rules form a basis for the admissible rules of IPC. Similarly, modal Visser rules are formulated for modal logics such as K4, S4 and GL (Jeřábek 2005). I will characterize a sequent-based proof system for the admissible rules of propositional Lax Logic, containing Visser-like rules. In this work we will see that the structure of the relational semantics will be of great importance.



• 21.04.2021 [Bern-Prague Joint Seminar]
  
  Federico Faroldi (Ghent University and University of Salzburg): The Structure of Reasons: Subtraction and Partiality

  Practical reasons are central both in everyday normative reasoning and in normative theorizing, but most accounts treat them as atomic and flat. In this talk, I investigate the structure of practical reasons in order to deal with aggregation, double counting, subtraction, and partiality. The ideal aim is to give a unified formal account that is able to serve as a semantic backdrop to construct natural logical systems to reason with reasons, based on a hyperintensional justification logic with a truthmaker semantics.



• 14.04.2021
  
  Hitoshi Omori (Ruhr University Bochum): Two applications of Herzberger’s semantics

  In his paper "Dimensions of truth", Hans Herzberger develops a semantic framework that captures both classical logic and weak Kleene logic through one and the same interpretation. The aim of this talk is to apply the simple idea of Herzberger to two kinds of many-valued semantics. This application will be led by the following two questions: (i) Is de Finetti conditional a conditional? (ii) What do CL, K3 and LP disagree about? Note: This is a joint work with Jonas R. B. Arenhart.



• 18.03.2021 (Thursday) [Joint session with the Logic Seminar of the Institute of Philosophy, CAS]
  
  Berta Grimau and Carles Noguera (The Czech Academy of Sciences): These Degrees go to Eleven: Fuzzy Logics and Graded Predicates

  In the literature on vagueness one finds two very different kinds of degree theory. The dominant kind of account of gradable adjectives in formal semantics and linguistics is built on an underlying framework involving bivalence and classical logic: its degrees are not degrees of truth. On the other hand, fuzzy logic based theories of vagueness --largely absent from the formal semantics literature but playing a significant role in both the philosophical literature on vagueness and in the contemporary logic literature-- are logically nonclassical and give a central role to the idea of degrees of truth. Each kind of degree theory has a strength: the classical kind allows for rich and subtle analyses of ordinary language constructions such as the positive and comparative forms of gradable adjectives, while the fuzzy kind yields a compelling solution to the sorites paradox. In this talk we will argue that the fuzzy kind of theory can match the benefits of the classical kind but not vice versa. We develop a new version of the fuzzy logic approach that --unlike existing fuzzy theories-- yields compelling analyses of ordinary language constructions such as the positive and comparative forms of gradable adjectives, while retaining the advantage of genuinely solving the sorites paradox. At the same time we will argue that a bivalent, classical approach to vague predicates cannot form the basis for an equally convincing solution to the sorites. As an overall conclusion we will defend that the nonclassical, fuzzy kind of degree theory is superior. (Joint work of Petr Cintula, Berta Grimau, Carles Noguera, and Nicholas J.J. Smith)



• 10.03.2021 [Bern-Prague Joint Seminar]
  
  Brett McLean (Université Nice Sophia Antipolis): Temporal logic of Minkowski spacetime

  If we wish to do temporal logic on (flat) spacetime, special relativity suggests we should use an accessibility relation that is independent of the choice of inertial frame, and that there are a limited number of ways to do this. Two possible accessibility relations are 'can reach with a lightspeed-or-slower signal' and 'can reach with a slower-than-lightspeed signal'. We focus on the resulting frames in 2D spacetime (1 space + 1 time dimension). For both frames, validity of formulas in the basic temporal language is a PSPACE-complete problem. I will describe the proofs of these results and also how those proofs can be extended to obtain results on interval logics. This is joint work with Robin Hirsch. The lightspeed-or-slower case is due to Hirsch and Reynolds.



• 24.02.2021 [Bern-Prague Joint Seminar]
  
  Luca Reggio (University of Oxford): Counting Homomorphisms Between Finite Structures

  Lovász (1967) showed that two finite relational structures A and B are isomorphic if, and only if, the number of homomorphisms from C to A is the same as the number of homomorphisms from C to B for any finite relational structure C. Categorical generalisations of this result were proved independently in the early 1970s by Lovász and Pultr. I will present another categorical variant of Lovász' theorem and explain how it can be used, in combination with the game comonads recently introduced by Abramsky et al., to obtain homomorphism counting results in finite model theory. This is joint work with Anuj Dawar and Tomáš Jakl.



• 17.02.2021
  
  Igor Sedlár (The Czech Academy of Sciences): Changing the World, Constructively

  The finite tree property of intuitionistic logic entails completeness with respect to posets where each element, seen as a possibly partial situation, is under a maximal element, seen as a possible world containing the situation. This suggests a natural semantics for intuitionistic modal logic based on posets with a binary relation on the set of maximal elements. In this semantics, truth of modal formulas in a situation is determined by looking at worlds containing the situation and worlds accessible from them. In this paper we study modal logics arising from such a semantics. A general completeness-via-canonicty result is provided and various operations on such posets including filtrations are studied. Differences with respect to intuitionistic modal logics known from the literature are discussed. In the final part a completeness result for a version of intuitionistic propositional dynamic logic based on the framework is obtained and the logic is shown to be decidable.



• 03.02.2021
  
  Guillermo Badia (University of Queensland): 0-1 Laws in Mathematical Fuzzy Logic

  The 0-1 law for classical first-order logic states that, in a relational vocabulary, every formula is almost always true or almost always false on finite models. This theorem is due to Ronald Fagin and was proved in the 1970s building up on work started by Carnap. Given the failure of traditional model-theoretic properties such as compactness on finite models, it was quite remarkable to find a native of the finite setting using probabilistic techniques. In this talk, I will generalize the classical theorem to a many-valued context in the following form: for every formula there is a truth-value that the formula takes almost always or almost never on finite models. The new result will cover the cases of finitely-valued fuzzy logics such as Łukasiewicz, Gödel-Dummet and Product logics (and, of course, Boolean logic as an extreme case). This work also generalizes a theorem obtained in a more limited setting for the case of some Łukasiewicz logics by Robert Kosik and Chris Fermüller. (Joint work with Carles Noguera)



• 16.12.2020
  
  Jamie Wannenburg (University of Pretoria): Some algebraic (and topological) tools and their application to logic

  The talk will be a non-technical overview of the speaker’s research interests, for the purpose of introducing the researcher to the working group. The main areas of interest are Abstract Algebraic Logic, Universal Algebra, and Substructural Logic—with a focus on Relevance and Intuitionistic Logics. But the talk will focus on a handful of specific tools from these areas, ex. Birkhoff’s Theorem, Jónsson's Theorem, some Bridge theorems and Esakia Duality, emphasising their applications and giving examples from the speaker's previous research.



• 02.12.2020
  
  Adam Přenosil (Vanderbilt University): Logics of n-filters

  Classical logic is defined by truth-preservation in Boolean algebras: if the premises take the top value, then so does the conclusion. Dually, one might be interested in logics defined by the preservation of non-falsity: if the conclusion takes the bottom value, then so does one of the premises. Such logics are paraconsistent: in the four-element Boolean algebra both x and its negation may be non-false. In addition, the familiar rule of adjunction fails here: we may not infer that the conjunction of x and y is non-false given that x and y are non-false. In this talk, we shall study logics of non-falsity and other logics generated by upsets of Boolean and De Morgan algebras. In particular, we show that each finitely generated extension of the four-valued logic of Belnap and Dunn (FDE), admits a completeness theorem with respect to a finite Gentzen calculus, though not always a finite Hilbert calculus.



• 18. 11. 2020
  
  Kentaro Yamamoto (ICS CAS): The Combinatorics of Finite Heyting Algebras and the Topological Group of The Automorphisms of Their Limit
  
  

  There are several results linking combinatorial properties of Fraïssé classes, certain classes of structures having the amalgamation property, and topological properties of the automorphism groups of their limits. In this talk, the speaker's work in progress on one instance of research in this vein, which is on the Fraïssé class of finite Heyting algebras will be presented. This class is not uniformly locally finite unlike most other examples considered in this vein of research. It will be shown that our automorphism group is non-isomorphic to existing examples and that it is non-amenable. At the end of the talk, future research ideas pertaining to the Ramsey property of the class and, equivalently, the extreme amenability of the automorphism group will be discussed.



• 04.11.2020
  
  Tommaso Moraschini (Uni. of Barcelona): On Equational Completeness Theorems
  
  

  A logic is said to admit an equational completeness theorem when it can be interpreted into the equational consequence of some class of algebras. Even if the vast majority of completeness theorems in the literature are of this form, it is known that there are logics lacking any equational completeness theorem. Despite the simplicity of this notion, intrinsic characterizations of logics with admitting an equational completeness theorem have proved elusive. This is partly because equational completeness theorems can take unexpected forms, e.g., in view of Glivenko's Theorem, classical propositional logic is related to the variety of Heyting algebras by a (certainly nonstandard) equational completeness theorem. As it happens, nonstandard equational completeness theorems of this form are ubiquitous.

  In this talk, we present a characterization of logics with at least one tautology (resp. locally tabular logics) admitting an equational completeness theorem. For a protoalgebraic logic, this amounts to the demand that there are two distinct logically equivalent formulas. While the problem of determining whether a logic admits an equational completeness theorem will be shown to be decidable for logics presented by a finite set of finite matrices and for locally tabular logics presented by a finite Hilbert calculus, we shall see that it becomes undecidable for arbitrary logics presented by finite Hilbert calculi. The undecidability result persists even if we restrict to equivalential logics.

  A draft collecting these observations is available online at http://uivty.cs.cas.cz/~moraschini/files/submitted/equational.pdf

• 21.10.2020
  
  Igor Sedlár (ICS CAS): Generalizing the Completeness Argument for Propositional Dynamic Logic
  
  The standard argument establishing weak completeness of Propositional Dynamic Logic with respect to Kripke models relies on the presence of Boolean negation in the language and produces a finite counter-model for each non-theorem. Both of these features make the standard argument inapplicable to versions of PDL based on specific non-classical logics, namely, those without Boolean negation and/or without the finite model property. For instance, the former applies to PDL based on intuitionistic and many superintuitionistic logics, the latter applies to PDL combined with Boolean Lambek calculus and both apply to PDL based on some relevant logics. In this talk, I will outline a generalization of the standard completeness argument that covers this wider class of propositional dynamic logics.


• 14.10.2020
  
  Andrew Tedder (ICS CAS): Decidability and Consistency in Some Paraconsistent Arithmetics
  
  Following on some joint work with Badia, Cintula, and Hájek, I'll show that two arithmetic theories couched in first order extensions of the three-valued paraconsistent logics A3 and RM3 are essentially undecidable (i.e. any $\Sigma_1$-consistent extension/expansion of these is undecidable). With this in hand, I'll consider questions of decidability concerning some $\Sigma_1$-inconsistent extensions of these theories. I'll conjecture that the theory in question has some $\Sigma_1$-inconsistent (but non-trivial) extensions which are decidable, and some which are undecidable, suggesting candidates for these extensions from among inconsistent models of arithmetic.


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


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


• 12. 12. 2018
  
  Berta Grimau (UTIA CAS): The Instability of Plural Scepticism towards Superplural Logic
  
  Abstract: Plural Logic is an extension of First-Order Logic which has, as well as singular terms and quantifiers, their plural counterparts. Analogously, Superplural Logic is an extension of Plural Logic which has, as well as plural terms and quantifiers, superplural ones. The basic idea is that superplurals stand to plurals like plurals stand to singulars (they are pluralized plurals). Allegedly, Superplural Logic enjoys the expressive power of a simple type theory while committing us to nothing more than the austere ontology of First-Order Logic. Were this true, Superplural Logic would be a useful tool, with various applications in the philosophy of mathematics, metaphysics and formal semantics. However, while the notions of plural reference and quantification enjoy widespread acceptance today, their superplural counterparts have been received with a lot of scepticism. In this talk, I will argue for the legitimacy of a face value interpretation of Superplural Logic by showing that some ordinary languages display clear cases of superplural reference and that they do so in an indispensable manner. Since the arguments I will put forward are of the same sort friends of Plural Logic have employed to defend their position, I will conclude that the (commonly held) view that Plural Logic is legitimately interpreted at face value but not so its superplural extensions is likely to suffer from internal tensions.


• 5. 12. 2018
  
  Guillermo Badia (Kepler University, Linz): Maximality of first-order logics based on finite MTL-chains
  
  


• 28. 11. 2018
  
  Andrew Tedder (ICS CAS): Residuals and conjugates in positive substructural logic
  
  Abstract: While the relations between an operation and its residuals play an essential role in substructural logic, a closely related relation between operations is that of conjugation - so closely related that with Boolean negation, the conjugates and residuals of an operation are interde_nable. In this talk extensions of the Lambek Calculus including conjugates of fusion (without negation) are investigated. Some interesting properties of the conjugates are discussed, a proof system is presented, its adequacy questioned, and some applications are considered.


• 21. 11. 2018
  
  Carles Noguera (UTIA CAS): General neighborhood and Kripke semantics for modal many-valued logics
  
  Abstract: Frame semantics, given by Kripke or neighborhood frames, do not give completeness theorems for all modal logics extending, respectively, K and E. Such shortcoming can be overcome by means of general frames, i.e. frames equipped with a collection of admissible sets of worlds (which is the range of possible valuations over such frame). We export this approach from the classical paradigm to modal many-valued logics by defining general A-frames over a given residuated lattice A (i.e., the usual frames with a collection of admissible A-valued sets). We describe in details the relation between general Kripke and neighborhood A-frames and prove that, if the logic of A is finitary, all extensions of the corresponding logic E of A are complete w.r.t. general neighborhood frames. Our work provides a new approach to the current research trend of generalizing relational semantics for non-classical modal logics to circumvent axiomatization problems.


• 14. 11. 2018
  
  Luca Reggio (ICS CAS): Duality, definability and continuous functions
  
  Abstract: Weierstrass approximation theorem states that any continuous real-valued function defined on a closed real interval can be approximated by polynomials. In 1937 Marshall Stone proved a vast generalisation of this result: nowadays known as the Stone-Weierstrass theorem, this is a fundamental result of functional analysis with far-reaching consequences. We show how, through duality theory, the Stone-Weierstrass theorem can be seen as an instance of the Beth definability property of a certain logic.


• 19. 10. 2018
  
  Special session -- Amanda Vidal (ICS CAS): Generalizing Geiger's result to two valued versions
  
  Abstract: We will go through an introduction to the algebraic approach to CSP and VCSP. We will then explore a notion of order-homomophism over valued structures that gives place to certain polymorphisms, and we show that these polymorphisms, considered over a small transformation of the original structure, characterize up to preservation the set of pp-definable formulas in the structure. When the polymorphisms preserve both strong or weak conjunction, they will characterize the corresponding definable formulas in locally finite structures. This can be seen as a natural generalization of Geigers characterization result for usual CSP to valued cases. Moreover, we will study how these kind of polymorphisms can be modified to preserve positive formulas with strong conjunction only (in the sense of the usual VCSP studied in the literature).