Two consecution calculi are introduced: one for the implicational fragment of the logic of entailment with truth and another one for the disjunction free logic of nondistributive relevant implication. The proof technique—attributable to Gentzen—that uses a double induction on the degree and on the rank of the cut formula is shown to be insufficient to prove admissible various forms of cut and mix in these calculi. The elimination theorem is proven, however, by augmenting the earlier double inductive proof with additional (...) inductions. We also give a new purely inductive proof of the cut theorem for the original single cut rule in Gentzen’s sequent calculus $ LK $ without any use of mix. (shrink)

Two consecution calculi are introduced: one for the implicational fragment of the logic of entailment with truth and another one for the disjunction free logic of nondistributive relevant implication. The proof technique—attributable to Gentzen—that uses a double induction on the degree and on the rank of the cut formula is shown to be insufficient to prove admissible various forms of cut and mix in these calculi. The elimination theorem is proven, however, by augmenting the earlier double inductive proof with additional (...) inductions. We also give a new purely inductive proof of the cut theorem for the original single cut rule in Gentzen’s sequent calculus \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$ LK $$\end{document} without any use of mix. (shrink)

It is proved that Ackermann’s rule δ is admissible in a wide spectrum of relevant logics satisfying certain syntactical properties.

Reviewed Works:Gaisi Takeuti, Proof Theory.Georg Kreisel, Proof Theory: Some Personal Recollections.Wolfram Pohlers, Contributions of the Schutte School in Munich to Proof Theory.Stephen G. Simpson, Subsystems of $\mathbf{Z}_2$ and Reverse Mathematics.Solomon Feferman, Proof Theory: A Personal Report.

The aim of this paper is to provide a Routley-Meyer semantics for Ackermann’s logics of “strenge Implikation” Π ′ and Π ′′ . Besides the Disjunctive Syllogism, this semantics validates the rules Necessitation and Assertion. Strong completeness theorems for Π ′ and Π ′′ are proved. A brief discussion on Π ′ , Π ′′ and paraconsistency is included.

We show, first, that the normalization procedure for S4 modal logic presented by Dag Prawitz in [5] does not work. We then develop a new natural deduction system for S4 classical modal logic that is logically equivalent to that of Prawitz, and we show that every derivation in this new system can be transformed into a normal derivation.

We show, first, that the normalization procedure for S4 modal logic presented by Dag Prawitz in [5] does not work. We then develop a new natural deduction system for S4 classical modal logic that is logically equivalent to that of Prawitz, and we show that every derivation in this new system can be transformed into a normal derivation.

The Logic R4 is obtained by adding the axiom □(A v B) → (◇A v □B) to the modal relevant logic NR. We produce a model theory for this logic and show completeness. We also show that there is a natural embedding of a Kripke model for S4 in each R4 model structure.

The logic CE (for "Classical E") results from adding Boolean negation to Anderson and Belnap's logic E. This paper shows that CE is not a conservative extension of E.

We introduce several restricted versions of the structural rules in the implicational fragment of Gentzen's sequent calculus LJ. For example, we permit the applications of a structural rule only if its principal formula is an implication. We investigate cut-eliminability and theorem-equivalence among various combinations of them. The results include new cut-elimination theorems for the implicational fragments of the following logics: relevant logic E, strict implication S4, and their neighbors (e.g., E-W and S4-W); BCI-logic, BCK-logic, relevant logic R, and the intuitionistic (...) logic. (shrink)

A sequent calculus for the positive fragment of entailment together with the Church constants is introduced here. The single cut rule is admissible in this consecution calculus. A topological dual gaggle semantics is developed for the logic. The category of the topological structures for the logic with frame morphisms is proven to be the dual category of the variety, that is defined by the equations of the algebra of the logic, with homomorphisms. The duality results are extended to the logic (...) of entailment that includes a De Morgan negation. (shrink)

Two consecution calculi are introduced: one for the implicational fragment of the logic of entailment with truth and another one for the disjunction free logic of nondistributive relevant implication. The proof technique—attributable to Gentzen—that uses a double induction on the degree and on the rank of the cut formula is shown to be insufficient to prove admissible various forms of cut and mix in these calculi. The elimination theorem is proven, however, by augmenting the earlier double inductive proof with additional (...) inductions. We also give a new purely inductive proof of the cut theorem for the original single cut rule in Gentzen’s sequent calculus $ LK $ without any use of mix. (shrink)

This paper has two aims. First, it sets out an interpretation of the relevant logic E of relevant entailment based on the theory of situated inference. Second, it uses this interpretation, together with Anderson and Belnap’s natural deduc- tion system for E, to generalise E to a range of other systems of strict relevant implication. Routley–Meyer ternary relation semantics for these systems are produced and completeness theorems are proven. -/- .