In the first part of this paper we indicate how Meredith's condensed detachment may be used to give a new proof of Belnap's theorem that if every axiom x of a calculus S has the two-property that every variable which occurs in x occurs exactly twice in x, then every theorem of S is a substitution instance of a theorem of S which has the two-property. In the remainder of the paper we discuss the use of mechanical theorem-provers, based either (...) on condensed detachment or on the resolution rule of J. A. Robinson, to investigate various calculi whose axioms all have the two-property. Particular attention is given to D-groupoids, i.e. sets of formulae which are closed under condensed detachment. (shrink)

Lattice BCK logic is the expansion of the well known Meredith implicational logic BCK expanded with lattice conjunction and disjunction. Although its natural axiomatization has three rules named modus ponens, ∨‐rule and ∧‐rule, we show that we can give an equivalent presentation with just modus ponens and ∧‐rule, however it is impossible to obtain an equivalent presentation with modus ponens as unique rule. In this paper we study and characterize all axiomatic extensions of lattice BCK logic with modus ponens as (...) unique rule. We obtain an infinite chain of proper axiomatic extensions with this property. Moreover, we prove that there is no weakest axiomatic extension of Lattice BCK‐logic admitting modus ponens as unique rule. (shrink)

This paper provides a finer analysis of the well-known form of the Local Deduction Theorem in contraction-free logics . An infinite hierarchy of its natural strengthenings is introduced and studied. The main results are the separation of its initial four members and the subsequent collapse of the hierarchy.

This article answers two questions (posed in the literature), each concerning the guaranteed existence of proofs free of double negation. A proof is free of double negation if none of its deduced steps contains a term of the formn(n(t)) for some term t, where n denotes negation. The first question asks for conditions on the hypotheses that, if satisfied, guarantee the existence of a double-negation-free proof when the conclusion is free of double negation. The second question asks about the existence (...) of an axiom system for classical propositional calculus whose use, for theorems with a conclusion free of double negation, guarantees the existence of a double-negation-free proof. After giving conditions that answer the first question, we answer the second question by focusing on the Lukasiewicz three-axiom system. We then extend our studies to infinite-valued sentential calculus and to intuitionistic logic and generalize the notion of being double-negation free. The double-negation proofs of interest rely exclusively on the inference rule condensed detachment, a rule that combines modus ponens with an appropriately general rule of substitution. The automated reasoning program Otter played an indispensable role in this study. (shrink)

We introduce a general technique for finding sets of axioms for a given class of semigroups. To illustrate the technique, we provide new sets of defining axioms for groups of exponent n, bands, and semilattices.