时间：5月10日16:00-17:40，

地点：澳门沙金在线平台新斋324

Section 1

16:00-17:00，Thomas Studer（瑞士伯尔尼大学）

Title: Common knowledge from a proof-theoretic perspective

Abstract:

To say that a proposition A is common knowledge means‘everybody knows that A’and‘everybody knows that everybody knows that A’and‘everybody knows that everybody knows that everybody knows that A’and so on. Semantically, common knowledge can easily be characterized as the least fixed point of acertain monotone operator. Proof-theoretically, this translates to either aleast fixed point rule or an induction axiom. However, how to applycut-elimination and other proof-theoretic techniques to common knowledge is not yet fully understood. In this talk we will survey the state of the art and discuss open problems about the proof theory of common knowledge.

Section 2

17:00-17:40，朱吟秋、俞珺华（澳门沙金在线平台）

Title: Diagonal /circular extensions of a sequent calculus

Abstract:

For a sequent calculus X that enjoys a rule R that principally introduces positive occurrences of a key-note operator, the diagonal extension of X is gained by substituting rule R from X by rule D, where D is just like R, but has an extra negative copy of positive principals (from its conclusion) ateach of its premises. To the contrast, the circular extension of X enjoys exactthe same axioms and rules as X, but employs instead a generalized notion of proof, called circular proof. In a circular proof, each leaf can either be a given axiom, or has a same sequent as another node on the unique path from that leaf to the root. Daniyar Shamkanov verified that the diagonal extension and the circular extension of a calculus for modal logic K4 coincide in terms of provability (both are calculi for G？del-L？b logic GL). In this talk, we will sketch our finding that this can also be achieved purely in terms of proof transformation, which also allows us to prove a parallel result for Visser's BPL, where both extensions are calculi for his FPL.

欢迎参加！