Tsinghua University – University of Amsterdam Joint Research Centre for Logic

Tsing Ch’a Past Session from 2025

Sessions in 2026-2027 Spring Semester

2026 June 11 14:00-15:30 Haoxuan Luo (罗昊轩, Tsinghua University) General Fitting Models Based on Term Functions

Unlike modal logic, which uses \box\phi to express that \phi is known or necessary, justification logic uses t: \phi to express that t is a reason or proof for \phi. This talk focuses on term functions, which specify what each justification term can justify.

I will first introduce the basic language, axiomatic calculus, and two semantic models: Mkrtychev models (M-models) and Fitting models (F-models). In my work, I will present a global logic for a set of term functions and a local logic for one fixed term function. Finally, I will discuss the global-local equivalence theorem and the strong completeness result.

2026 May 28 16:00-17:30 Weijun Yu (余伟俊, Tsinghua University) The Logic of Shuo Zai in the Mohist Canons

 

 

The Mohists attached great importance to shuo 說 (“explanation”) and proposed the principle of “using explanations to bring out reasons” (以說出故). In the Mohist Canons, especially the Jingxia (Canon B), the sentence structure shuo zai 說在 + X appears frequently and may be regarded as a linguistic manifestation of this principle.

This talk begins with a brief comparison between shuo (“explanation”) and a group of related concepts—argument, justification, and proof—and then examines the function and grammar of shuo and shuo zai in Mohism. The presentation focuses on a systematic classification of the semantic types of the shuo zai structure and examines how it relates to core Mohist concepts such as lei 類(“kind”), gu 故(“reason/cause”), and li 理(“principle”).

2026 May 14 14:00-15:30 Yumin Ji (池幽旻, Tsinghua University) Language, Logic, and Cognition: Generics, Medvedev Logic, and Learning via limited instances

 

 

Generics are sentences that express generalizations while tolerating exceptions, as in “Birds fly” or “Sharks attack people.” Despite their ubiquity in everyday language, the cognitive mechanisms underlying their use remain unclear. This question has attracted attention across several disciplines, particularly linguistics, logic, and cognitive science. This talk is situated at the intersection of these three fields.

The talk begins with a brief overview of the historical development of research on generics in linguistics, followed by a cross-linguistic analysis identifying three central notions associated with generics: typicality, diagnosticity, and naturalness. I then introduce Gärdenfors’s theory of conceptual spaces [Gärdenfors 2000, 2014], which aims to model how humans learn, structure, and organize concepts. Building on this framework, I propose a modification that allows a more flexible representation of concept formation and aligns with an instance-based view of learning. The three key notions associated to generics are then formally represented within the revised framework. I also present an intriguing relationship between the modified framework and Medvedev logic, an intermediate logic that is not finitely axiomatizable. Finally, I examine whether the proposed formalization aligns with empirical findings from cognitive science.

References

[Gärdenfors 2000] Gärdenfors, P. (2000). Conceptual Spaces: The Geometry of Thought. MIT Press, Cambridge, MA.

[Gärdenfors 2014] Gärdenfors, P. (2014). The Geometry of Meaning: Semantics Based on Conceptual Spaces. MIT Press, Cambridge, MA.

2026 Apr 9 14:00-15:30 Wenlong Zheng (郑文龙, Tsinghua University) Nonmonotonicity and Actual Causation: The Theory of Bochman’s Causal Calculus

 

 

Causality is a fundamental concept in reasoning, yet capturing its exact formal semantics has historically posed a challenge for standard deductive systems. In his 2021 book A Logical Theory of Causality, Alexander Bochman develops a causal calculus based on rules of the form A\Rightarrow B  (“A causes B”), situated within a nonmonotonic reasoning framework. By treating causal rules as default assumptions, we will see how causal reasoning emerges as a special instance of nonmonotonic reasoning developed within the knowledge representation and symbolic branches of artificial intelligence.

In this talk, we will first introduce the basic techniques of Bochman’s causal calculus. Second, we will briefly contrast this rule-based logical framework with the standard structural equation modeling (SEM) approach. Finally, the main focus of the talk will be applying this calculus to formalize actual causation.

2026 Feb 26 14:00-15:30 Haoxuan Yin (尹昊萱, University of Oxford) Modal Logic as a Type System for Metaprogramming

 

 

Metaprogramming languages allow programmers to construct, manipulate and run code. In the presence of imperative features, ensuring program safety is challenging, as free variables can be passed around in references. In this talk, I present Layered Modal ML (LMML), a metaprogramming language that supports storing and running open code under a strong type safety guarantee. The type system utilises contextual modal types (Hu & Pientka, ESOP 2024) to track and reason about free variables in code explicitly. A contextual modal type \Box(\Gamma\vdash T) reads “a piece of code of type T with free variables \Gamma.” If time permits, I will also talk about using operational game semantics to model program equivalences in LMML, and how this tool can be used to verify faithfulness in metaprogramming-based program optimisations.

