JRC for Logic
Tsinghua University – University of Amsterdam Joint Research Centre for Logic
JRC for Logic
Tsinghua University – University of Amsterdam Joint Research Centre for Logic

Tsinghua Logic Salon

Initiated by the center’s students and researchers in 2019, the Tsinghua Logic Salon has quickly grown into a lively platform for try-outs and exchanges of new ideas. Researchers in various fields of logic are invited to present their latest research, as well as the challenges that they see. Every participant is encouraged to engage in discussions and exchange of perspectives. Each session lasts for 1.5 hours in total, with 30 minutes of discussion included.

Organizing Committee:

Junhua Yu, Chenwei Shi, Wei Wang, Han Xiao, Haoxuan Luo. (From June 2025 to Now)

Junhua Yu, Chenwei Shi, Wei Wang, Jialiang Yan, Penghao Du. (From September 2023 to June 2025)

■ Current Events

It was shown recently by Borzechowski et al. that Propositional Dynamic Logic (PDL) has Craig Interpolation. Whether test-free PDL without the ‘?’ operator has interpolation remained open.
In this talk on ongoing work I will show that the answer is negative, with a counterexample: there is a test-free PDL validity for which no test-free interpolant exists. The validity only uses one atomic program and the Kleene star, so the result also applies to other modal logics with transitive closure operators such as common knowledge.
This result was originally obtained using LLMs and Lean and I will describe the method in the talk as well.

About the speaker: Malvin Gattinger is assistant professor in Theoretical Computer Science at the ILLC of the University of Amsterdam. He obtained his PhD as part of the Tsinghua-UvA JRC in 2018 and has been a PostDoc in Groningen before re-joining ILLC. His research interests are Modal Logic, Model Checking, Gossip Protocols, Formalization and Epistemic Planning.

The weakly Euclidean modal logic \(\mathrm{wK5} = \mathrm{K} \oplus \Diamond p \to \Box(p \lor \Diamond p)\) is determined by weakly Euclidean frames, i.e., frames satisfying the first-order condition \(\forall xyz(xRy \land xRz \to y = z \lor yRz)\). The logic \(\mathrm{wK5}\) is a proper sublogic of the Euclidean modal logic \(\mathrm{K5}\). We will show that the interval \([\mathrm{wK5}, \mathrm{K5}]\) contains a continuum of non–finitely axiomatizable logics. The logic \(\mathrm{wK5}\) has the hereditary finite model property. All finite depth logics in the lattice \(\mathrm{NExt}(\mathrm{wK5})\) are locally tabular. Finally, we show that \(\mathrm{wK5}\) has the polysize model property which yields that it has a NP–complete satisfiability problem. Moreover, all subframe logics in \(\mathrm{NExt}(\mathrm{wK5})\) have the polysize model property.

About the speaker: 马明辉，中山大学哲学系教授、博士生导师。一直研究modal logic、intuitionistic logic、De Morgan logic等逻辑理论的模型论和证明论，还对19世纪以来的逻辑发展史以及它们在哲学中产生的后果感兴趣。

While most adults tend to interpret disjunctive statements like ‘A or B’ exclusively, some children (age 3-5/6) have a conjunctive interpretation. We propose that children who interpret disjunctions conjunctively do so because they have not yet fully developed two cognitive abilities: 1. the ability to engage with models that verify sentences by virtue of an empty configuration (zero-models); and 2. the ability to process (conflicting) alternatives in a parallel fashion (split-states). In the first part of the talk I will argue against theories explaining conjunctive interpretations in terms of alternative-based reasoning and present the core of our cognitive approach. In the second part, I will propose formalisations of zero-models and split-states in a bilateral teams semantics, and show how the assumption that children cannot engage with these mental structures explains their conjunctive behaviour.
This is joint work with Tomasz Klochowicz and Giorgio Sbardolini.

About the speaker: Maria Aloni is Associate Professor at the Department of Philosophy and at Institute for Logic, Language and Computation (ILLC) of the University of Amsterdam. Her primary research interests lie in the areas of formal semantics and pragmatics, philosophical logic and philosophy of language. She is associate editor of the Journal of Semantics; and member of the editorial board of Semantics and Pragmatics. She has edited (with Paul Dekker) the Cambridge Handbook of Formal Semantics.

The system of intuitionistic logic with actuality recently proposed by Niki and Omori is arguably better suited to capture classical actuality within an intuitionistic background logic, as it proves a number of classically-flavored principles, including @φ ∨ ¬@φ, ¬¬@φ → @φ, ((@φ → ψ) → @φ) → @φ, or (@φ → ψ) ∨ (@ψ → φ). In this paper, I firstly develop an alternative system that justifies the actuality operator intuitionistically by means of an extension of the BHK explanation developed by Bentzen and Fassio to reason with actuality. The corresponding formal semantics invalidates a wide range of such classical principles. I also present an axiomatization and establish soundness and completeness. Secondly, I classify a family of intermediate intuitionistic systems between Niki and Omori’s classical and our intuitionistic actuality.

