(Image : Bruno’s talk in group meeting)
Toward a Mechanization of a Classical Proof of Completeness for Intuitionistic Logic.
关于直觉逻辑完全性证明的一种经典机制
Date : 21 March 2022 (15:30-16:30)
Venue : Room 307, Meng Mingwei Building, Zijingang Campus, Zhejiang University (ZLAIRE Lab)
Abstract : Standard Henkin-style completeness proofs are founded on a contrapositive reasoning that allows us to show that Γ ⊭ p by assuming that Γ ⊬ p. The basic proof step is the extension of Γ∪{¬p} to a maximal consistent set. However, constructively, it is not possible to show that Γ∪{¬p} is consistent from the assumption that Γ ⊬ p. In intuitionistic logic, in particular, a set of premisses Γ that does not prove p may happen to prove ¬¬p (and thus be consistent with p). In this talk, I discuss ways to circumvent this limitation and work in progress toward a formalization of a modified Henkin completeness proof for intuitionistic logic using the proof assistant Lean.
主讲人简介：浙江大学哲学学院“百人计划”研究员。2019年于中山大学取得逻辑学博士，曾先后担任捷克科学院哲学研究所博士后研究员和美国卡内基梅隆大学哲学系博士后研究员，2021年11月正式入职浙江大学哲学学院。专业研究领域为数理哲学、哲学逻辑、逻辑学，尤其对围绕数学建构主义的主题特别关注，专注于直觉主义和类型论之间的联系。同时，也对种类论在使用证明助手的数学形式化应用有所研究。