模态逻辑GL的基于广义谢弗竖的分析性模态公理系统（英文）

基于广义谢弗竖这种新算子,本文构造了模态逻辑GL的模态表列和分析性模态公理系统。广义谢弗竖是一种n元算子,为模态逻辑的表达式提供一种新记法,使分析性模态公理系统的陈述直接明了。由于谢弗竖是一种新算子,基于它的模态表列规则与通常的基于模态词和联结词的表列规则有所不同。分析性模态公理系统中的内定理证明很简单。因为分析性模态公理系统与模态表列之间存在某种对应关系,所以GL的分析性模态公理系统的完全性由GL的模态表列的完全性结果易证。GL的模态系统的完全性证明比较特殊,无法直接应用证明模态逻辑完全性的一般方法——典范模型方法,需要用一种过滤的方法挑出一些可能世界构造有穷模型。     

系统Z中的范式和插入定理

系统Ｚ是我在文［１］中建立的的经典命题逻辑的一个公理系统。这系统只用一种初始联结词──广义析舍,而且采用括号记法,因而使得系统的陈述更为直接明了。它的可判定性、可靠性、完全性和独立性等证明也都很简单。系统Ｚ是很有独特之处的,分离规则和双重否定规则在其中都不成立。本文将继续这方面的工作。首先,我们提出一种析舍范式,并阐明它跟合取范式和析取范式的联系。其次,我们陈述并证明插入定理。通常插入定理的证明很少或几乎没有直接以公理系统为基础进行的,而我们的证明则是施归纳于系统Ｚ中证明的长度进行的,这是系统Ｚ…     

哥德尔的直觉主义逻辑思想

哥德尔（Kurt Godel）是现代逻辑史上的巨匠，他在逻辑史上有两大贡献：一是他证明了罗素和怀特海在《数学原理》中提出的一阶逻辑演算的完全性定理（1930），即任何有效的一阶公式都是可证的。二是他证明了著名的不完全性定理（1931），《数学原理》的系统和集合论的ZF公理系统不足以判定能在这些系统中形式化的所有数学问题...     

一个与卢卡西维兹不同的亚里士多德三段论形式系统

30多年前,波兰数学家、逻辑学家卢卡西维兹首次用现代逻辑的方法对亚氏三段论进行形式化的研究,并建立了亚氏三段论的形式系统(以下简称LS)。LS使用4条公理和14个断定命题(即命题逻辑的定理)。4条公理是:     

休谟原则与弗雷格定理

弗雷格《算术的基本规律》中二阶逻辑理论FL是不一致的,在语法上可以推演出罗素悖论,在语义上,矛盾于康托尔定理,进而是不可满足的。通过仔细考察弗雷格的逻辑系统FL、FL的子系统FA以及算术还原为逻辑的推理过程,可以看出弗雷格在用公理五与概念的数的显定义推演出休谟原则后,不再实质依赖于公理五与概念的数的显定义。休谟原则与带完整二阶存在概括规则的二阶逻辑组成的系统FA是一致的,并且足以推出戴德金皮亚诺系统的五条公理,这实质上给出了不同于皮亚诺公理系统的另外一种算术公理化系统。根据自然数的定义,弗雷格实质上利用数学归纳法证明了每个自然数都有后继存在,加上后继的唯一性,弗雷格就保证了无穷多的自然数的存在。     

分支时空结构上的时空逻辑（英文）

Belnap通过在分支时间结构上添加空间关系,提出了更一般化的分支时空结构。在本文中,我们首次为这种分支时空结构建立相应的逻辑系统。在该逻辑中,我们引入一个空间模态算子来表达模型中的空间关系。我们给出该逻辑的公理系统,并证明它的完备性。     

弗雷格《概念记号》研究

近年来，弗雷格研究的一个突破性成果是发现了弗雷格定理：用Ｈｕｍｅ原理取代弗雷格的公理Ｖ＊，把它作为唯一的非逻辑公理加入到《概念记号》的二阶逻辑中可得到一个一致的系统；应用《概念记号》的序列理论来定义自然数，便可在上述系统中证明Ｐｅａｎｏ关于自然数的五个公设。弗雷格定理的发现促使人们重新审视弗雷格的著作，《概念记号》便是焦点之一。本文回答四个问题：１．弗雷格在《概念记号》中要解决什么具体问题？２．他所说的“语言的逻辑缺陷”究竟是什么？３．有什么证据把《概念记号》的量词理论归于二阶逻辑？４．序列的纯…     

