Seminar Announcement
Talk by : Weighted Automata and Quantitative Logics
@ Seminar on Applied Mathematical Logic20.11.2024 14:00
Quantitative models and quantitative analysis in Computer Science are receiving increased attention. The goal of this talk is to investigate quantitative automata and quantitative logics. Weighted automata on finite words have already been investigated in seminal work of Schützenberger (1961). They consist of classical finite automata in which the transitions carry weights. These weights may model, e.g., the cost, the consumption of resources, or the reliability or probability of the successful execution of the transitions. This concept soon developed a flourishing theory. We investigate weighted automata and their relationship to weighted logics. For this, we present syntax and semantics of a quantitative logic; the semantics counts ‘how often’ a formula is true in a given word. Our main result, extending the classical result of Büchi, shows that if the weights are taken from an arbitrary semiring, then weighted automata and a syntactically defined fragment of our weighted logic are expressively equivalent. A corresponding result holds for infinite words. Moreover, this extends to quantitative automata investigated by Henzinger et al. with (non-semiring) average-type behaviors, or with discounting or limit average objectives for infinite words.
Talk by : Isabelle/HOL and Its Logic: User's Point of View
@ Seminar on Applied Mathematical Logic06.11.2024 14:00
Isabelle is a generic proof assistant that allows axiomatization of arbitrary object logic, the most widely used of which is HOL. The talk will be an introduction in Isabelle/HOL. I will briefly sketch its history and mention my motivation for using it in an ongoing project of formalization of combinatorics on words. The main part of the talk will be a live session illustrating how some design features of Isabelle/HOL are reflected in user's work. Time permitting, these will include the distinction between meta-logic and the object logic, polymorphic simple types, higher order unification, (non-existence of) proof terms, design of proof tactics, and construction of verified algorithms.
Talk by : About semilinear prevarieties of Abelian l-groups
@ Seminar on Applied Mathematical Logic30.10.2024 14:00
It is a well-known fact that Abelian logic has no finitary extensions (which is equivalent to the fact that the quasivariety of Abelian l-groups has no notrivial subquasivariety). In this talk we will try to axiomatize all semilinear (infinitary) extensions of Abelian logic. Alternatively, we will try to provide an axiomatization for all semilinear prevarieties of abelian l-groups. The strategy we will try to use is as follows: For a subdirectly irreducible chain C, we find a generalized quasiequation E such that for any Abelian l-group A we have: E does not hold in A if C is embeddable in A.
Talk by : Abduction in the extensions of the Belnap--Dunn logic
@ Seminar on Applied Mathematical Logic23.10.2024 14:00
We explore the problem of explaining observations from a classically inconsistent theory by adopting a paraconsistent framework. In particular, we consider theories formulated in the languages of the Belnap — Dunn logic and its implicative expansion. The solutions are then given in one of the two further expansions of BD: BD○ that introduces formulas of the form ○ф (‘the information on ф is reliable’) and BD△ that augments the language with △ф's (‘there is information that ф is true’). We show that explanations in BD○ and BD△ are not reducible to one another. We analyse the complexity of standard abductive reasoning tasks (solution recognition, solution existence, and relevance / necessity of hypotheses) depending on the language of the solution and on the language of the theory. In addition, we consider the complexity of abductive reasoning in the Horn fragment of the implicative extension of BD.
Talk by : Mathematics as a natural and dynamic process. Philosophical arguments.
@ Seminar on Applied Mathematical Logic17.10.2024 14:00
Viewing mathematics as a natural and dynamic process offers an explanation for its effectiveness that is totally free of supernatural assumptions and is therefore virtually verifiable. Considering it as a cultural product offers an explanation for its historical evolution and at the same time for its being commonly perceived as externally existing. Consequently, the concept of truth also changes: one moves from a truth that is given to a careful management of acquired information. To this aim, one must keep all conceptual distinctions and thus adopt a minimal stock of assumptions. Adopting this minimalist foundation not only allows one to develop mathematics at will, but also brings out deep structures and solves problems that were previously left in the dark. Also, it turns out that topology is crucial in keeping the real aspects of mathematics, expressed by pointfree topology, distinct from the ideal aspects, expressed by ideal points and spaces over a pointfree structure. These are thus introduced mathematically and explicitly, and justified by their conservativity over the real aspects, and not declared to exist by the pure logical consistency of the formal system by which they are implicitly defined. In this way, an ideal abstract mathematics can be developed that does not suffer from the abstrusities of axiomatic set theory ZFC and, in particular, maintains the priority of the computational aspects of mathematics. All of this can be seen as the beginning of a new paradigm in mathematics, in the sense of Kuhn, or as the completion of the set-theoretic revolution initiated by Frege and Cantor. Either way, it establishes a healthier and more direct relation to reality, not mediated by ideologies of various kinds.
Talk by : Mathematics as a natural and dynamic process. Mathematical facts.
@ Seminar on Applied Mathematical Logic16.10.2024 16:00
In a dynamic vision, in which mathematics is seen as a human product, one moves from a given truth to a careful handling of acquired information. So the foundation is intuitionistic (Law of Excluded Middle is not assumed) to distinguish positive existence, predicative (Power Set Axiom is not assumed) to distinguish sets constructed from below from collections, effective (Axiom of unique Choice is not assumed) to distinguish operations with explicit instructions from functions. Adopting this minimalist foundation in practice brings out some deep underlying structures of topology, such as logical duality between closed and open, symmetry between points and observables, continuity as a commutative square, etc., that were previously hidden by too strong assumptions. Topology in the proper sense is obtained by adding a module of convergence to these basic structures. In this way, richer notions are obtained so that, for example, it can be proved that there is an embedding of the category of concrete spaces, with points, into that of positive topologies, which are pointfree. This brings to solution an issue that has been open for more than half a century, It turns out that topology plays a central role for all mathematics, since it allows one to distinguish real, or computational, aspects from ideal, or infinitary ones. Since points are usually determined by an infinite amount of information, in order to maximize the computational, or real, aspects of mathematics, pointfree topology must be developed as much as possible. Ideal aspects are introduced locally and explicitly as ideal points and spaces over a positive topology. The most important structures in mathematics, such as real numbers, Zariski topology, etc., are obtained as ideal spaces over a positive topology. A lot of future work remains: primarily, to expand the mathematics expressible in this way as much as possible and to develop a proof assistant based on the minimalist foundation.
Talk by : Epistemic Probability Logics
@ Seminar on Applied Mathematical Logic09.10.2024 16:00
Epistemic logics formalise reasoning about agents' epistemic attitudes, such as knowledge and belief, towards the occurrence or non-occurrence of events. Similarly, epistemic probability logics formalise reasoning about epistemic attitudes towards the probability of events. One of the most important epistemic probability logics studied in the literature is Fagin and Halpern's PS5 (Fagin and Halpern, 1994), which extends the standard multi-agent epistemic logic S5 with probability operators expressing linear combinations of probabilities of events. In this work-in-progress talk, we outline an alternative approach to combining epistemic logics with probability, based on modal fuzzy logic. Our work aims at extending the results of a recent paper by Baldi, Cintula and Noguera (2020), who showed that there are mutual translations between the propositional fragment of PS5 and the fuzzy logic of probability introduced by Hájek et al. (2000), based on propositional Łukasiewicz logic. Our aim is to determine whether there are similar translations linking richer fragments of PS5, including modal operators, and fuzzy probability logics based on modal Łukasiewicz logic.
Talk by : One is all you need: Second-order Unification without First-order Variables
@ Seminar on Applied Mathematical Logic05.06.2024 16:00
We consider the fragment of Second-Order unification, referred to as Second-Order Ground Unification (SOGU), with the following properties: (i) only one second-order variable allowed, (ii) first-order variables do not occur. We show that Hilbert's 10th problem is reducible to a necessary condition for SOGU unifiability if the signature contains a binary function symbol and two constants, thus proving undecidability. This generalizes known undecidability results, as either first-order variable occurrences or multiple second-order variables were required for the reductions. Furthermore, we show that adding the following restriction:(i) the second-order variable has arity 1, (ii) the signature is finite, and (iii) the problem has bounded congruence, results in a decidable fragment. The latter fragment is related to bounded second-order unification in the sense that the number of bound variable occurrences is a function of the problem structure. We conclude with a discussion concerning the removal of the bounded congruence restriction. Joint work with Julian Parsert.
Talk by : A Personal Perspective on the Game Comonad Programme
@ Seminar on Applied Mathematical Logic24.04.2024 16:00
Finite model theory's main focus is in the study of logics that have close connections to descriptive complexity. One of the main tools to show e.g. inexpressibility of certain logics are model comparison games, such as the Ehrenfeucht--Fraisse, pebble, and bisimulation games. The main idea behind game comonads comes from the observation that plays in a typical model comparison game can be encoded into a semantics construction which, moreover, admit the structure of a comonad on the category of relational structures. This allows one to treat model comparison games abstractly, in the language of category theory. In this talk, I give an overview of the game comonad programme, its recent development and open problems. Concretely, I will list the most notable game comonads and explain their relationship with various logic fragments. I will also overview the recent model-theoretic results proved in this framework. I shall also explain how the various different model comparison games can be viewed as an instance of a game in arboreal categories, which are used to axiomatise common features of Eilenberg--Moore categories of coalgebras of game comonads.
Talk by : Pointed lattice subreducts of varieties of residuated lattices
@ Seminar on Applied Mathematical Logic10.04.2024 16:00
The literature on residuated lattices (RLs) contains a number of results describing the lattice reducts of some variety V of RLs. Such results frequently state either that every lattice is a subreduct of some RL in V (for example, if V is the variety of commutative RLs or of cancellative RLs) or that the lattice subreducts are precisely the distributive lattices (for example, if V is the variety of l-groups or of Heyting algebras). We improve on existing results of this form in two ways. Firstly, we consider pointed lattice subreducts (subreducts in the signature expanded by the constant 1 for the multiplicative unit), which gives us more fine-grained information about where exactly a sublattice can occur. Typical properties of interest whose statement requires the signature of pointed lattices are conicity and distributivity at 1. Secondly, instead of considering particular varieties of RLs, we treat semi-K and pre-K RLs uniformly, where K ranges all over positive universal classes of pointed lattices contained in a certain variety. For example, we show that every prelinear RL is distributive and that every preconic RL is distributive at 1. The description of the pointed lattice subreducts of RLs and of CRLs is left as an open problem.
Talk by : Infinitary Rules for Abelian Logic
@ Seminar on Applied Mathematical Logic13.03.2024 16:00
In Abelian logic, the reduced models are lattice-ordered Abelian groups. We will focus on three important linear models of Abelian logic: integers, rational numbers and real numbers. These three structures are indistinguishable using finitary rules, but can be separated using infinitary rules. In this talk, we will focus on finding these rules and discuss properties of the corresponding generalized quasivarieties.
Talk by : New directions in quantum reasoning
@ Seminar on Applied Mathematical Logic14.02.2024 16:00
The logical underpinnings of quantum mechanics have been the subject of sustained interest since Birkhoff and von Neumann’s pioneering work in the 1930s, but progress has been impeded by the difficulty of several fundamental questions in the area, most notably issues connected to decidability. However, recent years have seen the emergence of a new approach that situates quantum logic within the substructural paradigm, opening the possibility of applying totally new techniques. In this talk, we will discuss these recent trends, report on some important progress arising from this perspective, and identify some open remaining questions.
Talk by : On Geometric Implications
@ Seminar on Applied Mathematical Logic07.02.2024 16:00
It is a well-known fact that although the poset of open sets of a topological space is a Heyting algebra, its Heyting implication is not necessarily stable under the inverse image of continuous functions and hence is not a geometric concept. This leaves us wondering if there is any stable family of implications that can be safely called geometric. In this talk, we will first introduce an abstract notion of implication as a binary modality and investigate its basic properties and possible representations. Then, we will use a weaker version of categorical fibrations to define the geometricity of a category of pairs of spaces and implications over a given category of spaces. We will characterize all geometric categories over a given category S, provided that S has some basic closure properties. Specifically, we will show that there is no non-trivial geometric category over the full category of spaces.
Talk by : Relevance Properties in First-Order Relevant Logicss
@ Seminar on Applied Mathematical Logic31.01.2024 16:00
In this work-in-progress talk I begin the discussion of relevance properties available in first-order logics. I explore the philosophical motivation for many first-order variants of the Variable Sharing Property, and show of some logics whether or not they satisfy these properties. Future mathematical and philosophical directions are outlined.
Talk by : special session
@ Seminar on Applied Mathematical Logic25.01.2024 14:00
Talk by : Equational theories of idempotent semifields
@ Seminar on Applied Mathematical Logic24.01.2024 16:00
An idempotent semifield is an idempotent semiring such that its multiplicative reduct is a group. In this talk I will present several results about equational theories of idempotent semifields. The results include that no non-trivial class of idempotent semifields has a finitely based equational theory; that there are continuum-many equational theories of idempotent semifields; and that the equational theory of the class of all idempotent semifields is co-NP-complete. This is joint work with George Metcalfe.
Talk by : What Proof Theory Can Do for You
@ Seminar on Applied Mathematical Logic17.01.2024 16:00
Although the prime object of study for structural proof theory is proof calculi (especially analytic ones), it has many applications to important logical properties, such as conservativity, consistency, decidability, complexity, interpolation, etc. In my talk, I will present some recent successes in solving long-time open problems by proof-theoretic means, including the Lyndon interpolation property for Gödel logic (intermediate logic of linear frames) and the decidability of (bimodal) intuitionistic S4.