Gentzen-Type Methods for Bilattice Negation

A general Gentzen-style framework for handling both bilattice (or strong) negation and usual negation is introduced based on the characterization of negation by a modal-like operator. This framework is regarded as an extension, generalization or re- finement of not only bilattice logics and logics with strong negation, but also traditional logics including classical logic LK, classical modal logic S4 and classical linear logic CL. Cut-elimination theorems are proved for a variety of proposed sequent calculi including CLS (a conservative extension of CL) and CLS_cw (a conservative extension of some bilattice logics, LK and S4). Completeness theorems are given for these calculi with respect to phase semantics, for SLK (a conservative extension and fragment of LK and CLS_cw, respectively) with respect to a classical-like semantics, and for SS4 (a conservative extension and fragment of S4 and CLScw, respectively) with respect to a Kripke-type semantics. The proposed framework allows for an embedding of the proposed calculi into LK, S4 and CL.     

Normal Modal Substructural Logics with Strong Negation

We introduce modal propositional substructural logics with strong negation, and prove the completeness theorems (with respect to Kripke models) for these logics.     

Quantized Linear Logic,Involutive Quantales and Strong Negation

A new logic, quantized intuitionistic linear logic (QILL), is introduced, and is closely related to the logic which corresponds to Mulvey and Pelletier's (commutative) involutive quantales. Some cut-free sequent calculi with a new property quantization principle and some complete semantics such as an involutive quantale model and a quantale model are obtained for QILL. The relationship between QILL and Wansing's extended intuitionistic linear logic with strong negation is also observed using such syntactical and semantical frameworks.     

Nelson's Negation on the Base of Weaker Versions of Intuitionistic Negation

Constructive logic with Nelson negation is an extension of the intuitionistic logic with a special type of negation expressing some features of constructive falsity and refutation by counterexample. In this paper we generalize this logic weakening maximally the underlying intuitionistic negation. The resulting system, called subminimal logic with Nelson negation, is studied by means of a kind of algebras called generalized N-lattices. We show that generalized N-lattices admit representation formalizing the intuitive idea of refutation by means of counterexamples giving in this way a counterexample semantics of the logic in question and some of its natural extensions. Among the extensions which are near to the intuitionistic logic are the minimal logic with Nelson negation which is an extension of the Johansson's minimal logic with Nelson negation and its in a sense dual version — the co-minimal logic with Nelson negation. Among the extensions near to the classical logic are the well known 3-valued logic of Lukasiewicz, two 12-valued logics and one 48-valued logic. Standard questions for all these logics — decidability, Kripke-style semantics, complete axiomatizability, conservativeness are studied. At the end of the paper extensions based on a new connective of self-dual conjunction and an analog of the Lukasiewicz middle value ½ have also been considered.     

Non-Classical Negation in the Works of Helena Rasiowa and Their Impact on the Theory of Negation

The paper is devoted to the contributions of Helena Rasiowa to the theory of non-classical negation. The main results of Rasiowa in this area concerns–constructive logic with strong (Nelson) negation,–intuitionistic negation and some of its generalizations: minimal negation of Johansson and semi-negation.We discuss also the impact of Rasiowa works on the theory of non-classical negation.A lecture presented at the International Conference Trends in Logic III : A. Mostowski, H. Rasiowa and C. Rauszer in memoriam, Warsaw, Ruciane-Nida September 23-26, 2005.     

A Rule-Extension of the Non-Associative Lambek Calculus

An extension L ⁺ of the non-associative Lambek calculus Lis defined. In L ⁺ the restriction to formula-conclusion sequents is given up, and additional left introduction rules for the directional implications are introduced. The system L ⁺ is sound and complete with respect to a modification of the ternary frame semantics for L.     

Constructive Logic with Strong Negation is a Substructural Logic. I

The goal of this two-part series of papers is to show that constructive logic with strong negation N is definitionally equivalent to a certain axiomatic extension NFL _ew of the substructural logic FL _ew . In this paper, it is shown that the equivalent variety semantics of N (namely, the variety of Nelson algebras) and the equivalent variety semantics of NFL _ew (namely, a certain variety of FL _ew -algebras) are term equivalent. This answers a longstanding question of Nelson [30]. Extensive use is made of the automated theorem-prover Prover9 in order to establish the result. The main result of this paper is exploited in Part II of this series [40] to show that the deductive systems N and NFL _ew are definitionally equivalent, and hence that constructive logic with strong negation is a substructural logic over FL _ew . Presented by Heinrich Wansing     

关于不可化归的多态式量词句的CCG探析