不可超越的无穷：关于直谓性和后继公理的关系

本文首先将新弗雷格主义的发展划分为三个阶段：（1）弗雷格算术（由二阶逻辑和休谟原则构成的理论）的一致性和对于二阶皮亚诺算术公理的可推出性的证明,（2）对休谟原则和二阶逻辑的哲学辩护与反驳,（3）对休谟原则和二阶逻辑进行限制,并证明其一致性和可推出性。然后着重介绍：（1）直谓二阶逻辑和公理V的一致性,（2）直谓二阶逻辑和休谟原则不能推出皮亚诺算术的后继公理。这说明一致性和可推出性在弗雷格系统的直谓片段中不可兼得。最后在直观上做出简单的分析。     

从形式系统的整体性看法规

形式系统的整体性一般包括公理独立性、一致性和完全性,另外还有层次性的问题。独立性是指各公理间的不可推演性;一致性是指它们会不会导致矛盾的性质;完全性是指系统内的公理加推演规则能否演绎出系统内的所有定理的性质;层次性则要求系统层次分明,由分层本身不导致悖论。 一个意义完整的法规与形式系统有着本质的不同。首先,法规无所谓公理;其次,法规中不仅仅有陈述句,更多的是规范句;再者,法规条文使用容易产生歧义的自然语言,远不     

弗雷格的《算术基本规律》

弗雷格被看作是分析哲学的奠基人和数理逻辑的创始人,然而,他的毕生工作都致力于建立一种被称为逻辑主义的数学哲学。他在《算术基本规律》一书中给出了执行逻辑主义方案的形式系统。然而,由于罗素悖论的发现,很少有人关注弗雷格的《算术基本规律》。本文将主要介绍《算术基本规律》一书,包括其符号系统的说明,公理、规则、定义和定理的说明,罗素发现的悖论以及弗雷格的补救措施。     

From Wittgenstein’s N-operator to a New Notation for Some Decidable Modal Logics

Wittgenstein’s N-operator is a ‘primitive sign’ which shows every complex proposition is the result of the truth-functional combination of a finite number of component propositions, and thus provides a mechanical method to determine logical truth. The N-operator can be interpreted as a generalized Sheffer stroke. In this paper, I introduce a new ‘primitive sign’ that is a hybrid of generalized Sheffer stroke and modality, and give a uniform expression for modal formulas. The general form of modal formula in the new notation is [A₀···A_n?1; B₀···B_m?1], which is semantically equivalent to ¬A₀∨···∨¬ A_n?1∨? (¬B₀∨···∨¬B_m?1). Based on this new notation, I propose several analytic axiomatic systems for some decidable modal logics. Every axiom of these analytic systems is an ‘Atomic-Sheffer’, which is the result of the combination of a finite number of component propositions. The inferential rules are analytic in that the set of elementary propositions that are combined in the premiss overlaps the set of elementary propositions combined in the conclusion, in virtue of which every complex proposition can be reduced to an ‘Atomic-Sheffer’ at the ultimate level. The analytic modal systems have the same classical inferential rules. Different modal systems can be built by adding special modal inferential rules. In an analytic system for modal logic L, valid formulas on L-models can be proved by a purely mechanical method.     

Uniform Interpolation and Propositional Quantifiers in Modal Logics

We investigate uniform interpolants in propositional modal logics from the proof-theoretical point of view. Our approach is adopted from Pitts’ proof of uniform interpolationin intuitionistic propositional logic [15]. The method is based on a simulation of certain quantifiers ranging over propositional variables and uses a terminating sequent calculus for which structural rules are admissible. We shall present such a proof of the uniform interpolation theorem for normal modal logics K and T. It provides an explicit algorithm constructing the interpolants. Presented by Heinrich Wansing     

Sequent-systems and groupoid models. I

The purpose of this paper is to connect the proof theory and the model theory of a family of propositional logics weaker than Heyting's. This family includes systems analogous to the Lambek calculus of syntactic categories, systems of relevant logic, systems related toBCK algebras, and, finally, Johansson's and Heyting's logic. First, sequent-systems are given for these logics, and cut-elimination results are proved. In these sequent-systems the rules for the logical operations are never changed: all changes are made in the structural rules. Next, Hubert-style formulations are given for these logics, and algebraic completeness results are demonstrated with respect to residuated lattice-ordered groupoids. Finally, model structures related to relevant model structures (of Urquhart, Fine, Routley, Meyer, and Maksimova) are given for our logics. These model structures are based on groupoids parallel to the sequent-systems. This paper lays the ground for a kind of correspondence theory for axioms of logics with implication weaker than Heyting's, a correspondence theory analogous to the correspondence theory for modal axioms of normal modal logics.The first part of the paper, which follows, contains the first two sections, which deal with sequent-systems and Hubert-formulations. The second part, due to appear in the next issue of this journal, will contain the third section, which deals with groupoid models.     

