直觉主义逻辑的直观语义与形式语义

On Intuitive Semantics and Formal Semantics for Intuitionistic Logic

直觉主义逻辑的直观语义(即"证明解释")是直觉主义逻辑建立的基础,它遵循直觉主义的构造性立场,但"构造性证明"这个内涵概念依赖于人们的直观理解。直觉主义逻辑的形式语义更为精致,其中以对话语义为代表的博弈式语义和以克里普克(Kripke)语义为代表的模型论式语义具有代表性。对话语义的构建是满足直觉主义要求的,并且从博弈的角度解读了"构造性证明",它是一种满足直觉主义逻辑直观语义的形式语义。Kripke语义的构建是依赖于"实无穷"的,这是直觉主义所拒斥的;另外,"Kripke有效"利用了赋值函数来定义,这是一种外延定义,与直觉主义逻辑的直观语义有偏离。尽管如此,Kripke语义的认识论解释从认识论视角对直觉主义逻辑形式系统作了解读,为直觉主义逻辑在其他领域的应用开辟了道路,也通过逻辑作为桥梁促进了多学科的交叉研究。

Intuitionistic Logic is based on its intuitive semantics(i.e."proof interpretation").It accords with the intuitionistic requirement of constructivity,but the concept of"constructive proof"relies on our intuitive understanding.Formal semantics for intuitionistic logic are more sophisticated than intuitive semantics.They are represented for example by dialogue semantics as a typical game theoretical semantics and Kripke semantics as a typical model theoretical semantics.Dialogue semantics fulfills all requirements of intuitionism,and interprets the meaning of "constructive proof"from the game theoretic point of view,so it is a kind of formal semantics which is in line with intuitive semantics for intuitionistic logic.On the other hand Kripke semantics uses the notion of actual infinity which intuitionism rejects;moreover,"Kripke valid"is defined by assignment functions and this is a kind of extensional definition.In this it also deviates from the intuitive semantics for intuitionistic logic.Nonetheless, Kripke semantics makes a valuable contribution to interdisciplinary research,for the epistemic interpretation of Kripke semantics interprets the formal systems of intuitionistic logic from the point of view of epistemology,and thus opens up new ways for applications in other areas.