广义量词理论对英语中一些特定的量词句进行分析,把其中两个单态式量词合并成一个多态式量词。Keenan证明了这个多态式量词的意义不能化归为两个单态式量词的意义,即多态式量词的意义不能从两个单态式量词的标准意义推演出来。Keenan的研究是很有价值的,但本文尝试从另外的角度思考,对汉语类似的多态式量化句进行个案处理,采纳组合范畴语法针对自然语言表层结构的词汇主义方法,遵循部分表达式的意义决定整体表达式意义的组合原则,从两个单态式量词的非标准意义推演出整个多态式量词句的量化意义。     

Infinite Set Unification with Application to Categorial Grammar

In this paper the notion of unifier is extended to the infinite set case. The proof of existence of the most general unifier of any infinite, unifiable set of types (terms) is presented. Learning procedure, based on infinite set unification, is described.     

A Note on the Interpolation Property in Tense Logic

It is proved that all bimodal tense logics which contain the logic of the weak orderings and have unbounded depth do not have the interpolation property.     

A Note on Binary Inductive Logic

We consider the problem of induction over languages containing binary relations and outline a way of interpreting and constructing a class of probability functions on the sentences of such a language. Some principles of inductive reasoning satisfied by these probability functions are discussed, leading in turn to a representation theorem for a more general class of probability functions satisfying these principles.     

A Note on Graded Modal Logic

We introduce a notion of bisimulation for graded modal logic. Using this notion, the model theory of graded modal logic can be developed in a uniform manner. We illustrate this by establishing the finite model property and proving invariance and definability results.     

The Class of Extensions of Nelson's Paraconsistent Logic

The article is devoted to the systematic study of the lattice εN4_⊥ consisting of logics extending N4_⊥. The logic N4_⊥ is obtained from paraconsistent Nelson logic N4 by adding the new constant ⊥ and axioms ⊥ → p, p → ∼ ⊥. We study interrelations between εN4_⊥ and the lattice of superintuitionistic logics. Distinguish in εN4_⊥ basic subclasses of explosive logics, normal logics, logics of general form and study how they are relate. The author acknowledges support by the Alexander von Humboldt-Stiftung and by Counsil for Grants under RF President, project NSh - 2112.2003.1.     

Canonical Extensions and Relational Representations of Lattices with Negation

This work is part of a wider investigation into lattice-structured algebras and associated dual representations obtained via the methodology of canonical extensions. To this end, here we study lattices, not necessarily distributive, with negation operations.We consider equational classes of lattices equipped with a negation operation ¬ which is dually self-adjoint (the pair (¬,¬) is a Galois connection) and other axioms are added so as to give classes of lattices in which the negation is De Morgan, orthonegation, antilogism, pseudocomplementation or weak pseudocomplementation. These classes are shown to be canonical and dual relational structures are given in a generalized Kripke-style. The fact that the negation is dually self-adjoint plays an important role here, as it implies that it sends arbitrary joins to meets and that will allow us to define the dual structures in a uniform way.Among these classes, all but one—that of lattices with a negation which is an antilogism—were previously studied by W. Dzik, E. Or?owska and C. van Alten using Urquhart duality.In some cases in which a given axiom does not imply that negation is dually self-adjoint, canonicity is proven with the weaker assumption of antitonicity of the negation.     

Negation in the Context of Gaggle Theory

We study an application of gaggle theory to unary negative modal operators. First we treat negation as impossibility and get a minimal logic system Ki that has a perp semantics. Dunn's kite of different negations can be dealt with in the extensions of this basic logic K_i. Next we treat negation as “unnecessity” and use a characteristic semantics for different negations in a kite which is dual to Dunn's original one. K_u is the minimal logic that has a characteristic semantics. We also show that Shramko's falsification logic FL can be incorporated into some extension of this basic logic K_u. Finally, we unite the two basic logics K_i and K_u together to get a negative modal logic K_-, which is dual to the positive modal logic K₊ in [7]. Shramko has suggested an extension of Dunn's kite and also a dual version in [12]. He also suggested combining them into a “united” kite. We give a united semantics for this united kite of negations.     

A Note on Priest's Finite Inconsistent Arithmetics

We give a complete characterization of Priest's Finite Inconsistent Arithmetics observing that his original putative characterization included arithmetics which cannot in fact be realized.     

The Revival of Rejective Negation

Whether assent (acceptance) and dissent (rejection) are thought of as speech acts or as propositional attitudes, the leading idea of rejectivism is that a grasp of the distinction between them is prior to our understanding of negation as a sentence operator, this operator then being explicable as applying to A to yield something assent to which is tantamount to dissent from A. Widely thought to have been refuted by an argument of Frege"s, rejectivism has undergone something of a revival in recent years, especially in writings by Huw Price and Timothy Smiley. While agreeing that Frege"s argument does not refute the position, we shall air some philosophical qualms about it in Section 5, after a thorough examination of the formal issues in Sections 1–4. This discussion draws on – and seeks to draw attention to – some pertinent work of Kent Bendall in the 1970s.