About the speaker: Bruno Bentzen is an assistant professor of philosophy at Zhejiang University. His work revolves around the philosophy of logic and mathematics, with a particular emphasis on the tradition of mathematical intuitionism and constructive type theory. He has published a number of articles in some of the most prestigious journals in logic and philosophy of mathematics (Review of Symbolic Logic, Notre Dame Journal of Formal Logic, Philosophia Mathematica, Journal of Logic and Computation, History and Philosophy of Logic, Erkenntnis, etc.) He is the author of the upcoming Springer book “Philosophical type theory” and the first author of the edited book “Logics for AI and Law” published by College Publications in 2023.

Many current hyperintensional logics with a semantics using truthmaking, ‘support’, or teams fit in a long tradition of set-lifting classical logical systems. I will add some older examples dating back to around 1980, stressing the essentially modal character of this move. Next I will discuss the mathematical framework of ‘Complex Algebra’ that lies behind set-lifting. Finally, I introduce two faithful translations of known hyperintensional logics into classical modal logics. I conclude with some discussion of the many new issues these connections raise for both kinds of logical system.

References
J. van Benthem, 2018, ‘Implicit and Explicit Stances in Logic’, Journal of Philosophical Logic, 48, 571–601. 
–, 2024, ‘Relational Patterns, Partiality, and Set Lifting in Modal Semantics’, in Y. Weiss and R. Birman, eds., Outstanding Logicians Volume Saul Kripke, Springer Science Publishers, 93–119.
M. Aloni, A. Baltag, J. van Benthem, N. Bezhanishvili & S. Knudstorp, 2026, ‘Translating BSL’, paper in progress, ILLC, University of Amsterdam.

About the speaker: Johan van Benthem is a University Professor emeritus of pure and applied logic at the University of Amsterdam, Henry Waldgrave Stuart Professor of Philosophy at Stanford University, and Jin Yuelin Professor of Logic at Tsinghua University Beijing. He has worked in modal logic, temporal logic, logical semantics and syntax of natural language, as well as dynamic logics of information, computation, and agency. He was the founding director of the ‘Institute for Logic, Language and Computation’ (ILLC) at the University of Amsterdam, and the first Chair and First Honorary Member of the European Association for Language, Logic and Information (FoLLI). His published books include “The Logic of Time” (1983), “Modal Logic and Classical Logic” (1985), “Essays in Logical Semantics” (1986), “Language in Action” (1991), and “Exploring Logical Dynamics” (1996). His current main interest is the theme of intelligent interaction, at the interface of logic, computer science, cognitive science, and game theory, with new books “Modal Logic for Open Minds” (2010), “Logical Dynamics of Information and Interaction” (2011) and “Logic in Games” (2014). Published some 400 papers. Editor of Handbooks of “Logic and Language” (1997), “Modal Logic” (2006), “Spatial Logics” (2007), and “Philosophy of Information” (2008). He is a member of the Academia Europaea (1991), the Royal Dutch Academy of Arts and Sciences (1992), Institut International de Philosophie (2001), and Hollandsche Maatschappij der Wetenschappen (2002). In addition, he is also a foreign member of the American Academy of Arts and Sciences. In 1996 he received the Dutch national NWO Spinoza Premium for his total research.

A classical result of Bergstra and Tucker states that every finitely generated computable algebra admits a finite presentation after expanding the signature with finitely many auxiliary computable operations. They also prove that every computably enumerable algebra can be embedded into a finitely presented algebra by adding new operations to the extended algebra. These results led Bergstra and Tucker, and independently Goncharov, to ask in the late 1970s whether every finitely generated computably enumerable algebra admits a finite presentation by either equations or quasi-equations in an expansion without extending the domain. The equational case of this problem was fully resolved in the 1988-2014 period. 

This work addresses the remaining case of conditional equations, i.e., quasi-equations of the form (s1=t1 ∧ … ∧ sn=tn) => s=t. Unlike equations, conditional equations are not preserved under homomorphisms, a fundamental difference that renders the methods developed for the equational case inapplicable to quasi-equations. We therefore develop a new approach and construct a finitely generated computably enumerable algebra that admits no finite presentation by conditional equations in any expansion. The proof brings together techniques from several areas: universal algebra, through the analysis of almost free algebras and their algorithmic properties; model theory, via quantifier elimination for almost free algebras; and computability theory, via a finite injury priority argument. This provides a complete solution to the Bergstra–Tucker problem and closes the final gap in the theory of finite presentations for computably enumerable finitely generated algebras.
This is a joint work with Jia Yifan and Heer Tern Kooh.

About the speaker: Bakh Khoussainov 现任电子科技大学算法与逻辑实验室主任，研究领域涵盖数理逻辑与理论计算机科学。他是新西兰皇家学会会士、欧洲科学院院士，并入选中国国家级人才计划（长江学者讲席学者）。他曾获欧洲理论计算机科学协会 Nerode 奖、洪堡奖，以及 STOC 2017 最佳论文奖。

他已指导20余名博士研究生，发表研究论文160余篇，并曾在康奈尔大学、海德堡大学、新加坡国立大学、新西伯利亚国立大学、京都大学等高校担任教授或访问教授。

 

■Past Events

Click HERE to check the past events from 2019-2024.

Click HERE to check the past events from 2024-.