Theoretical Topics on Formal Systems
December 19, 2024, Beijing, China
Tsinghua University
- Time: 13:00-17:30, December 19, 2024
- Venue: Room 329, School of Humanities, Tsinghua University.
Program

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.

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.

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.