直觉主义数学对逻辑联接词和量词的解释依赖于“构造性”等不精确的概念,因而不是严格构造性的,这不同于形式可证性概念。哥德尔想尝试用严格构造性的证明概念来代替,他希望实现一种放宽条件的希尔伯特纲领,构造同时具有直觉主义的构造性特征和有穷主义特点的形式可证性逻辑。可证性逻辑为困扰已久的自指概念提供了新的研究工具,另外,可证性研究了数学上许多重要的结论(如哥德尔第二不完全性定理)。沿着哥德尔的思想,后来的逻辑学家也作了很多相关研究,阿提莫夫的证明逻辑是比较有代表性的研究成果。本文就主要对可证性逻辑发展史进行研究,全文由四章构成。第一章:直觉主义逻辑BHK的解释。本章首先介绍了直觉主义流派的主要思想,并将直觉主义逻辑与经典逻辑的不同点进行分析;然后描述了直觉主义命题逻辑和一阶谓词逻辑系统,并在此基础上得出直觉主义逻辑BHK的解释。第二章:哥德尔的可证性逻辑。本章首先介绍了哥德尔的主要理论成果,以了解哥德尔可证性逻辑的历史背景;然后具体分析哥德尔的可证性逻辑系统,它克服了直觉主义数学的非构造性特点,是介于直觉主义数学与古典数学之间的逻辑系统。第三章:Logic of proofs。可证性(Provability)研究的两个新方向:一个是由S.Artemov在1994年发起的loqic of proofs(这是受到基础关系以及给直觉主义逻辑提供强有力的可证性语义问题的鼓舞);另一个是graded provability algebras,旨在为可证性逻辑在主流的证明理论传统中建立联系和寻找应用。本章主要介绍了S.Artemov对可证性逻辑的研究成果。第四章:可证性逻辑的历史梳理。本章主要对可证性逻辑发展的历史脉络进行梳理。