Preservation of Craig interpolation by the product of matrix logics

The product of matrix logics, possibly with additional interaction axioms, is shown to preserve a slightly relaxed notion of Craig interpolation. The result is established symbolically, capitalizing on the complete axiomatization of the product of matrix logics provided by their meet-combination. Along the way preservation of the metatheorem of deduction is also proved. The computation of the interpolant in the resulting logic is proved to be polynomially reducible to the computation of the interpolants in the two given logics. Illustrations are provided for classical, intuitionistic and modal propositional logics.     

Deontic action logic, atomic boolean algebras and fault-tolerance

We introduce a deontic action logic and its axiomatization. This logic has some useful properties (soundness, completeness, compactness and decidability), extending the properties usually associated with such logics. Though the propositional version of the logic is quite expressive, we augment it with temporal operators, and we outline an axiomatic system for this more expressive framework. An important characteristic of this deontic action logic is that we use boolean combinators on actions, and, because of finiteness restrictions, the generated boolean algebra is atomic, which is a crucial point in proving the completeness of the axiomatic system. As our main goal is to use this logic for reasoning about fault-tolerant systems, we provide a complete example of a simple application, with an attempt at formalization of some concepts usually associated with fault-tolerance.     

Proof-Theoretic Functional Completeness for the Hybrid Logics of Everywhere and Elsewhere

A hybrid logic is obtained by adding to an ordinary modal logic further expressive power in the form of a second sort of propositional symbols called nominals and by adding so-called satisfaction operators. In this paper we consider hybridized versions of S5 (“the logic of everywhere”) and the modal logic of inequality (“the logic of elsewhere”). We give natural deduction systems for the logics and we prove functional completeness results.     

Implicit connectives of algebraizable logics

An extensions by new axioms and rules of an algebraizable logic in the sense of Blok and Pigozzi is not necessarily algebraizable if it involves new connective symbols, or it may be algebraizable in an essentially different way than the original logic. However, extension whose axioms and rules define implicitly the new connectives are algebraizable, via the same equivalence formulas and defining equations of the original logic, by enriched algebras of its equivalente quasivariety semantics. For certain strongly algebraizable logics, all connectives defined implicitly by axiomatic extensions of the logic are explicitly definable.Special issue of Studia Logica: Algebraic Theory of Quasivarieties Presented by M. E. Adams, K. V. Adaricheva, W. Dziobiak, and A. V. Kravchenko     

Arrow Logic and Infinite Counting

We consider arrow logics (i.e., propositional multi-modal logics having three -- a dyadic, a monadic, and a constant -- modal operators) augmented with various kinds of infinite counting modalities, such as 'much more', 'of good quantity', 'many times'. It is shown that the addition of these modal operators to weakly associative arrow logic results in finitely axiomatizable and decidable logics, which fail to have the finite base property.     

Expressive Power and Incompleteness of Propositional Logics

Natural deduction systems were motivated by the desire to define the meaning of each connective by specifying how it is introduced and eliminated from inference. In one sense, this attempt fails, for it is well known that propositional logic rules (however formulated) underdetermine the classical truth tables. Natural deduction rules are too weak to enforce the intended readings of the connectives; they allow non-standard models. Two reactions to this phenomenon appear in the literature. One is to try to restore the standard readings, for example by adopting sequent rules with multiple conclusions. Another is to explore what readings the natural deduction rules do enforce. When the notion of a model of a rule is generalized, it is found that natural deduction rules express “intuitionistic” readings of their connectives. A third approach is presented here. The intuitionistic readings emerge when models of rules are defined globally, but the notion of a local model of a rule is also natural. Using this benchmark, natural deduction rules enforce exactly the classical readings of the connectives, while this is not true of axiomatic systems. This vindicates the historical motivation for natural deduction rules. One odd consequence of using the local model benchmark is that some systems of propositional logic are not complete for the semantics that their rules express. Parallels are drawn with incompleteness results in modal logic to help make sense of this.