基于构造性思想的直觉主义逻辑证明语义

Proof Semantics Based on Mental Construction for Intuitionistic Logic

布劳威尔的直觉主义把数学理解为心智的构造性活动,只接受心智可构造的数学对象和数学证明。在直觉主义看来,判定一个命题为真必须要给出这个命题的构造性证明,对逻辑联结词及量词的理解也是基于构造性立场的。本文构建了直觉主义逻辑的证明语义,这是一种内涵语义,其特点是:遵循构造性思想、尽量贴近直观、避免使用集合概念,语义解释从具体命题、具体对象(个体)、具体性质和关系等出发,使具体命题成为“公式解释”和“直观有效”概念的基础。进而在这种语义下证明了直觉主义命题逻辑和谓词逻辑的可靠性。

In Brouwer’s intuitionism,he regards mathematics as activities of mental construction.In his opinion,one only admits mathematical objects and proofs which can be constructed in our mind.From an intuitionistic point of view,when we assert that a proposition is true,we have to offer a constructive proof for this proposition.Therefore,the meaning of basic propositional connectives and quantifiers is based on construction.This paper builds proof semantics for intuitionistic logic.The proof semantics are a kind of intentional semantics.The features of the proof semantics include following constructivism,trying to preserve our intuitions,avoiding using the conception of sets to construct our semantics.In proof semantics we give semantical interpretations on the basis of concrete propositions,concrete objects(individuals)and concrete properties and relations and so on.Furthermore,the conceptions of“interpretations for formulas”and“intuitive validity”are defined based on concrete propositions.We give proofs for soundness theorems of intuitionistic propositional and predicate logics based on our semantics.