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)

The implicational fragment of the relevance logic "ticket entailment" is closely related to the so-called hereditary right maximal terms. I prove that the terms that need to be considered as inhabitants of the types which are theorems of $T_\rightarrow$ are in normal form and built in all but one casefrom B, B' and W only. As a tool in the proof ordered term rewriting systems are introduced. Based on the main theorem I define $FIT_\rightarrow$ - a Fitch-style calculus for the (...) implicational fragment of ticket entailment. (shrink)

We introduce necessary and sufficient conditions for a (single-conclusion) sequent calculus to admit (reductive) cut-elimination. Our conditions are formulated both syntactically and semantically.

In this paper, we shall confine ourselves to the study of sentential constants in the system R of relevant implication.In dealing with the behaviour of the sentential constants in R, we shall think of R itself as presented in three stages, depending on the level of truth-functional involvement.

A 'Kripke-style' semantics is given for combinatory logic using frames with a ternary accessibility relation, much as in the Tourley-Meyer semantics for relevance logic. We prove by algebraic means a completeness theorem for combinatory logic, by proving a representation theorem for 'combinatory posets.' A philosophical interpretation is given of the models, showing that an element of a combinatory poset can be understood simultaneously as a set of states and as a set of actions on states. This double interpretation allows for (...) one such element to be applied to another . Application turns out to be modeled the same way as 'fusion' in relevance logic.We also introduce 'dual combinators' that apply from the right. We then explore relationships to some well-known substructural logics, showing that each can be embedded into the structurally free. non-associative Lambek calculus, with the embedding taking a theorem ω to a statement of the form Γ ⊨ ω, where Γ is some fusion of the combinators needed to justify the structural assumptions of the given substructural logic. This builds on earlier ideas from Belnap and Meyer about a Gentzen system wherein structural rules are replaced with rules for introducing combinators. We develop such a system and prove a cut theorem. (shrink)

This is a review, with historical and critical comments, of a paper by I. E. Orlov from 1928, which gives the oldest known axiomatization of the implication-negation fragment of the relevant logic R. Orlov's paper also foreshadows the modal translation of systems with an intuitionistic negation into S4-type extensions of systems with a classical, involutive, negation. Orlov introduces the modal postulates of S4 before Becker, Lewis and Gödel. Orlov's work, which seems to be nearly completely ignored, is related to the (...) contemporaneous work on the axiomatization of intuitionistic logic. (shrink)

We introduce necessary and sufficient conditions for a (single-conclusion) sequent calculus to admit (reductive) cut-elimination. Our conditions are formulated both syntactically and semantically.

The implicational fragment of the relevance logic "ticket entailment" is closely related to the so-called hereditary right maximal terms. I prove that the terms that need to be considered as inhabitants of the types which are theorems of $T_\rightarrow$ are in normal form and built in all but one casefrom B, B' and W only. As a tool in the proof ordered term rewriting systems are introduced. Based on the main theorem I define $FIT_\rightarrow$ - a Fitch-style calculus (related to (...) $FT_\rightarrow$ ) for the implicational fragment of ticket entailment. (shrink)

The fixed point combinator (Y) is an important non-proper combinator, which is defhable from a combinatorially complete base. This combinator guarantees that recursive equations have a solution. Structurally free logics (LC) turn combinators into formulas and replace structural rules by combinatory ones. This paper introduces the fixed point and the dual fixed point combinator into structurally free logics. The admissibility of (multiple) cut in the resulting calculus is not provable by a simple adaptation of the similar proof for LC with (...) proper combinators. The novelty of our proof—beyond proving the cut for a newly extended calculus–is that we add a fourth induction to the by-and-large Gentzen-style proof. (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)

Die Gründe, die C. I. Lewis [5], [6] bewogen haben, neben der gewöhnlichen Implikation eine strikte Implikation einzuführen, sind bekannt. In der vorliegenden Arbeit wird aus ähnlichen Gründen eine strenge Implikation eingeführt, die jedoch einen engeren Begriff darstellt als die strikte Implikation. Mit einer Arbeit von Arnold Schmidt [7] hat meine nur geringe Berührungspunkte, da der Verfasser sich mit der strikten Implikation beschäftigt. Für diese wird ein relativ einfaches Axiomensystem angegeben und gezeigt, wie man durch geeignete Definitionen von Notwendigkeit und (...) Möglichkeit bei eventueller Hinzufügung von Zusatzaxiomen die bekannten Systeme des Modalitätenkalküls erhält. Den Hauptteil meiner Arbeit bildet die Einführung meines Implikationsbegriffs; im zweiten Teil der Arbeit komme ich dann auf dieser Basis auch zu einer Einführung der Modalitäten.Um die Art der Einführung des Kalküls zu motivieren, wollen wir kurz auf das eingehen, das uns mehr oder weniger deutlich vorschwebt, wenn wir von der strengen Implikation sprechen. Die strenge Implikation, die wir durchA → Bwiedergeben, soll ausdrücken, daß zwischenAundBein logischer Zusammenhang besteht, daß der Inhalt vonBein Teil des Inhaltes vonAist, oder wie wir es sonst ausdrücken wollen. Das hat mit der Richtigkeit oder Falschheit vonAundBnichts zu tun. So würde man die Allgemeingültigkeit einer FormelA→ (B → A) ablehnen, da sie den Schluß vonAaufB → Aeinschließt und da die Richtigkeit vonAnichts damit zu tun hat, ob zwischenBundAein logischer Zusammenhang besteht. (shrink)