This is joint work with Andrzej Murawski and Luke Ong. The full version of the paper can be found at https://arxiv.org/abs/2602.03033. The talk will not suppose any prior knowledge of programming language theory, but familiarity with statically typed programming languages such as C++ or Java would be helpful.

Sessions in 2025-2026 Fall Semester

 

DateSpeaker
2025 Nov 6Qian Chen 陈谦 (Tsinghua University)
2025 Nov 20Xi Yang 杨曦 (Tsinghua University) [Logic Reading Program]
2025 Dec 11 Weijun Yu 余伟俊 (Tsinghua University)
2025 Dec 12Xi Yang 杨曦 (Tsinghua University) [Logic Reading Program]
2025 Dec 26Xin Li 李鑫 (Tsinghua University) [Logic Reading Program]
2026 Jan 6Xin Li 李鑫 (Tsinghua University) [Logic Reading Program]

Abstract:

In his Philosophical Investigations, Wittgenstein distinguishes between seeing and seeing-as, arguing that in seeing we do not merely receive perceptual input but interpret the object under different aspects. Inspired by this distinction, Michael Beaney develops the notion of knowing-as, which differs from knowing-that and knowing-how, concerning the aspects in which something is known. Knowing-as is structurally ambiguous: the expression “I know X as Y” may mean “I know X-as-Y,” or “I-as-Y know X.” These two structures correspond respectively to aspectual knowledge and perspectival knowledge. In this talk, I will focus on Mohist epistemology and logic to analyze the concept of knowing-as. First, I will review Wittgenstein’s distinction of seeing/seeing-as and Beaney’s theory of knowing-as, comparing with the parallel analogy of seeing and knowing in Mohist Canon, to establish a bridge between seeing-as and knowing-as. Second, I will discuss the two senses of knowing-as in Mohist philosophy: I will relate knowing-as to Mohist concept leiqu類取(‘selecting according to kind’) and compare Mohist and Zhuangzian perspectival epistemology. Finally, since knowing-as is also closely connected to analogical reasoning, which is seen as the central feature of Chinese logic, I will quote Beaney’s logical interpretations of the Happy Fish Dialogue and argue that Mohists have a theory of analogical justification.

Tense logics are normal bi-modal logics with ‘future-looking’ and ‘past-looking’ modalities. The degree of Kripke-incompleteness of a logic L in some lattice C of logics is the cardinality of logics in C which share the same class of Kripke-frames with L. A celebrated result on Kripke-incompleteness is Blok’s dichotomy theorem for the degree of Kripke-incompleteness in the lattice NExt(K) of all normal modal logics: every normal modal logic L is of the degree of Kripke-incompleteness 1 or continuum. In this talk, we focus on the lattice NExt(K4t) of all normal extensions of K4t, where K4t is the tense logic of transitive frames. We show that Blok’s theorem of the degree of Kripke-incompleteness for modal logic K can be extended to K4t.

Sessions in 2025-2026 Spring Semester

The integration of temporal reasoning with agency—the formalization of how agents make choices over time—is a foundational area of study in philosophy and logic. Temporal logic and STIT (Seeing to It That) logic have been well-established separately, with complete axiomatizations existing for both systems. Temporal STIT (TSTIT) logic combines temporal operators with STIT operators to model agency over time. While there has been some prior work on the axiomatization of TSTIT logic, existing results are limited to specific classes of STIT frames, leaving the general axiomatization problem open. In this talk, we will focus on the axiomatization of TSTIT logic with temporal operators X, F, and the STIT operator for a single agent, interpreted over discrete time and bundled trees. Specifically, we will explore a transformation method involving bundled trees and Ockhamist frames, which aims at constructing a general STIT frame.

This is a joint work with Zhang Yan.

References:
[Belnap et al.(2001)] Nuel Belnap, Michael Perloff, and Ming Xu. 2001. Facing the future: agents and choices in our indeterminist world. Oxford University Press. 
[Ciuni and Zanardo(2010)] Roberto Ciuni and Alberto Zanardo. 2010. Completeness of a branching-time logic with possible choices. Studia Logica 96 (2010), 393–420. 
[Ciuni and Lorini(2018)] Roberto Ciuni and Emiliano Lorini. 2018. Comparing semantics for temporal STIT logic. Logique et Analyse 243 (2018), 299–339.

