逻辑研究和逻辑史的研究——与蔡曙山同志商榷

逻辑研究推理并且主要是研究推理形式。具体地说,它研究推理中从前提到结论的必然联系。过去,人们从自然语言出发研究这种必然联系,建立相应的推理形式或规则。今天,人们从构造形式语言出发,通过建立逻辑演算来研究从前提到结论的必然联系。逻辑演算是形式系统,是把逻辑理论形式化的结果。今天人们熟悉并且经常使用的一阶逻辑就包括把命题逻辑形式化而建立的命题演算系统和把谓词逻辑形式化而建立的谓词演算系统。     

中外两种主要推理模型的实验再比较研究

本研究采用2X2两因素(自变量分别为“心理模型数量”和不同“内容性质”)重复测量拉丁方实验方法,在范畴三段论推理题的内在结构为“形式正确”,且“推理者已经掌握相应的形式逻辑推理规则”的前提条件下,对西方学者提出的“心理模型”与中国学者提出的“推理题和推理者的推理知识双重结构模型”这两种理论模型再次进行了实验比较研究。结果表明,对于“正确形式—正确内容”和“正确形式—错误内容”两种不同结构的推理题,若按照形式逻辑规则来判定推理者“对各推理题的结论能否从两个前提中推论出来的推论结果”是否正确,则有:(1)当推理题含有错误内容的情况下,即使该推理题只是由“一个心理模型”所构成,也会使推理者降低对其结论判定为“正确”的可能性;(2)当推理题是由正确内容所构成时,即使该推理题是由三个心理模型所构成,对其结论判定为“正确”的可能性也要比“单模型——错误内容”构成的推理题的可能性更高。由此得到的比较结论是:在本实验条件下,“推理题和推理者的推理知识双重结构模型”对实验结果所做的解释要比“心理模型”理论所做的解释更为贴切。     

谈谈自然推理

自然推理系统是二十世纪三十年代首先被波兰逻辑学家C·雅斯科夫斯基和德国的逻辑学家G·根森分别提出的。在自然推理系统中,出发点并不是公理,而是随时引进的假设前提,从这些假设前提出发,应用推理规则或推理图式,就能有效的达到推理目的。由于这种推理方法类似于自然科学尤其数学中常用的那种证明程序(如定律,定理的证明)。因此,把它称为自然推理或自然演算。为了了解自然推理的实质及特点,我们必须对构成自然推理系统的推理部分,即推理规则及推理所依据的推理图式作一简单介绍。(由于篇幅所限其它部分不在此介绍了)。     

Braine心理逻辑理论述评

该文对Braine提出的在推理心理学研究领域占居重要地位的“心理逻辑理论”做了综合述评。“心理逻辑理论”主要包括三方面内容:构成“心理逻辑理论”基础的一组推理规则图式、将推理规则图式应用于推理过程的推理方案、实际应用意义。Braine认为他和他的同事于1984年设计并实施的以“自然推理系统”所含各推理规则为实验材料的实验结果支持该理论的基本观点。     

Rips的“证明心理学理论”述评

该文对Rips提出的“证明心理学理论”做了综合述评。这一理论主要包含三方面的内容:对推理过程与人类记忆相互关系的解释;(2)根据逻辑学中的“自然推理规则”进行修正后用于解释人类推理过程的推理规则;(3)关于如何控制推理过程的论述。Rips认为他于1983年设计并实施的以“自然推理系统”所含各推理规则为实验材料的实验结果支持该理论的基本观点。     

中外两种推理理论的实验比较研究

通过两个实验对中国学者提出的“推理题与推理者的推理知识双重结构模型”和Evans提出的“双重加工理论”进行了实验比较研究。实验一通过两种评定方法对相应性质命题进行评定后所得实验结果表明Evans等(1983)有关“信念效应”研究中的“结论可信性”变量可以视为与胡竹菁等(1996)实验中的“内容正确性”变量是同一性质的变量; 实验二根据“形式正确性”和“内容正确性”两个自变量设计的推理实验结果与Evans等(1983)的研究结果基本一致; 但增加“内容熟悉性”这一自变量设计的推理实验结果表明“推理题与推理者的推理知识双重结构模型”比Evans提出的“双重加工理论”能更好地解释推理者对性质三段论的推理结果。     

孔子人道思想的结构

