Papers on (mostly distributive) Substructural Logics

John Slaney



More Proofs of an Axiom of Lukasiewicz

This is the abstract of the paper:

John Slaney.
More Proofs of an Axiom of Lukasiewicz.
Journal of Automated Reasoning , 29 (2002): 59-66.

This paper reports results and some new problems in one of the domains to which automatic first-order theorem provers have been most successfully applied: axiomatics of non-classical propositional logics. It is well known that one of the standard axioms of the denumerable-valued pure implication logic of Lukasiewicz becomes derivable from the remainder in the presence of negation. Here it is shown that the same axiom is similarly derivable using conjunction and disjunction instead of negation. This closes a problem left open by Harris and Fitelson Journal of Automated Reasoning 27, 2001). Related problems are discussed, and five such open problems are hereby proposed as challenges to the automated reasoning community.



Logic for Two

This is the abstract of the paper:

John Slaney and Robert Meyer.
Logic for Two: The Semantics of Distributive Substructural Logics.
Proceedings of the First International Joint Conference on Qualitative and Quantitative Practical Reasoning (ECSQARU-FAPR) , (1997): 554-567.

This is an account of the semantics of a family of logics whose paradigm member is the relevant logic R of Anderson and Belnap. The formal semantic theory is well worn, having been discussed in the literature of such logics for over a quarter of a century. What is new here is the explication of that formal machinery in a way intended to make sense of it for those who have claimed it to be esoteric, `merely formal' or downright impenetrable. Our further goal is to put these logics in the service of practical reasoning systems, since the basic concept of our treatment is that of an agent a reasoning to conclusions using as assumptions the theory of agent b, where a and b may or may not be the same. This concept requires true multi-agent reasoning, as opposed to what is merely reasoning by multiple agents.



Finite Models for some Substructural Logics

This is the abstract of the paper:

J K Slaney.
Finite Models for some Substructural Logics.
Logique et Analyse , 139-140 (1992, published 1994): 313-333.

This paper is a report of computer-driven research into the modelling of propositional systems related both to linear logic and to relevant logic. One result is an exponential lower bound on the number of models of given size validating such systems. Another theorem explores dualities within models for such systems in order to explain striking regularities in the distribution of models of the system C. In these researches the computer figures not as a prover of theorems, nor even as a proof assistant, but as a source of quasi-empirical data.



Classical Versions of BCI, BCK and BCIW Logics

This is an abstract of the paper:

John K Slaney and Martin W. Bunder.
Classical Versions of BCI, BCK and BCIW Logics.
Bulletin of the Section of Logic, University of Lódz; , 23 (1994): 61-65.

We give an implicational formula X such the results of strengthening each of the substructural logics BCI, BCIW and BCK by the addition of X is a distict system weaker than classical logic, but such that BCKW plus X is classical logic. This answers a question posed by Karpenko. The derivations and independence proofs in this paper were generated automatically using our programs SCOTT and MaGIC.



A General Logic

This is the introduction to the paper:

John Slaney.
A General Logic.
Australasian Journal of Philosophy 68 (1990): 74-88.

This is an essay in logic in the traditional sense: the formal theory of inference. In it I attempt a unified account of a fairly wide range of logical systems, some very well known and others less so. These systems include classical logic, relevant logics such as Anderson and Belnap's R, close relatives of fuzzy logic, some modal logics and many weaker, but still interesting, nonstandard systems. These diverse logics, quite different in their philosophical underpinnings, are displayed as variations on a single and simple theme. Although its concern is with formal logic this paper is designed to be accessible to non-specialists. It only assumes familiarity with a natural-deduction formulation of elementary logic such as that of Lemmon's Beginning Logic. Nonclassical logics much as presented here have been introduced successfully to students with no formal logical training beyond a standard one-semester first course.

Little of the formal material of this paper is really new. In particular, following the work of Dunn, Meyer, Sylvan etc, relevant logicians have been using the most important technical device of my presentation at least since 1973 (see J.M. Dunn's `Gentzen system for Positive Relevant Implication' in Anderson and Belnap's Entailment (1975). Recent work by logical intuitionists on realizability semantics for their theories is also very close both formally and motivationally to my account. What is slightly more original to this paper is (I hope) a maximally smooth version of relevant logics and many of their rivals intended partly to dispose of the complaint that such systems are difficult, highly contrived and esoteric. I have also tried to emphasise the unified theory of so wide a spread of logics, to provide a framework within which they can be compared and contrasted with each other and which renders their extensive common content clearly visible. It has, at any rate, long seemed desirable that these scattered facts, in some form familiar to many of us, should somehow be gathered together in one place.



Solution to a Problem of Ono and Komori

This is the introduction to the paper:

John Slaney.
Solution to a Problem of Ono and Komori.
Journal of Philosophical Logic 18 (1989): 103-111.

The logics DBCK and DBCC result from BCK and BCC respectively by the addition of a postulate for the distribution of conjunction over disjunction. Ono and Komori (Journal of Symbolic Logic 1984) leave as an open problem the provision of a cut-free formulation of these logics. In this paper their problem is solved by means of a technique which extends to a great range of non-classical systems such as the positive parts of relevant logics.

A flaw in the proof in this paper was pointed out by Peter Schröder-Heister. This was corrected in a subsequent note, also published in the Journal of Philosophical Logic.



Reduced Models for Relevant Logics Without WI

This is an abstract of the paper:

John Slaney.
Reduced Models for Relevant Logics Without WI.
Notre Dame Journal of Formal Logic 28 (1987): 395-407.

The object of this paper is to prove a reduced modelling theorem for a wide range of logics which are weaker than the usual relevant logics in that they lack the rule of contraction. Reduced modelling means that in the Routley-Meyer semantics for these systems the base world T where truth is evaluated satisfies the condition that for all worlds a and b, a is contained in b iff RTab. The proof makes use of a three-valued metavaluation to establish the primeness of the logics in question. The result subsumes an earlier theorem of the author (Studia Logica 1984) which covered only three of the logics.

A minor correction to this paper was later made by Steve Giambrone.



Automated Reasoning Group
Computer Sciences Laboratory
Research School of Information Sciences and Engineering
Australian National University