Disjunctive dependence is an interesting variant of functional dependency, which is used to express dependency like “x functionally determines y or z”. In this talk, I will discuss representation theorem for disjunctive dependence in dependence models and present some negative and positive results on it.

When faced with complex epistemic-combinatorial situations, agents struggle to formally differentiate between relational patterns, creating gaps in formal models.

To address this, we introduce strictly relevant operators and construct an Epistemic Logic based on Possible Knowledge Bases (EL_{PKB}). Among these, these new operators require not only the absence of counterexample situations but also every truth cases must exist, ensuring a precise representation.

To this end, we introduce a non-Kripke model that incorporates PKBs to define the semantics. In this context, a PKB refers to the knowledge combinations that an agent might possess in a given state. Then we explore the correspondence between PKBs under different definitions and the cognitive properties of agents.

In the end, we try to provide sequent calculus for this logic.

This is a report of this paper: Jalali, Raheleh. “Proof complexity of substructural logics.” Annals of Pure and Applied Logic 172.7 (2021): 102972.

One of the most important aims of proof complexity is proving lower bounds on proof size for tautological formulae in various proof systems. Aside from the extensive study of some well-known classical proof systems, recently there have been some investigations into the complexity of proofs in non-classical logics. In R. Jalali (2021), the author investigates the proof complexity of a wide range of substructural systems and concludes that for any proof system P at least as strong as Full Lambek calculus and polynomially simulated by the extended Frege system for some superintuitionistic logic of infinite branching, there is an exponential lower bound on the proof lengths.
In this talk, I will first present a simple example of resolution system and show how proof complexity system works. Then I will introduce Jalali’s work: construct hard tautologies to show the existence of an exponential lower bound on the lengths of proofs in proof systems and on the number of proof lines for a wide range of substructural logics.

Donald Sturgeon’s Ph.D thesis is an inquiry of the epistemology in early China. In this thesis, he argues that in early Chinese thought, some key concepts from the Western tradition of philosophy—such as truth and belief—did not play a particularly important role in understanding knowledge. Meanwhile, action and the capacity for correct action constitute the core elements of the Chinese conception of knowledge, forming a stark contrast with the JTB-like account of knowledge that excludes the factor of action.

In this talk, I will introduce the three main chapters of his thesis. The thesis first discusses the problem of knowledge acquisition. In early China, people agreed that knowledge derives on one hand from the heart-mind (心) and sensory organs, and on the other hand from practical training or cultivation leading. However, philosophers had fundamental disagreements about what ultimately determines what counts as knowledge. Secondly, knowledge was generally conceived as systematically correct action, and thus linguistic knowledge is the correct use of language. Language plays a crucial role in expressing and transmitting knowledge, and can therefore guide action to make it conform to the correct dao. This key function depends on objective standards for language use, but the standards was challenged by skepticism. The thesis finally discusses Zhuangzi’s skepticism and argues that his skepticism to some extent improved our epistemic position.

References

1. Donald Sturgeon, 2014. Knowledge in Early Chinese Thought. Ph.D Thesis, University of Hong Kong.

This talk presents a theoretical and computational study of belief dynamics in social networks using a threshold automaton model. We disprove the universal stability conjecture of belief convergence proposed by Liu et al. (2014), demonstrating instead that original formulation of the conjecture is exclusively achieved in finite, strongly connected networks. Our analysis establishes complete convergence conditions, generalizes stability criteria that extend beyond the original conjecture, and reveals that oscillating networks are equivalent to bipartite networks. The results provides a strict upper bound of time required for network stability, and by combining the six degrees of separation theory, it can be concluded that under this model, all humanity will stabilize in an extremely short time. These findings are further corroborated through experimental validation via simulation studies.

References

1. Liu, F., Seligman, J. & Girard, P. Logical dynamics of belief change in the community. Synthese 191, 2403–2431 (2014). https://doi.org/10.1007/s11229-014-0432-3

Arbitrary announcement operators are dynamic modalities that quantify over all possible messages that can be announced. They enable the expression of whether a given formula remains valid under any such announcement, thereby significantly enhancing the expressive power of Social Announcement Logic (SAL) in modeling information flow. However, incorporating such operators presents major formal challenges, particularly in proving the soundness of inference rules and establishing finitary completeness. In this work, we introduce a model transformation technique that provides a soundness proof for key inference rules involving arbitrary announcements. Based on this result, we construct a finitary axiomatization of SAL and prove its weak completeness using a standard Henkin-style method. We conclude by discussing the potential application of this technique to more complex scenarios, including reasoning about higher-order beliefs and dynamic changes in network structure. This talk is based on a paper accepted for presentation at LORI 2025.