孔子是儒学思想体系的奠基人,而不是周文化的全盘接受者,其所以“从周”,与他追求有序化的最高理想有关。我们所理解的周文化很多是孔子及其后学整理的结果,“子不语”正是孔子“从周”前提下进行思想转换的一种方式。在孔子的社会学的功能体系中,并没有什么核心概念。君子人格系统、作为文化价值的仁学系统与社会结构和规则构成的礼学系统三者互相规定、互为条件,它们都是自身处于不停转换过程中的具有时间性和历史性的子系统,共同构成一个更广泛的均衡有序的文明结构。     

《句法结构》要略

乔姆斯基的《句法结构》是对美国传统的描写语言学的一场革命,其革命性首先表现在乔姆斯基站在理性主义的立场上反对描写语言学的经验主义。他把语言学看成跟自然科学中的其他科学一样,可以从假设出发,进行推演并形式化。换句话说,非经验主义是可能的。《句法结构》有一半篇幅用于英语语法的形式化。非经验主义和形式化是转换生成语法的首要标志。把句法关系作为语言结构的中心并以此说明语句的生成是这场革命的又一表现。为了描写和解释语言现象,乔姆斯基在《句法结构》中论证了语法的生成能力,认为应该把语法看成是能生成无限句子的有限规则系统。它以“核心句”为基础,通过转换规则描写和分析不同句式之间的内在联系。该书分析了以“马尔可夫过程”为基础的通讯理论,认为它只能生成有限状态的语法,而这种“有限状态的语法”不能生成象英语这种语言里含有不连续结构的所有合乎语法的句子。基于此,乔姆斯基提出了转换语法模式,认为它才能生成所有合乎语法的句子而不会生成不舍乎语法的句子。转换语法模式由短语结构规则、转换规则、语素音位规则三套规则构成。短语结构规则有三种：合并、递归、推导式,其基本形式是x→y。→读作“改写”,这个公式就是将X改写成Y。短语结构规则生成的是“核心语符列”,不经过转换直接由这种语符列得出的基本句型叫“核心句”。转换规则包括：移位、删略、添加。最后运用语素音位规则得出实际说出的句子。这三套规则中,最引人注目的是转换规则,因为短语结构规则和语素音位规则实际上继承了描写语言学的“直接成分分析”和语素音位的分析．转换是一种创新,它使语法具有更强的解释力。《句法结构》是转换生成语法第一阶段—?     

规则顺序与规则类型对儿童规则推理的影响

学前儿童时期是各种推理能力产生和发展的重要时期。本研究采用Frye和Zelazo等（1996）所设计的“二进二出”装置,设置了规则顺序、规则类型的规则推理任务,采用个别实验法,研究了90名3～4岁儿童规则推理能力的发展。在本研究条件下,结果发现：1．当规则呈现顺序不同时,儿童规则推理成绩差异显著,先呈现哪个规则,则利用这个规则进行推理的成绩就较好;2．不同规则类型下儿童的推理成绩差异极其显著,竖直规则下的推理任务更容易;3．3．5～4岁是儿童二维合取规则推理能力发展的快速期。     

"命题推理"的心理学研究综述

本文在对“如果…,那么…”规则、“四卡问题”和“THOG”等三种有关“命题推理”领域的研究作了简要综述。     

Gentzen-Style Axiomatizations for Some Conservative Extensions of Basic Propositional Logic

We introduce two Gentzen-style sequent calculus axiomatizations for conservative extensions of basic propositional logic. Our first axiomatization is an ipmrovement of, in the sense that it has a kind of the subformula property and is a slight modification of. In this system the cut rule is eliminated. The second axiomatization is a classical conservative extension of basic propositional logic. Using these axiomatizations, we prove interpolation theorems for basic propositional logic.     

Game Semantics for the Lambek-Calculus: Capturing Directionality and the Absence of Structural Rules

In this paper, we propose a game semantics for the (associative) Lambek calculus. Compared to the implicational fragment of intuitionistic propositional calculus, the semantics deals with two features of the logic: absence of structural rules, as well as directionality of implication. We investigate the impact of these variations of the logic on its game semantics. Presented by Wojciech Buszkowski     

Relational Semantics of the Lambek Calculus Extended with Classical Propositional Logic

We show that the relational semantics of the Lambek calculus, both nonassociative and associative, is also sound and complete for its extension with classical propositional logic. Then, using filtrations, we obtain the finite model property for the nonassociative Lambek calculus extended with classical propositional logic.     

