$\omega$ $\aleph$ $\infty$
Mathematical Logic at Fudan

Fudan Logic Student Seminar 2024

November 8

Speaker: 姜乐怀 JIANG, Lehuai

Time: 13:30 - 15:10. Location: HGW2403.

Argumentation framework with attitude classification: a new approach to handle controversial arguments, self-contradictory arguments and attack loops.

Although Dung’s theory has become the de facto standard in the field of argumentation-based inference, a problem noted by scholars is that a pair of controversial arguments might belong to the same extension under Dung’s four semantics, leading to their unexpected simultaneous acceptance. To address the shortcomings of Dung’s semantics in handling controversial arguments, the primary approach is to modify some basic concepts within his theory to propose new semantics, with the most representative work being prudent semantics proposed by Coste-Marquis and others. Nonetheless, these new semantics treat controversial arguments in a singular manner, failing to effectively address the various complex situations they entail. In this report, we claim that the attitudes between arguments are crucial in addressing controversial arguments, and argumentation framework with attitude classification (AAF) can adeptly navigate the complexities involved. Additionally, such a framework can be used to tackle issues related to self-contradictory arguments and attack loops.

October 18

Speaker: 宋书浩 SONG, Shuhao

Time: 13:30 - 15:10. Location: HGW2403.

Formalization of ZF set theory and modal logic in Lean

My graduate thesis focuses on the formalization of ZF set theory, particularly concerning large cardinals beyond choice, such as Reinhardt and Berkeley cardinals. I will discuss some details about my formalization plan.

Inspired by Zhang Zhiqing, I finished the formalization of Gödel's ontological proof in Lean. With a trick of typeclass synthesizing, so that Kripke's semantics can be easily formalized in Lean, and all pre-existing tactics can be used. Some modification to the typeclass synthesizing process in Lean was done to finish this formalization, and in this talk I will present them. Slides

September 6

Speaker: 鞠大恒 JU, Daheng

Time: 13:30 - 15:10. Location: HGW2403.

A new kind of anti-foundation axioms

In non-well-founded set theory, the canonical way to construct anti-foundation axioms is to use regular bisimulations, and the well-known axioms FAFA, SAFA and AFA are all induced by regular bisimulations. In this talk, we study the "sufficient and necessary condition" for a regular graph relation to induce a relatively consistent anti-foundation axiom, and construct a new kind of anti-foundation axioms which cannot be induced by regular bisimulations.