Some investigations into the algebraic constructive aspects of a decision procedure for various fragments of Relevant Logics are presented. Decidability of these fragments relies on S. Kripke's gentzenizations and on his combinatorial lemma known as Kripke's lemma that B. Meyer has shown equivalent to Dickson's lemma in number theory and to his own infinite divisor lemma, henceforth, Meyer's lemma or IDP. These investigations of the constructive aspects of the Kripke's-Meyer's decision procedure originate in the development of Paul Thistlewaite's “Kripke” theorem (...) prover that had been devised to tackle the decision problem of the Relevant Logic R. A. Urquhart's pen and paper solution that relies on a sophisticated algebraic and geometric treatment of the problem shows the usefulness of an algebraic approach in Logic. Here, the study of the constructive aspects of the Kripke-Meyer decision procedure relies on various algebraic constructive results in the theory of polynomials rings. (shrink)

A calculus of names is a logical theory describing relations between names. By a pure calculus of names we mean a quantifier-free formulation of such a theory, based on classical propositional calculus. An axiomatisation of a pure calculus of names is presented and its completeness is discussed. It is shown that the axiomatisation is complete in three different ways: with respect to a set theoretical model, with respect to Leśniewski's Ontology and in a sense defined with the use of axiomatic (...) rejection. The independence of axioms is proved. A decision procedure based on syntactic transformations and models defined in the domain of only two members is defined. (shrink)

This is an extended critical notice of Gillian Russell's book, Barriers to Entailment.

This book provides a critical examination of how the choice of what to believe is represented in the standard model of belief change. In particular the use of possible worlds and infinite remainders as objects of choice is critically examined. Descriptors are introduced as a versatile tool for expressing the success conditions of belief change, addressing both local and global descriptor revision. The book presents dynamic descriptors such as Ramsey descriptors that convey how an agent’s beliefs tend to be changed (...) in response to different inputs. It also explores sentential revision and demonstrates how local and global operations of revision by a sentence can be derived as a special case of descriptor revision. Lastly, the book examines revocation, a generalization of contraction in which a specified sentence is removed in a process that may possibly also involve the addition of some new information to the belief set. (shrink)

As is well known, answer-set programs do not satisfy the replacement property in general, i.e., programs and that are equivalent may cease to be so when they are put in the context of some other program, i.e., and may have different answer sets. Lifschitz, Pearce, and Valverde thus introduced strong equivalence for context-independent equivalence, and proved that such equivalence holds between given programs and iff and are equivalent theories in the monotonic logic of here-and-there. In this article, we consider a (...) related question: given a program, does there exist some program from a certain class of programs such that and are equivalent under a given notion of equivalence? Furthermore, if the answer to this question is positive, how can we recast as an equivalent program from? In particular, we consider classes of programs that emerge by allowing disjunction and/or negation, and as equivalence notions we consider strong, uniform, and ordinary equivalence. Based on general model-theoretic properties and a novel form of canonical programs, we develop semantic characterisations for the existence of such a program, determine the computational complexity of checking existence, and provide rewriting rules for recasting. (shrink)

The paper is dedicated to the 80th birthday of the outstanding Russian logician A.V. Kuznetsov. It is addressing a history of the ideas and research conducted by him in non-classical and intermediate logics.