Seminar Announcement
2021
Talk by : A Generalization of Ultraproducts
@ Seminar on Applied Mathematical Logic10.11.2021 16:00
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’.
Talk by : The automorphism groups of ultrahomogeneous lattices
@ Seminar on Applied Mathematical Logic03.11.2021 16:00
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.
Talk by : Reduction procedures and the meaning of proofs
@ Seminar on Applied Mathematical Logic27.10.2021 16:00
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. and 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 identify 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.
Talk by : Decidability of some intuitionistic and Gödel modal logics with transitivity
@ Seminar on Applied Mathematical Logic20.10.2021 16:00
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).
Talk by : On the adequacy of temporal logics for modelling European transport regulations
@ Seminar on Applied Mathematical Logic26.07.2021 16:00
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.
Talk by : Epimorphisms in varieties of semilinear residuated lattices
@ Seminar on Applied Mathematical Logic23.06.2021 16:00
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.
Talk by : Dependent types and finite limits in games
@ Seminar on Applied Mathematical Logic16.06.2021 16:00
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
Talk by : A maximality result for bi-intuitionistic propositional logic
@ Seminar on Applied Mathematical Logic26.05.2021 16:00
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.
Talk by : Varieties of necessity in a non-classical setting
@ Seminar on Applied Mathematical Logic19.05.2021 16:00
In standard modal logics, there are three common conceptions of necessity: the universal conception, the equivalence relation conception, and the axiomatic conception. These 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.
Talk by : Generalized basic logic from a modal point of view
@ Seminar on Applied Mathematical Logic05.05.2021 16:00
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.
Talk by : The admissible rules of Lax Logic
@ Seminar on Applied Mathematical Logic28.04.2021 16:00
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.
Talk by : The Structure of Reasons: Subtraction and Partiality
@ Seminar on Applied Mathematical Logic21.04.2021 16:00
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.
Talk by : Two applications of Herzberger’s semantics
@ Seminar on Applied Mathematical Logic14.04.2021 16:00
: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:
- Is de Finetti conditional a conditional?
- What do CL, K3 and LP disagree about?
Talk by : These Degrees go to Eleven: Fuzzy Logics and Graded Predicates
@ Seminar on Applied Mathematical Logic18.03.2021 16:00
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).
Talk by : Counting Homomorphisms Between Finite Structures
@ Seminar on Applied Mathematical Logic24.02.2021 16:00
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.
Talk by : Changing the World, Constructively
@ Seminar on Applied Mathematical Logic17.02.2021 16:00
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.
Talk by : 0-1 Laws in Mathematical Fuzzy Logic
@ Seminar on Applied Mathematical Logic03.02.2021 16:00
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 Lukasiewicz, 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 Lukasiewicz logics by Robert Kosik and Chris Fermüller. (Joint work with Carles Noguera)
2020
Talk by : Some algebraic (and topological) tools and their application to logic
@ Seminar on Applied Mathematical Logic16.12.2020 16:00
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.
Talk by : Logics of n-filters
@ Seminar on Applied Mathematical Logic02.12.2020 16:00
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.
Talk by : The combinatorics of finite Heyting algebras and the topological group of the automorphisms of their limit
@ Seminar on Applied Mathematical Logic18.11.2020 16:00
There are several results linking combinatorial properties of Fraissé 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 Fraissé 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.
Talk by : On Equational Completeness Theorems
@ Seminar on Applied Mathematical Logic04.11.2020 16:00
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.
Talk by : Admissibility in the multi-conclusion setting
@ Seminar on Applied Mathematical Logic12.02.2020 16:00
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).
Talk by : Ehrenfeucht-Fraisse methods in the model theory of L-topological spaces over finite MTL-chains
@ Seminar on Applied Mathematical Logic22.01.2020 16:00
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 _nite. In this talk, I consider only MTL algebras, but it is possible that this further restriction can be relaxed.
Talk by : Axiomatic systems of Gödel Modal Logics
@ Seminar on Applied Mathematical Logic11.12.2019 16:00
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 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.
Talk by : Craig interpolation in software verification
@ Seminar on Applied Mathematical Logic04.12.2019 16:00
Craig interpolation is a logical concept popularized in formal veri_cation community by McMillan (2003). Since then, several successful veri_cation 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 unsatis _ability, and _nally present our recent result regarding computation of interpolants for systems of linear inequalities over rational numbers.
Talk by : Information Flow in Logics in the Vicinity of BB
@ Seminar on Applied Mathematical Logic20.11.2019 16:00
B is the basic logic of the Routley-Meyer semantic framework, and BB that of the `neigh-bourhood 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 ow 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 re_ne 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 reections on situation theoretic interpretations of the RM semantics more generally.
Talk by : Profiniteness and finitely generated varieties
@ Seminar on Applied Mathematical Logic23.10.2019 16:00
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.
Talk by : Profinite Heyting algebras and the representation problem for Esakia spaces
@ Seminar on Applied Mathematical Logic30.10.2019 16:00
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.