直觉主义逻辑与程序设计语言

以下摘要由 AI 根据胶片自动生成。

布劳威尔的直觉主义数学哲学拒绝排中律，将命题的真值定义为该命题的证明，由此产生了直觉主义逻辑的自然演绎系统，其合取、析取、蕴含、永假各有对应的引入与消除规则，并通过局部归约保证逻辑系统的和谐性。Curry-Howard 同构揭示”证明即程序、命题即类型”的深层联系：蕴含对应函数类型，合取对应积类型，由此将设计直觉主义逻辑系统等价于设计带类型的编程语言。报告还介绍了直觉主义模态逻辑、线性逻辑等同构以及相继式演算、切割归约等推理方式的变体。