Rui Zhu / Ray
Research areas: dynamic epistemic logic, social announcement logic, arbitrary announcements, justification logic, and the early history of modal logic.
My recent work focuses on social announcement logic with arbitrary announcement operators. I use model-transformational methods to obtain finitary axiomatizations and to prove soundness and completeness results for these systems. I am also interested in extending social announcement logic toward applications, especially in modelling how information flows through social networks and in describing network structure within a logical language. For this reason, axiomatizing these logics, developing tableau systems, and analysing their decidability are central parts of my current research. I have also worked on justification logic and hybrid logic, and I maintain a continuing interest in the early history of modal logic, especially the long-overlooked contributions of Chinese logicians such as Shen Yuting.
祝瑞 / Ray
研究领域：动态认知逻辑、社交宣告逻辑、任意宣告、核证逻辑，以及早期模态逻辑史。
我近期的主要工作是用模型变换方法研究带有任意宣告算子的社交宣告逻辑，建立其有穷公理系统，并证明相应系统的可靠性与完全性。 我也希望把社交宣告逻辑进一步推广到应用场景中，尤其是用它模拟信息在社交网络中的流动，并用逻辑语言刻画社交网络结构。 因此，对这些逻辑进行公理化、建立表列式系统并分析其可判定性，是我目前最核心的研究方向。 此外，我也曾研究核证逻辑与混合逻辑，并持续关注早期模态逻辑史，尤其是沈有鼎等中国逻辑学家长期被忽视的贡献。
Research
Contributions and current directionsSocial Announcement Logic and arbitrary announcements
I work on logics for belief diffusion in social networks. Building on the logic of network announcements developed in Towards a Logic of Tweeting, my recent work gives a finitary proof system for arbitrary sincere announcements. This solves an open problem left by earlier infinitary treatments of arbitrary announcement operators in the social-network setting.
Method. The key technical idea is a two-stage model transformation: first normalizing models with respect to fresh propositional names, then extending belief states so that a required witness message can be embedded into the model. I regard this as a portable method for other logics with arbitrary operators, including fragments of arbitrary public announcement logic.Tableaux, Proof Theory, and Decidability
I am developing tableau calculi for social announcement logic. This work provides the first tableau system for social announcement logic, simplifies the proof-theoretic treatment of the logic, and separates out the finite-representative problem behind arbitrary sincere announcements. In this way, it offers a clearer technical route toward decidability.
Plan: I plan to prove decidability for social announcement logic with arbitrary operators, and then extend the same strategy to Boolean arbitrary public announcement logic and related dynamic epistemic logics with arbitrary modalities.Justification Logic, Names, and Possible Worlds
During my master's study, I worked on justification logic with names. The main result of this work is that internalization can still be proved without adding the reflexivity axiom. This answers a question left by Fitting and leads to soundness and completeness for the corresponding minimal system.
Plan: Fitting once encouraged me to continue this line of research. I have also considered using justification logic with names in dynamic epistemic logic. Another open task is to give a genuinely constructive proof of the realization theorem for this logic. Overall, Fitting's system has strong expressive power and promising applications.History of logic and early modal logic
I reconstruct overlooked contributions of Chinese logicians to the formation of modern modal logic. My current paper argues that Shen Yuting was the first to prove, syntactically, that Lewis's System B plus axioms 4 and B entails axiom 5, thereby correcting Oskar Becker's claim that these principles generate an independent ten-modality calculus.
Project. This is part of a larger project on Chinese philosophers and logicians in early modal logic, including Shen Youqian, Shen Yuting, Tang Zaozhen, Jin Yuelin, Christine Ladd-Franklin, C. I. Lewis, and the transnational networks through which symbolic logic travelled.研究方向
主要贡献与当前计划社交宣告逻辑与任意宣告
这个计划研究社交网络中的信念扩散逻辑。在 Towards a Logic of Tweeting 所建立的网络宣告逻辑基础上，我进一步研究带有任意真诚宣告算子的社交宣告逻辑，并给出了有穷证明系统。这解决了之前留下的有穷公理化问题。
主要方法： 核心技术是两阶段模型变换——先把模型关于新命题变元正规化，再扩展主体的信念状态，使所需的 witness message 能够嵌入模型语义。这一方法有较强的可迁移性，也可以用于任意公开宣告逻辑及其他带任意算子的逻辑片段。表列式系统、证明论与可判定性
我正在发展社交宣告逻辑的表列式演算。该工作给出了第一个社交宣告逻辑的表列式系统，简化了该逻辑的证明论处理， 并把任意真诚宣告背后的“有限代表”问题明确分离出来，从而为可判定性证明提供了更清晰的技术路径。
计划： 我计划进一步证明带任意算子的社交宣告逻辑的可判定性，并把相关方法扩展到布尔任意公开宣告逻辑等带有任意算子的动态认知逻辑中。核证逻辑、名字与可能世界
我在硕士期间研究带名字的核证逻辑。该工作的核心结果是：即使不加入自反性公理，也可以证明相应系统的内在化定理， 从而回答 Fitting 当年留下的问题，并进一步得到最小系统的可靠性与完全性。
计划： Fitting 曾期待我继续推进这一方向。我后来也曾考虑把这种带名字的核证逻辑用于动态认知逻辑。 另外，该逻辑的 realization theorem 仍缺少一个真正构造性的证明。总体而言，Fitting 的这一系统表达力很强，仍有相当好的应用前景。逻辑史与早期模态逻辑
我正在重构中国逻辑学家在现代模态逻辑形成期被忽视的贡献。当前论文指出，沈有鼎是第一个以纯句法方式证明 Lewis 系统 B 加公理 4 与公理 B 蕴含公理 5 的人，由此纠正了 Oskar Becker 所谓“十模态演算”的误判。
计划： 我在考虑进行一个名为“中国逻辑学家在早期模态逻辑中的贡献”的研究，涉及沈有乾、沈有鼎、汤藻真、金岳霖、Christine Ladd-Franklin、C. I. Lewis、William. T. Parry 以及现代符号逻辑的发展。Selected Publications
Representative work, with brief context- 2026
A Finitary Axiomatization of Arbitrary Social Announcement Logic
This paper presents the core finitary system for arbitrary sincere announcements in social networks. Its main contribution is the model-transformation method that makes the discharge rule for arbitrary announcements sound without relying on an infinitary proof system.
-
2025
Arbitrary Announcements in Social Networks: A Finitary Proof System
This journal article studies social announcement logic with both arbitrary announcement operators and free announcement operators. The free announcement operator substantially increases the expressive power of the language and makes it possible to describe social-network structure in a systematic way. The axiom system and the completeness proof are quite different from those in my other work on arbitrary social announcement logic. The paper also shows that social announcement logic is not merely a simple fragment of public announcement logic, but a dynamic epistemic logic with its own structural features.
-
2017
Towards a Logic of Tweeting
This paper is the starting point of my work on social announcement logic. Led by Dr Zuojun Xiong, it formalizes one-to-many communication in social networks as a logical system and gives a sound and complete axiomatization of the minimal logic of tweeting. Later work on social announcement logic, free announcement logic, and arbitrary social announcement logic can be seen as further developments of this basic framework.
- 2015
The Minimal System of Justification Logic with Names
The paper studies names in justification logic and shows that internalization can be proved without adding the reflexivity axiom, answering a problem left open by Fitting.
- 2026
Shen Yuting in Early Modal Logic: The Axiom Interdependence of S5
This paper reconstructs Shen Yuting's syntactic proof that System B + 4 + B entails 5, showing that Shen corrected Becker's ten-modality claim and helped stabilize the S4/S5 hierarchy before model-theoretic semantics became standard.
代表性论著
代表性成果及简要说明- 2026
A Finitary Axiomatization of Arbitrary Social Announcement Logic
这篇论文给出了社交网络中任意真诚宣告的核心有穷证明系统。主要贡献是模型变换方法：它使任意宣告的 discharge rule 得到可靠性证明，而不需要诉诸无穷规则系统。
-
2025
Arbitrary Announcements in Social Networks: A Finitary Proof System
这篇期刊论文研究带有任意宣告算子与自由宣告算子的社交宣告逻辑。自由宣告算子显著增强了语言的表达力， 使我们能够更系统地刻画社交网络结构。论文给出的公理系统及其完全性证明，与我关于任意社交宣告逻辑的另一项工作有明显不同； 它也说明，社交宣告逻辑并不是公开宣告逻辑的简单片段，而是具有自身结构特征的动态认知逻辑。
-
2017
Towards a Logic of Tweeting
这是社交宣告逻辑工作的起点。该论文由熊作军博士主导，把社交网络中的一对多传播形式化为逻辑系统，并给出了 minimal logic of tweeting 的可靠与完全公理化。后来的社交宣告逻辑、自由宣告逻辑和任意社交宣告逻辑，都可以看作是在这一基本框架上的进一步发展。
- 2015
The Minimal System of Justification Logic with Names
该文研究带名字的核证逻辑，并证明不加入自反性公理也可以得到内在化定理，从而回答 Fitting 留下的问题。
- 2026
Shen Yuting in Early Modal Logic: The Axiom Interdependence of S5
该文重构沈有鼎关于 System B + 4 + B 蕴含 5 的纯句法证明，说明沈有鼎纠正了 Becker 的十模态误判，并在现代语义学形成前为 S4/S5 层级的稳定化作出关键贡献。
Selected Recent Talks
2024–2026, with themes- Apr 2026
Shen Yuting and Early Modal Logic
Presented the historical thesis that Shen Yuting was the first to derive axiom 5 from axioms 4 and B in Lewis's System B, and explained why this matters for the later S4/S5 hierarchy.
- Dec 2025
Arbitrary Social Announcement Logic
Explained the finitary axiomatization of arbitrary social announcements and the model transformation technique behind the proof.
- Dec 2025
Shen Yuting and S5 Interdependence
Introduced Shen Yuting's contribution to an international audience and situated it alongside Becker, Wajsberg, Parry, Lewis, and the later semantic tradition.
- Nov 2025
Tableau System of Social Announcement Logic
Reported the first tableau system for Social Announcement Logic and discussed how tableau rules can simplify proof search and support decidability analysis.
- Oct 2025
A Finitary Axiomatization of Social Announcement Logic
Presented the LORI paper on a finitary axiomatization of arbitrary social announcement logic, focusing on the open problem and its proof-theoretic resolution.
- Jun 2025
How to Handle Arbitrary Announcement Operators
Discussed how arbitrary announcement operators can be handled by model transformation rather than by relying only on infinitary rules or necessity-form machinery.
- Nov 2024
Free Social Announcement Logic
Presented the free-announcement fragment as a clean entry point to the broader family of social announcement logics.
近期学术报告
2024–2026，附主题说明- 2026年4月
Shen Yuting and Early Modal Logic
报告沈有鼎最早在 Lewis 系统 B 中从公理 4 与公理 B 推出公理 5 的历史与逻辑意义，并说明这一结果为何关系到后来 S4/S5 层级的稳定化。
- 2025年12月
Arbitrary Social Announcement Logic
介绍任意社交宣告逻辑的有穷公理化，尤其是可靠性证明的模型变换方法。
- 2025年12月
Shen Yuting and S5 Interdependence
面向国际听众介绍沈有鼎的贡献，并将其放在 Becker、Wajsberg、Parry、Lewis 以及后来的语义学传统中理解。
- 2025年11月
Tableau System of Social Announcement Logic
报告社交宣告逻辑的第一个表列式系统，并讨论表列规则如何简化证明搜索、支持判定性分析。
- 2025年10月
A Finitary Axiomatization of Social Announcement Logic
报告 LORI 论文的核心结果：任意社交宣告逻辑的有穷公理化，以及对开放问题的证明论解决。
- 2025年6月
How to Handle Arbitrary Announcement Operators
讨论如何用模型变换处理任意宣告算子，而不是完全依赖无穷规则或 necessity form 技术。
- 2024年11月
Free Social Announcement Logic
以自由宣告片段作为切入点，展示社交宣告逻辑家族的基本结构。
Teaching
Logic, philosophy, mathematics, and programmingUniversity teaching
- Tutor, University of Auckland: PHIL 101 Introduction to Logic; PHIL 105 Critical Thinking.
- Teaching Assistant, University of Canterbury: PHIL 233 Epistemology and Metaphysics; PHIL 311 Meaning, Mind, and the Nature of Philosophy.
- Invited teaching session on belief propagation in dynamic epistemic logic, University of Auckland.
Teaching interests
- Mathematical logic, modal logic, dynamic epistemic logic, automata theory, and theory of computation.
- Logic education through interactive slides, small programs, and visual examples.
- Practical bridges between logic and programming: parsers, normal forms, minimization algorithms, and small reasoning tools.
教学
逻辑、哲学、数学与编程大学教学
- 奥克兰大学助教：PHIL 101 “Introduction to Logic”；PHIL 105 “Critical Thinking”。
- 坎特伯雷大学助教：PHIL 233 “Epistemology and Metaphysics”；PHIL 311 “Meaning, Mind, and the Nature of Philosophy”。
- 奥克兰大学研究生课程邀请教学报告：动态认知逻辑中的信念传播建模。
教学兴趣
- 数理逻辑、模态逻辑、动态认知逻辑、自动机理论与计算理论。
- 通过交互式课件、小程序和可视化例子进行逻辑教学。
- 把逻辑教学与实用编程结合起来：解析器、范式转换、最简表达式算法和小型推理工具。
Digital Work
Teaching, public scholarship, and experimentsInteractive slides
A collection of reveal.js presentations for logic, mathematics, and programming. These slides are designed to make abstract ideas such as belief update, tableaux, model transformation, and proof search easier to see and discuss in class.
Chinese Logicians and Early Modal Logic
A public-facing project on Chinese logicians' contributions to early modal logic, including Shen Yuting and related figures. It is intended both as historical scholarship and as a resource for readers outside the Chinese academic context.
GitHub projects and experiments
Code, teaching examples, and experimental materials related to logic, programming instruction, and web-based academic communication. I prefer small, transparent tools that students can inspect and modify.
Computational logic for teaching
A navigation page for small logic tools and classroom programs: formula parsers, CNF conversion, tableaux, K-map and Quine–McCluskey style minimization, social-network demos, and other executable examples that connect formal syntax with code.
数字项目
教学、公共学术与实验面向教学的计算逻辑
这是小型逻辑工具和课堂程序的导航页，包括公式解析器、CNF 转换、表列式生成器、卡诺图与 Quine–McCluskey 最简化、社交网络演示，以及把形式语法和可执行代码连接起来的示例。
Interests and Making
Beyond academiaLong-distance running
I am a full-marathon finisher with a personal best of 3:17 at the Christchurch Marathon 2018, and I have also served as a pacer for several running events. Running has shaped my life.
Drama
From 2009 to 2011, I played a leading role in the Chinese online sitcom Nansheng Nadianshi. This experience deepened my interest in drama, film, and the performing arts, and gave me a more direct sense of narrative, character-building, and public expression. During my university years, I also participated in several stage productions.
Embedded programming
I am learning C51 microcontroller programming and experimenting with voice modules such as ASRPRO2. I am interested in using embedded systems as a bridge between programming, hardware interaction, and classroom demonstrations.
Learning New Tools
I am always open to learning new tools and methods when they are useful for teaching or research: from web development and reveal.js to Lean 4, Haskell, automata theory, Boolean minimization algorithms, and small parsers for logic courses. I also follow developments in artificial intelligence. Before large language models became widely popular, I had already studied several basic machine-learning models, such as KNN, RNN, and decision trees. However, the theoretical foundations of these topics lie more in mathematical statistics and computational methods than in my main field of logic; for now, they mainly support my teaching design, technical experiments, and interdisciplinary exploration.
个人兴趣与业余活动
学术之外长跑
我多次完成全程马拉松，个人最好成绩是 2018 年 Christchurch Marathon 的 3小时17分，也多次在跑步赛事中担任配速员。长跑是我生命中无法摆脱的习惯。
戏剧
2009—2011 年间，我曾主演中文网络情景剧 男生那点事。 这段经历加深了我对戏剧、电影与表演艺术的兴趣，也让我更直接地体会到叙事、角色塑造和公共表达的重要性。 此外，我在大学期间也参与过多部舞台话剧表演。
嵌入式编程
我正在学习 C51 单片机编程，并尝试 ASRPRO2 等语音模块。我对把嵌入式系统用于编程、硬件交互和课堂演示很感兴趣。
学习新工具
只要有助于教学或研究，我一直乐于学习新的工具和方法：从网页开发、reveal.js，到 Lean 4、Haskell、自动机理论、布尔最小化算法，以及逻辑课程中的小型解析器。 我也持续关注人工智能。在大语言模型广泛流行之前，我已经学习过若干机器学习的基本模型，例如 KNN、RNN 和决策树。 不过，这些内容的理论基础更多来自数理统计和计算方法，与我的逻辑学主线保持一定距离；它们目前主要服务于我的教学设计、技术实验和跨学科探索。
Contact
Academic correspondenceEmail: zrui956@aucklanduni.ac.nz
GitHub: github.com/Raycaesar
Interactive slides: slides-6xr.pages.dev
Logic tools directory: toolkits
Chinese logicians project: cn-logicians-eml.pages.dev
CV is available on request
联系方式
学术联系GitHub：github.com/Raycaesar
交互式课件：slides
逻辑工具：toolkits
中国逻辑学家项目：cn-logicians-eml.pages.dev
如需简历可来信索取