In this article, I present a semantically natural conservative extension of Urquhart’s positive semilattice logic with a sort of constructive negation. A subscripted sequent calculus is given for this logic and proofs of its soundness and completeness are sketched. It is shown that the logic lacks the finite model property. I discuss certain questions Urquhart has raised concerning the decision problem for the positive semilattice logic in the context of this logic and pose some problems for further research.

We report on progress and an unsolved problem in our attempt to obtain a clear rationale for relevance logic via semantic decomposition trees. Suitable decomposition rules, constrained by a natural parity condition, generate a set of directly acceptable formulae that contains all axioms of the well-known system R, is closed under substitution and conjunction, satisfies the letter-sharing condition, but is not closed under detachment. To extend it, a natural recursion is built into the procedure for constructing decomposition trees. The resulting (...) set of acceptable formulae has many attractive features, but it remains an open question whether it continues to satisfy the crucial letter-sharing condition. (shrink)