时间：2024年12月19日13:00-17:30
地点：清华大学逻辑学研究中心（蒙民伟人文楼 329）
议程
Rick Sommer
(Stanford University, USA)
Topic: Iterating reflection, fast growing functions, and transfinite induction
Time: 13:00-14:20
Abstract: In the context of subsystems and extensions of Peano Arithmetic (PA), this talk will explore connections between consistency, computational power, and generalizations of induction axioms. In particular, we begin with a base theory, such as Primitive Recursive Arithmetic (PRA) or Elementary Function Arithmetic (EFA), and we consider hierarchies generated from the base theory in three different ways: (1) extending theories via transfinite iterations of consistency or reflection principles, (2) adding statements of totality of fast-growing functions obtained by transfinite recursion, and (3) including axioms of transfinite induction for recursive ordinals. We will see that these three hierarchies align in surprising ways. This talk will describe the model-theoretic approach used to obtain these results, demonstrating the techniques of model-theoretic ordinal analysis, a powerful tool for measuring the proof-theoretic strength of theories of arithmetic and analysis.
Han Gao 高晗
(Aix-Marseille University & CNRS, France)
Topic: Proof-search and counter-model construction for intuitionistic modal logics
Time: 14:30-15:50
Abstract: Intuitionistic modal logic as a branch of non-classical logic enjoys a history tracing back to 1940s. In the development since then, two main traditions have emerged, one called intuitionistic modal logic and the other constructive modal logic. These two traditions are motivated by meta-logical properties and applications in computer science respectively. In this talk, we will first give a brief introduction to the general development of the field of intuitionistic modal logic, then introduce FIK, an intuitionistic modal logic specified by Kripke models satisfying the condition of forward confluence. We give a complete Hilbert-style axiom system of this logic and propose a bi-nested calculus for it. The calculus provides a decision procedure as well as a counter-model extraction: from any failed derivation of a given formula, we obtain by the calculus a finite counter-model of it directly. We also show how to restrict the level of nesting and then obtain a 1-level nested, label-free sequent calculus for FIK, which enjoys cut-elimination and shall have good complexity bound for the decision problem. Lastly, we mention some follow-up works and perspectives in the related field.
Zhe Lin 林哲
(Xiamen University, China)
Topic: Quasi Boolean algebras with operators and their applications
Time: 16:00-17:20
Abstract: This paper studies a family of many-valued modal logics based on the Belnap-Dunn logic. The decidability of the consequence relations is shown for them via strong finite model property proofs. Furthermore, we consider the application of these logics in the domain of formal argumentation, focusing in particular on frameworks that account for context shifts and the evolution of information.
关注我们，及时获取更多关于清华-阿姆斯特丹逻辑学联合研究中心的研究成果、科研教学活动、前沿问题研究进展及其他相关资讯。
