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

We are focusing on Plato’s method of diairesis. This is a method for discovering definitions of concepts that he developed in a series of dialogues, including Phaedrus, Sophist, Statesman, and Philebus. Interestingly, Gregory Cherlin points out that Saharon Shelah’s strategy for dividing lines in contemporary model theory is a mathematical version of Plato’s “cutting through the middle.” John T. Baldwin puts this more specifically: a dividing line is a property that must be both a “virtuous property” and its negation. In this talk, we will focus on more fundamental philosophical questions: Why do dividing lines exist? How can a philosopher or mathematician be sure that a dividing line has been discovered? The requirements for candidate dividing lines proposed by Shelah and the strategy of using the “test problem” parallel various actual methods of dividing in Plato’s dialogues. In essence, these requirements and strategies are actually intended to ensure that Plato’s requirement in the Sophist is to divide according to Form, that is, objective concepts as we understand them.

About the speaker: 

The talk begins with a brief introduction to Gärdenfors’s framework of conceptual spaces, in which concepts are modelled as regions in spaces built from quality dimensions. I then show how I use this framework to model the concept of natural number as a combination of several such spaces. I take the concept of natural number to be componential, distributed across at least four domains: the Approximate Number System (ANS), subitising, progression-regularity, and the symbolic system of numerals. Next, I focus on how the conceptual space of the ANS contributes to the conceptual space of the mature and professional concept of natural number. I use the model of the ANS to discuss concept learning. In particular, I explore the back-and-forth interactions between cognitive representations and cultural theoretical constructions (systems of notation, arithmetics, theories of computation) to understand how humans link the representations issuing from the ANS and other core cognition systems to the exact number words and numerals of their culture. Research funded with a Polish National Research Center grant OPUS21.

About the speaker: 

The talk is about simplicial semantics of modal predicate logic introduced in the 1990s by Dmitry Skvortsov. Although this semantics is not widely known, it is quite useful. Many logics that are incomplete in the standard Kripke semantics become complete in simplicial semantics, and an analogue of Sahlqvist theorem holds here. Another recent application is in the study of 1-variable fragments and expanding products of modal logics. In the talk we will state the corresponding results and briefly explain the methods of proofs.

About the speaker: Valentin Shehtman works as a principal scientist at the Higher School of Modern Mathematics, Moscow Institute of Physics and Technology. He is also a Professor at Higher School of Economics and Moscow State University teaching different courses in mathematical logic. V. Shehtman is one of the leading specialists in nonclassical logic. He is an author of a research monograph “Quantifcation in nonclassical logic” (with D.Gabbay, D. Skvortsov) and about 50 papers. He solved several important and difficult problems in the field. His research is basically in modal logic and related areas, such as intuitionistic logic, algebraic logic, categorial logic; with the emphasis in model-theoretic and combinatorial methods.

What is the relationship between thought and language? Both unfold as structured, sequential processes. In this talk, I will address this question through a study using the classic arcade game Pac-Man. We analyzed how humans and macaques played the game using a hierarchical model—the Language of Problem Solving—that represents gameplay as abstract strategies organized into structured, hierarchical sequences. Our analyses reveal that both species exhibit a “grammar” of problem solving, but at markedly different levels of complexity: macaques rely primarily on simple grammatical structures, whereas expert humans construct complex strategic “sentences” to navigate dynamic environments. Using fMRI, we linked this capacity in humans to a right-lateralized brain network that closely mirrors the left hemisphere’s language network. These findings suggest that thought and language rely on similar computational principles for organizing structured sequences. More broadly, they point to a prefrontal–parietal–temporal circuit for structured sequence computation, of which language may be a specialized function.

About the speaker: Tianming Yang, PhD, is Senior Investigator and Head of the Laboratory of Neural Mechanisms of Decision Making and Cognition at the Institute of Neuroscience, Center for Excellence in Brain Science and Intelligence Technology, Chinese Academy of Sciences. His laboratory investigates how neural circuits in the primate brain support complex decision making and higher cognition, combining behavioral paradigms in macaque monkeys and humans with electrophysiology, computational modeling, and artificial neural networks. Dr. Yang received his PhD in Neuroscience from Baylor College of Medicine in 2003 and completed postdoctoral training at the University of Washington  (2003-2008). He then served as a staff scientist at the U.S. National Institute of Mental Health (2008-2013), before establishing his own laboratory at the Institute of Neuroscience in 2013. Dr. Yang’s research has elucidated the neural mechanisms underlying probabilistic reasoning and decision-making within extended prefrontal and parietal networks. His work also explores how these computational principles can be modeled and applied to the development of artificial intelligence.

Concurrent game models are a standard semantic framework for logics of strategic reasoning. Many influential logics in this area are interpreted over concurrent game models, including Alternating-time Temporal Logic (ATL), introduced by Alur et al. (2002), which is a key framework for reasoning about strategic and coalitional ability. Roughly speaking, a concurrent game model consists of states and agents (forming coalitions), where, at each state, every coalition has available joint actions, and each such action induces a set of possible outcome states.

Li and Ju (2025, 2026) argued that standard concurrent game models rely on three assumptions that can be too strong in practice. The first is seriality: coalitions always have available joint actions. The second is the independence of agents: merging two available joint actions of two disjoint coalitions always yields an available joint action of their union. The third is determinism: joint actions of the grand coalition always have a unique outcome. 

There are eight classes of generalized concurrent game models, obtained by selectively imposing seriality, independence of agents, and determinism. In this talk, I will present eight generalized alternating-time temporal logics, each based on one of these eight classes of models.

We provide four semantics for these logics, based respectively on positional strategies, historical strategies, positional co-strategies, and historical co-strategies. We give fixed-point characterizations of the “globally” and “until” operators and show that all four semantics are equivalent. We also provide axiomatic systems for the eight logics and prove their soundness and completeness.

If time permits, I will also discuss some potential applications of generalized alternating-time temporal logics.

This talk is based on the following joint work with Yinfeng Li (University of Toulouse), Thomas Ågotnes (University of Bergen and Shanxi University), and Emiliano Lorini (University of Toulouse):

  • Fengkui Ju, Thomas Ågotnes, Yinfeng Li, and Emiliano Lorini. “Generalized alternating-time temporal logics II: Axiomatization.” Submitted, 2026.

  • Fengkui Ju, Thomas Ågotnes, Yinfeng Li, and Emiliano Lorini. “Generalized alternating-time temporal logics I: Semantics.” Information and Computation, Volume 310, 2026.

  • Yinfeng Li and Fengkui Ju. “Completeness of coalition logics with seriality, independence of agents, or determinism.” Journal of Logic, Language, and Information, 2026.

  • Yinfeng Li and Fengkui Ju. “A minimal coalition logic.” Journal of Logic and Computation, Volume 35, Issue 8, 2025.

About the speaker: 琚凤魁，北京师范大学哲学学院逻辑学专业教授，研究领域包括：关于agency的逻辑，尤其是关于联盟能力的逻辑；道义逻辑和法律推理；自然语言（模态词、条件句、祈使句等）的语义及相关逻辑。

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