在线期刊

类型-逻辑语法与逻辑形式系统的深刻联系

作者:张秋成

关键字:类型逻辑语法

摘要/Abstract

本文通过论述类型-逻辑语法与逻辑形式系统的深刻联系,揭示了该理论以逻辑推理为基础的主要特色。这主要体现在两个方面:其一是类型-逻辑语法与相干逻辑、线形逻辑等逻辑系统同属于所谓的子结构逻辑;其二是依据柯里―霍华德同构定理,类型-逻辑语法中的两种运算――句法范畴运算和λ-词项运算,都与直觉主义命题逻辑证明是同态对应关系。

By discussing the deep connection between Type-Logical Grammar (shortened as TLG) and logical systems, this paper reveals the deduction-based characteristic of TLG. There are two manifestations of this connection: (1) Like relevance logic, linear logic, etc., TLG also belongs to substructural logics; (2) According to the Curry-Howard isomorphism, the two computations in TLG, those of syntactic categories and -terms, are all homomorphic to the proofs in intuitionistic implicational logic.

版权声明:社科网的所有在线期刊内容均由各期刊编辑部根据协议提供。 任何个人、机构、网站如未经本网书面授权,私自复制或转载本网中的图片、文字,均将被视为侵权行为。此类行为一经发现,本网将依据《中国人民共和国版权法》和《互联网管理条例》,追究侵权者的责任。