Seminar on Applied Mathematical Logic

We consider two expansions of Gödel logic with two versions of paraconsistent negation. The first one is G_inv — the expansion with an involuitive negation ~_i defined via v(~_iA)=1-v(A). The second one is G^2 --- an expansion with a so-called ‘strong negation’ ¬. This logic utilises two independent valuations on [0,1] — v_1 (positive support) and v_2 (negative support) that are connected via ¬. Two valuations in G^2 can be combined into one valuation v on [0,1]^⟕ — the twisted product of [0,1] with itself — with two components v_1 and v_2. The two logics are closely connected but do not coincide since the set of values of G^2 is not ordered linearly. Our main goal is to study different entailment relations in G_inv and G^2 that are induced by filters on [0,1] and [0,1]^⟕, respectively. In particular, we determine the exact number of such relations in both cases, establish whether any of them coincide with the entailment defined via the order on [0,1] and [0,1]^⟕, and obtain their hierarchy. We also construct reductions of filter-induced entailment relations to the ones defined via the order.

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.

We study the connection between the form of the primitive rules of a proof system and the rules the system admits. We introduce a general and syntactically defined family of sequent-style calculi over the modal language and its fragments as an approximate formalization for "constructively acceptable" systems. We call these calculi constructive and show that any strong enough constructive sequent calculus, satisfying a mild technical condition, feasibly admits all Visser’s rules. This means that there exists a polynomial-time algorithm that, given a proof of the premise of a Visser’s rule, provides a proof for its conclusion. As a positive application, we establish the feasible admissibility of Visser’s rules in several sequent calculi for intuitionistic modal logics, including CK, IK, and their extensions by the modal axioms T, B, 4, 5, and the axioms for bounded width and depth, and propositional lax logic. On the negative side, we show that if a strong enough intuitionistic modal logic (satisfying a mild technical condition) does not admit at least one of Visser’s rules, then it cannot have a constructive sequent calculus. Consequently, no intermediate logic other than IPC has a constructive sequent calculus.

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.

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.

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. The talk is based on the joint work with Meghyn Bienvenu and Katsumi Inoue.

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.

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.

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.

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.

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.

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.

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.

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.

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.

We show that while standard first-order inductive logic is not decidable, a large class of inferences in objective Bayesian inductive logic is decidable. Decidability is achieved by reducing the general inference problem to a quantifier-free problem. We show that for any inference if the quantifier-free reduction of the premisses is satisfiable, then the original inference is decidable. We also consider inferences with infinitely many premisses and explore some properties of the logic.

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.

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.

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.

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

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.

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.

In this talk, we investigate connections between the family of comparative logics including Abelian logic, and some generalizations of Łukasiewicz logic. We provide axiomatizations for some extensions of pointed Abelian logic including unbound Łukasiewicz logic. We show the importance of the semilinearity property and we present the discrete versions of unboud Łukasiewicz logic. This talk is based on joint work with Marta Bílková, Petr Cintula and Carles Noguera.

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.

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.

Some references:

1. Martin Cooper, Andreas Herzig, Faustine Maffre, Frédéric Maris, Pierre Régnier: The epistemic gossip problem. Discrete Mathematics 342(3), pp 654-663, 2019.
2. Hans van Ditmarsch, Malvin Gattinger, Rahim Ramezanian: Everyone Knows that Everyone Knows: Gossip Protocols for Super Experts. Studia Logica, to appear, 2023. https://doi.org/10.1007/s11225-022-10032-3
3. Hans van Ditmarsch, Malvin Gattinger: The Limits to Gossip: Second-Order Shared Knowledge of All Secrets is Unsatisfiable. Proceedings of WoLLIC, pp 237-249, 2022.

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.

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.

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.

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.

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.

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.

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.

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. This is joint work with John L. Bell (see https://arxiv.org/abs/2207.02709).