Substructural Implicational Logics Including the Relevant Logic E

We introduce several restricted versions of the structural rules in the implicational fragment of Gentzen's sequent calculus LJ. For example, we permit the applications of a structural rule only if its principal formula is an implication. We investigate cut-eliminability and theorem-equivalence among various combinations of them. The results include new cut-elimination theorems for the implicational fragments of the following logics: relevant logic E, strict implication S4, and their neighbors (e.g., E-W and S4-W); BCI-logic, BCK-logic, relevant logic R, and the intuitionistic logic. This revised version was published online in June 2006 with corrections to the Cover Date.     

A Contraction-free and Cut-free Sequent Calculus for Propositional Dynamic Logic

In this paper we present a sequent calculus for propositional dynamic logic built using an enriched version of the tree-hypersequent method and including an infinitary rule for the iteration operator. We prove that this sequent calculus is theoremwise equivalent to the corresponding Hilbert-style system, and that it is contraction-free and cut-free. All results are proved in a purely syntactic way.     

弱逻辑F的矢列演算

本文建立起弱逻辑F的G3-型矢列演算G3F,并证明弱化规则、收缩规则和切割规则在G3F中是可容许的。此外,本文还运用证明论的方法给出一个通过哥德尔–麦金西–塔斯基翻译将G3F嵌入到G3K的新证明。     

The Problem of Foundation in Early Nyāya and in Navya-Nyāya

The evaluation of arguments was not the sole concern of logicians in ancient India. Early Nyāya and the later Navya-Nyāya provide an interesting example of the interaction between logic and ontology. In their attempt to develop a kind of property-location logic (Navya-)Naiyāyikas had to consider what kind of restrictions they should impose on the residence relation between a property and its locus (which might again be a property). Can we admit circular residence relations or infinitely descending chains of properties, each depending on its successor as its locus? Early Naiyāyikas and to some extent also Navya-Naiyāyikas regard these phenomena as a kind of absurdity and they want to rule them out. Their intuitions about properties are close to well-founded systems of set theory, whereas the author of the Navya-Nyāya work Upādhidarpa?a is a proponent of a non-well-founded property concept. Despite certain similarities with sets properties are still regarded as intensional objects in Navya-Nyāya. In the present article I demonstrate that a Quine/Morse-style extension of George Bealer's property calculus T1 (with or without a property adaptation of the axiom of regularity) may serve as a formal system which adequately mirrors the Navya-Nyāya property-location logic.     

Does the deduction theorem fail for modal logic?

Various sources in the literature claim that the deduction theorem does not hold for normal modal or epistemic logic, whereas others present versions of the deduction theorem for several normal modal systems. It is shown here that the apparent problem arises from an objectionable notion of derivability from assumptions in an axiomatic system. When a traditional Hilbert-type system of axiomatic logic is generalized into a system for derivations from assumptions, the necessitation rule has to be modified in a way that restricts its use to cases in which the premiss does not depend on assumptions. This restriction is entirely analogous to the restriction of the rule of universal generalization of first-order logic. A necessitation rule with this restriction permits a proof of the deduction theorem in its usual formulation. Other suggestions presented in the literature to deal with the problem are reviewed, and the present solution is argued to be preferable to the other alternatives. A contraction- and cut-free sequent calculus equivalent to the Hilbert system for basic modal logic shows the standard failure argument untenable by proving the underivability of ${\square\,A}$ from A.     

Varieties of Linear Calculi

A uniform calculus for linear logic is presented. The calculus has the form of a natural deduction system in sequent calculus style with general introduction and elimination rules. General elimination rules are motivated through an inversion principle, the dual form of which gives the general introduction rules. By restricting all the rules to their single-succedent versions, a uniform calculus for intuitionistic linear logic is obtained. The calculus encompasses both natural deduction and sequent calculus that are obtained as special instances from the uniform calculus. Other instances give all the invertibilities and partial invertibilities for the sequent calculus rules of linear logic. The calculus is normalizing and satisfies the subformula property for normal derivations.     

Interpreting HOL in the calculus of constructions

The purpose of this paper is to consider a representation of the HOL theorem-prover in the calculus of constructions with the property that consistency results from the calculus of constructions imply such results in HOL. This kind of representation is impossible using the propositions-as-types representation of logic and equality, but it is possible if a different representation is used.