Advances in Mathematical Logic
- Time: 13:30-17:30, July 7th, 2025
- Venue: Room 329, School of Humanities, Tsinghua University.
Program
13:30-14:20
Proof theory meets decision procedures: a case study in intuitionistic modal logic
A decision algorithm is an automated procedure establishing validity or invalidity of a formula in a given logical system. Proof systems, and in particular sequent calculus, can be fruitfully employed to define such algorithms. A proof theoretic decision procedure implements exhaustive and terminating proof search for the formula in the calculus. If a proof is found the formula is valid. Otherwise, one can usually construct a countermodel for the formula from a finite branch of a failed proof search tree. In the literature, proof-theoretic decision procedures have been defined for a number of systems, there including intuitionistic and modal logics.
In this talk we consider intuitionistic modal logic IK. After introducing the logics and its semantics, we shall present a fully labelled sequent calculus for the logic, explicitly incorporating semantic elements in the syntax. We will then discuss the corresponding decision algorithms, defined by implementing terminating proof search in the labelled calculus.
This talk is based on joint works with Roman Kuznets, Sonia Marin, Marianela Morales, and Lutz Straßburger.
14:20-15:10
Diagonal/circular extensions of a sequent calculus
A well-known sequent calculus for modal logic GL can be gained by `diagonalizing’ the only modal rule in a calculus for K4. To be more precise, given rule (X) in sequent calculus G that principally introduces positive occurrences of a key-note operator, by (d.X) we mean a rule just like (X), but with an extra negative copy of its positive principals at each of its premises. The result of replacing (X) in G by (d.X) is called the `diagonal extension’ of G on (X). The `circular extension’ of a sequent calculus G inherits exactly the same set of rules, but employs a generalized notion of proof called `circular proof’. In a circular proof tree, each leaf can either be derived by a 0-premise rule, or has the sequent same to another node on the unique branch it resides. Daniyar Shamkanov verifies that, circular extension of the mentioned calculus for K4 proves exactly those sequents provable in its diagonal extension (which fits GL). In this talk, we will see that Shamkanov’s result can also be achieved purely in terms of proof transformation, which also leads to a parallel result for Katsumasa Ishii etal.’s calculus of Albert Visser’s BPL. This is a joint work with Yinqiu Zhu.
15:10-15:30
Coffee Break
15:30-16:20
From Tarski to Lawvere, algebraic aspects of predicate logic
This talk is an introduction to the theory of doctrines after Lawvere, and their significance in the community of categorical logic. We shall focus on their semantics and their applications. In recent times some authors are trying to offer new approaches to many classical results in proof theory and syntactic manipulation of theories, including Herbrand’s theorem and Skolemization.
16:20-17:10
From subset spaces to modal logic: a framework for compatibility and specialization
Subset spaces are simple yet expressive structures consisting of a domain and a distinguished family of its subsets. In this paper, we introduce a relational semantics derived from such spaces by defining two fundamental relations: compatibility and specialization. The resulting triple, called a concord structure, captures the interplay between shared membership and refinement. The two concepts naturally arise in various fields including social network analysis, epistemic logic, and formal concept analysis. concord structures unify key ideas across these fields and provide a general modal semantics for reasoning about compatibility and specialization. We provide representation theorems for various classes of concord structures and their strict variant, and then develop sound and complete modal logics for them. Furthermore, we show that belief and conditional belief operators from evidence models and plausibility models can be expressed within modal logic for concord structures. Moreover, the compatibility modality captures a distinct epistemic notion: collateral refutation, where a claim is refuted whenever the current world is. This yields a new perspective on negative epistemic commitment.
17:10-17:30
Open Discussion