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.

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.

This is the introduction to the paper:

John Slaney.

A General Logic.

Australasian Journal of Philosophy68 (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 Logic18 (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 Logic28 (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 R*T**a**b*. 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