To promote interdisciplinary interaction between different faculty members and students on the campus, a weekly meeting has been organized by our postdoc Jialiang Yan since September 2023, called Tsing Ch’a Sessions (清茶会). Its slogan “know thyself and let others know you better.”
■Schedule for 2024-2025 academic year (Spring)
| Date | Speaker |
|---|---|
| 2025 Feb 27 | Sisi Yang (Tsinghua University) |
| 2025 Mar 20 | Wenfei Ouyang (Tsinghua University) |
| 2025 Mar 27 | Xi Yang (Tsinghua University) |
| 2025 Apr 24 | Haoxuan Luo (Tsinghua University) |
| 2025 May 08 | Xin Li (Tsinghua University) |
| 2025 May 22 | Yumin Ji (Tsinghua University) |
| 2025 May 29 | Weijun Yu (Tsinghua University) |
| 2025 Jun 05 | Ke Wu (China University of Political science and Law) |
| 2025 Jun 12 | Rui Zhu (University of Auckland) |
■Current Sessions
2025 Jun 12 14:00-15:30 Rui Zhu (祝瑞, University of Auckland) How to Handle Arbitrary Announcement Operators: Completeness and Model Transformation in Social Announcement Logic
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.
任意宣告算子是一种对所有可能的宣告语句进行量化的动态算子，用于表达在任意可被宣告的信息下，某公式是否成立。该算子的引入极大增强了社交宣告逻辑（Social Announcement Logic，SAL）在刻画信息传播过程中的表达能力，但也带来了新的形式化挑战，尤其是在推理规则的可靠性以及逻辑系统的有限公理化方面。本研究提出了一种模型变换技术，证明了涉及任意宣告算子的关键推理规则的可靠性。在此基础上，我们得以采用标准的亨金构造方法，为包含任意宣告算子的SAL建立一个弱完备性的有穷公理系统。最后，我们讨论了该技术在处理高阶信念与网络结构动态推理等复杂情境中的应用潜力。本报告基于作者已被LORI 2025接收的论文
2025 Jun 05 Ke Wu (吴可，China University of Political Science and Law)
The Convergence and Convergence Speed of Threshold Models in Social Networks
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
2025 May 29 14:00-15:30 Weijun Yu (余伟俊，Tsinghua University) Knowledge in early Chinese thought by Donald Sturgeon
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 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.
2025 May 22 14:00-15:30 Yumin Ji (池幽旻，Tsinghua University) Channels: From Logic to Probability — A Review of Jeremy Seligman’s Article
This talk reviews Jeremy Seligman’s article “Channels: From Logic to Probability,” which explores information flow through the Barwise–Seligman framework—an abstract model of channels originally developed to formalize logical information flow. Building on this foundation, the framework is extended to incorporate probabilistic notions of information, drawing insightful parallels between logical and probabilistic paradigms.
The presentation begins by introducing the foundational concepts of the Barwise–Seligman framework—classifications, infomorphisms, and channels—situating them within both logical and probabilistic contexts. I then turn to Dretske’s account of information flow, formalizing it using Shannon channels and comparing it with its logic-based counterpart, the Tarski channel. Three central conceptual challenges—the Strength Problem, the Modality Problem, and the Context Problem—are addressed through the introduction of a structural parameter known as a link.
Next, I examine how links arise from different types of theories: logic-based (Tarski theories), probability-based (Dretske theories), and a more general class that encompasses both, termed Gentzen theories. The talk concludes by connecting these theoretical constructions to situation semantics, demonstrating that Gentzen theories correspond to certain Barwise-style models. The result is a unified abstract framework that integrates logical and probabilistic accounts of information.
References：
- Seligman, J. (2008). Channels: From logic to probability. In G. Sommaruga (Ed.), Formal theories of information (pp. 193–215). Springer.
- Dretske, F. (1981). Knowledge and the flow of information. MIT Press.
2025 May 08 16:00-17:30 Xin Li （李鑫, Tsinghua University) An exponential lower bound of proof complexity for substructural logics
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.
Jalali, Raheleh. “Proof complexity of substructural logics.” Annals of Pure and Applied Logic 172.7 (2021): 102972.
2025 Apr 24 14:00-15:30 Haoxuan Luo (罗昊轩 Tsinghua University) An Epistemic Logic for Formalizing Correlations
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.
2025 Mar 27 14:00-15:30 Xi Yang (杨曦 Tsinghua University) Data exchange and structural characterizations
Data exchange is the problem of transforming data between databases with different schemas. Schema mappings are specifications that describe the rules for data exchange. They are typically expressed in a logical formalism, often a restricted fragment of first-order or second-order logic, chosen for its desirable structural properties.To say that a particular schema mapping language is characterized by certain structural properties means that a schema mapping has these properties if and only if it can be expressed in that language. In ten Cate and Kolaitis (2009), the authors studied structural characterizations of schema mapping languages such as global-as-view (GAV) dependencies and local-as-view (LAV) dependencies.In this talk, I will introduce the basic concepts of data exchange and schema mappings, with a focus on the structural characterizations established in the works of ten Cate and Kolaitis. If time permits, I will sketch my idea for a structural characterization of nested tuple-generating dependencies (nested TGDs), a problem that remains open.
1. Balder ten Cate and Phokion G. Kolaitis. 2009. Structural characterizations of schema-mapping languages. In Proceedings of the International Conference on Database Theory. 63–72.
2025 Mar 20 14:00-15:30 Wenfei Ouyang (欧阳文飞 Tsinghua University) Representation Theorem in Disjunctive Dependence
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.
2025 Feb 27 14:00-15:30 Sisi Yang (杨思思 Tsinghua University) Axiomatization problem of Temporal STIT Logic
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, aimed at constructing a general STIT frame.
Reference：
- [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.
■Past Sessions
Click HERE to check the past sessions.
