Seminar Announcement
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.
Talk by : Decidable Fragments of First Order Modal Logic
@ Seminar on Applied Mathematical Logic13.12.2023 16:00
First Order Modal Logic (FOML) extends First Order Logic (FO) with modal operators. FOML is suitable for many applications including planning, predicate epistemic logics among others. However, FOML is computationally unfriendly. Most of the decidable fragments of FO that are decidable (like the two variable fragment, guarded fragment, restriction to unary predicates) become undecidable when extended with modal operators. Until recently, the only known decidable fragment of FOML was the monodic fragment. In this talk we will discuss some new and interesting decidable fragments of FOML and its variants that we have identified. This talk includes some of the results from the speaker's PhD thesis (supervised by R. Ramanujam) and some results in collaboration with Mo Liu, R. Ramanujam and Yanijing Wang.
Talk by : A Tour of Substructural Interpolation
@ Seminar on Applied Mathematical Logic08.11.2023 16:00
"Interpolation" refers to a cluster of fundamental metalogical properties with applications spanning hardware and software verification, databases, and many other areas. In this talk, we survey the state of the art on interpolation in substructural logics, focusing in particular on big-picture features that shed some light on the nature of interpolation generally. We will also discuss some of the most important remaining open questions and on-going efforts to solve them.
Talk by : Maximum satisfiability problem in the real-valued MV-algebra
@ Seminar on Applied Mathematical Logic01.11.2023 16:00
In propositional Boolean logic, maximum satisfiability (MaxSAT) problem can be viewed as a generalization of the SAT problem. An input to the SAT problem is a CNF formula (a list of clauses) and the question is whether there is an assignment that satisfies all of them. MaxSAT is an optimization problem, namely to determine the maximum number of satisfied clauses in the list, over all assignments. Our work addresses the MaxSAT problem problem for a list of arbitrary formulas in the language of propositional Łukasiewicz logic, over the semantics provided by the MV-algebra on the real interval [0,1]. First we reduce the MaxSAT problem to the SAT problem in the same semantics. This provides a classification against which other approaches to the problem can be compared. Then we define a tableau-like method that eventually yields one or more systems of linear constraints, similar to the earlier approaches of Hähnle or Olivetti. This is joint work with Felip Manya and Amanda Vidal, presented at Tableaux 2023.
Talk by : Negated Implications in Connexive Relevant Logics
@ Seminar on Applied Mathematical Logic04.10.2023 16:00
Adding connexive theses to relevant logics has the unsavoury result of allowing one to prove every negated implication. In this talk, I'll diagnose this problem, and consider some avenues by which this result can be avoided.
Talk by : Fuzzy Information States and Fuzzy Support
@ Seminar on Applied Mathematical Logic07.06.2023 16:00
The semantic framework for representing questions known as inquisitive semantics is based on a relation of support relating formulas and information states (modeled as sets of possible worlds). In my talk I will discuss two ways of fuzzifying inquisitive semantics. The first one replaces crisp information states with fuzzy information states (modeled as fuzzy sets of possible worlds). The second one replaces the crisp notion of support with a notion of fuzzy support. I will show some properties of the resulting framework. For example, I will show that if we fuzzify inquisitive semantics in these two different directions, we obtain an abstract and very general version of a principle known from the basic inquisitive semantics as Truth-Support Bridge. I will also sketch some open questions related to this approach.
Talk by : Everyone Knows that Everyone Knows
@ Seminar on Applied Mathematical Logic17.05.2023 16:00
A gossip protocol is a procedure for sharing secrets in a network. The basic action in a gossip protocol is a telephone call wherein the calling agents exchange all the secrets they know. An agent who knows all secrets is an expert. The usual termination condition, given a finite number of agents, is that all agents are experts. We report on research investigating the termination condition that all agents know that all agents are experts. If agents only exchange secrets, there is no knowledge of the time, and no knowledge of the protocol, even stronger termination conditions are unreachable. Furthermore, n-2 + (n choose 2) calls are optimal to reach this epistemic goal. Although it is easy to come up with schedules achieving this, it is remarkably non-trivial to show that they are optimal.
Talk by : A Simplified Lower Bound on Intuitionistic Implicational Proofs
@ Seminar on Applied Mathematical Logic10.05.2023 16:00
One of the major open problems in classical proof complexity is to prove super-polynomial lower bounds on the length of proofs in Frege (aka Hilbert-style) systems, or equivalently, sequent calculus or natural deduction. Interestingly, exponential lower bounds are known for some non-classical logics (modal, superintuitionistic, substructural), starting with seminal work of Hrubeš (2007); they are all based on variants of the feasible disjunction property that play a similar role as monotone feasible interpolation for classical proof systems. This might suggest that the presence of disjunction is essential for these lower bounds, but Jeřábek (2017) adapted them to the purely implicational fragment of intuitionistic logic. This results in a complex argument employing an implicational translation of intuitionistic logic on top of the proof of the lower bound proper, which in turn relies on monotone circuit lower bounds (Razborov, Alon–Boppana). In this talk, I will show how to prove the exponential lower bound directly for intuitionistic implicational logic without any translations, using a simple argument based on an efficient version of Kleene’s slash. Apart from Frege, it applies directly to sequent calculus and (dag-like) natural deduction, obviating also the need for translation of these proof systems to Frege. One motivation for this work comes from presistent claims by Gordeev and Haeusler, who purport to show that all intuitionistic implicational tautologies have polynomial-size dag-like natural deduction proofs, implying NP = PSPACE. Their claims are false as they contradict the above-mentioned exponential lower bounds (and, in fact, also older exponential lower bounds on constant-depth proofs), but for a non-specialist, understanding this requires tracking down multiple papers and some reading between the lines. Our argument consolidates all proof-theoretic components of the lower bound into one simple proof, depending only on the Alon–Boppana circuit lower bound.
Talk by : How to compute uniform interpolant semantically
@ Seminar on Applied Mathematical Logic03.05.2023 16:00
This talk will be a tutorial of a known technique on computing uniform interpolants by examining finite (or finitely generated) algebras and their extensions. We will focus on intermediate logics, but the method is reasonably general.
Talk by : Promise Model Checking Problems over a Fixed Model
@ Seminar on Applied Mathematical Logic19.04.2023 16:00
The fixed-template constraint satisfaction problem (CSP) can be seen as the problem of deciding whether a given primitive positive first-order sentence is true in a fixed structure (also called model). We study a class of problems that generalizes the CSP simultaneously in two directions: we fix a set L of quantifiers and Boolean connectives, and we specify two versions of each constraint, one strong and one weak. Given a sentence which only uses symbols from L, the task is to distinguish whether the sentence is true in the strong sense, or it is false even in the weak sense. We classify the computational complexity of these problems for the existential positive equality-free fragment of first-order logic and we prove some upper and lower bounds for the positive equality-free fragment. The partial results are sufficient, e.g., for all extensions of the latter fragment. This is a joint work with Kristina Asimi and Silvia Butti.
Talk by : Computational Content of a Generalized Kreisel-Putnam Rule
@ Seminar on Applied Mathematical Logic22.03.2023 16:00
In this talk, we propose a computational interpretation of the generalized Kreisel-Putnam rule, also known as the generalized Harrop rule or simply the Split rule, in the style of BHK semantics. We will achieve this by exploiting the Curry-Howard correspondence between formulas and types. First, we inspect the inferential behavior of the Split rule in the setting of a natural deduction system for the intuitionistic propositional logic. This will guide our process of formulating an appropriate program that would capture the corresponding computational content of the typed Split rule. In other words, we want to find an appropriate selector function for the Split rule by considering its typed variant. Our investigation can also be reframed as an effort to answer the following questions: is the Split rule constructively valid? Our answer is positive for the Split rule as well as for its newly proposed generalized versions.
Talk by : First-Order Proof Schemata and Inductive Proof Analysis
@ Seminar on Applied Mathematical Logic08.03.2023 16:00
Proofs are more than just validations of theorems; they can contain interesting mathematical information like bounds or algorithms. However this information is frequently hidden and proof transformations are required to make it explicit. One such transformation on proofs in sequent calculus is cut-elimination (i.e. the removal of lemmas in formal proofs to obtain proofs made essentially of the syntactic material of the theorem). In his famous paper ``Untersuchungen ueber das logische Schliessen'' Gentzen showed that for cut-free proofs of prenex end-sequents Herbrand's theorem can be realized via the midsequent theorem. In fact Gentzen defined a transformation which, given a cut-free proof p of a prenex sequent S, constructs a cut-free proof p' of a sequent S' (a so-called Herbrand sequent) which is propositionally valid and is obtained by instantiating the quantifiers in S. These instantiations may contain interesting and compact information on the validity of S. Generally, the construction of Herbrand sequents requires cut-elimination in a given proof p (or at least the elimination of quantified cuts). The method CERES (cut-elimination by resolution) provides an algorithmic tool to compute a Herbrand sequent S' from a proof p (with cuts) of S even without constructing a cut-free version of p. A prominent and crucial principle in mathematical proofs is mathematical induction. However, in proofs with mathematical induction Herbrand's theorem typically fails. To overcome this problem we replace induction by recursive definitions and proofs by proof schemata. An extension of CERES to proof schemata (CERESs) allows to compute inductive definitions of Herbrand expansions (so-called Herbrand systems) representing infinite sequences of Herbrand sequents, resulting in a form of Herbrand's theorem for inductive proofs.
Talk by : One-variable RQ & RS5: A Frame Based Equivalence
@ Seminar on Applied Mathematical Logic01.03.2023 16:00
Often, for a propositional logic L, some one-variable fragment of L's first order extension corresponds to some modal logic on L. For the relevant logic R, it seems that the one-variable fragment of RQ (the stronger of R's two standard first-order extensions) corresponds to the modal relevant logic RS5 (the S5ish axiomatic extension of R which contains classical S5 in translation). This talk is a work in progress showing this equivalence. One direction of the equivalence is obtained by transforming first-order models into modal models. The other direction is (almost) obtained by evaluating all of RQ in a particular modal model. I also discuss some philosophical upshots/consequences of this result.
Talk by : Kleene Algebra With Tests for Weighted Programs
@ Seminar on Applied Mathematical Logic25.01.2023 16:00
Weighted programs generalize probabilistic programs and offer a framework for specifying and encoding mathematical models by means of an algorithmic representation. Kleene algebra with tests is an algebraic formalism based on regular expressions with applications in proving program equivalence. We extend the language of Kleene algebra with tests so that it is sufficient to formalize reasoning about a simplified version weighted programs. We introduce relational semantics for the extended language, and we generalize the relational semantics to an appropriate extension of Kleene algebra with tests, called Kleene algebra with weights and tests. We demonstrate by means of an example that Kleene algebra with weights and tests offers a simple algebraic framework for reasoning about equivalence and optimal runs of weighted programs.
Talk by : A Parametrised Axiomatization for a Large Number of Restricted Second-Order Logics
@ Seminar on Applied Mathematical Logic11.01.2023 16:00
By limiting the range of the predicate variables in a second-order language one may obtain restricted versions of second-order logic such as weak second-order logic or definable subset logic. In this note we provide an infinitary strongly complete axiomatization for several systems of this kind having the range of the predicate variables as a parameter. The completeness argument uses simple techniques from the theory of Boolean algebras.