An Elementary Proof of Chang's Completeness Theorem for the Infinite-valued Calculus of Lukasiewicz

The interpretation of propositions in Lukasiewicz's infinite-valued calculus as answers in Ulam's game with lies--the Boolean case corresponding to the traditional Twenty Questions game--gives added interest to the completeness theorem. The literature contains several different proofs, but they invariably require technical prerequisites from such areas as model-theory, algebraic geometry, or the theory of ordered groups. The aim of this paper is to provide a self-contained proof, only requiring the rudiments of algebra and convexity in finite-dimensional vector spaces.     

Marginalia on Sequent Calculi

The paper discusses the relationship between normal natural deductions and cutfree proofs in Gentzen (sequent) calculi in the absence of term labeling. For Gentzen calculi this is the usual version; for natural deduction this is the version under the complete discharge convention, where open assumptions are always discharged as soon as possible. The paper supplements work by Mints, Pinto, Dyckhoff, and Schwichtenberg on the labeled calculi.     

A new experimental method to identify the process of logical reasoning

Abstract: A new method to identify the process of logical reasoning is presented. In spite of its indispensability and importance, we have had few methods to identify a subject's reasoning process, except that of using verbal protocol data. In this paper, for the purpose of objective identification of the reasoning process, we propose a new method to obtain the subject's reasoning process, in terms of a resolution tree for a task of which the logical structure can be written by first-order predicate logic. The results of an experiment using this method are presented. They revealed some interesting features of human reasoning such as, large differences between subjects, remarkable parallel processes, and the existence of subgoals for each subject.     

What Russell Couldn't Describe

There is currently debate between deflationists and anti-deflationists about the ontology of persisting objects. Some deflationists think that disputes between, for example, four-dimensionalists (e.g. Ted Sider and David Lewis) and quasi-nihilists (e.g. Peter Van Inwagen and Trenton Merricks) are merely verbal disputes. Anti-deflationists deny this. Eli Hirsch is a deflationist who maintains that many ontological disputes are merely verbal. Theodore Sider maintains that the disputes are not merely verbal. Hirsch and Sider are thus engaged in a metaontological dispute. In this paper, I argue that Hirsch's metaontological dispute with Sider is, by Hirsch's own lights, itself merely verbal. I conclude that the mere verbalness of his metaontological dispute with Sider suggests that Hirsch's account of what makes a dispute merely verbal may be problematic.     

A sequent calculus for a logic of contingencies

We introduce a sequent calculus that is sound and complete with respect to propositional contingencies, i.e., formulas which are neither provable nor refutable. Like many other sequent and natural deduction proof systems, this calculus possesses cut elimination and the subformula property and has a simple proof search mechanism.     

Chunk and Permeate,a Paraconsistent Inference Strategy. Part I: The Infinitesimal Calculus

In this paper we introduce a paraconsistent reasoning strategy, Chunk and Permeate. In this, information is broken up into chunks, and a limited amount of information is allowed to flow between chunks. We start by giving an abstract characterisation of the strategy. It is then applied to model the reasoning employed in the original infinitesimal calculus. The paper next establishes some results concerning the legitimacy of reasoning of this kind – specifically concerning the preservation of the consistency of each chunk – and concludes with some other possible applications and technical questions.     

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.