E, R AND γ

1969 ◽  
Vol 34 (3) ◽  
pp. 460-474 ◽  
Author(s):  
Robert K. Meyer ◽  
J. Michael Dunn

By γ, we mean the rule, “From ├ A and ├ Ā V B, infer ├ B”.1 This rule has played an important and a controversial role in a set of relevant logics free of certain well-known paradoxes of implication, like AĀ-→B and A-→(B-→B). Among these logics we count the pioneering systems of strenge Implikation presented by Ackermann in [1],2 as well as the Anderson-Belnap systems E of entail-ment and R of relevant implication.3


1996 ◽  
Vol 61 (2) ◽  
pp. 402-420 ◽  
Author(s):  
Ross T. Brady

We establish cut-free left-handed Gentzenizations for a range of major relevant logics from B through to R, all with distribution. B is the basic system of the Routley-Meyer semantics (see [15], pp. 287–300) and R is the logic of relevant implication (see [1], p. 341). Previously, the contractionless logics DW, TW, EW, RW and RWK were Gentzenized in [3], [4] and [5], and also the distributionless logics LBQ, LDWQ, LTWQo, LEWQot, LRWQ, LRWKQ and LRQ in [6] and [7]. This paper provides Gentzenizations for the logics DJ, TJ, T and R, with various levels of contraction, and for the contractionless logic B, which could not be included in [4] using the technique developed there. We also include the Gentzenization of TW in order to compare it with that in [4]. The Gentzenizations that we obtain here for DW and RW are inferior to those already obtained in [4], but they are included for reference when constructing other systems. The logics EW and E present a difficulty for our method and are omitted. For background to the Gentzenization of relevant logics, see [6], and for motivation behind the logics involved, see [6], [1] and [15]. Because of the number of properties that are brought to bear in obtaining these systems, we prefer to consider Gentzenizations for particular logics rather than for arbitrary bunches of axioms.



2019 ◽  
Vol 16 (2) ◽  
pp. 10
Author(s):  
Peter Verdée ◽  
Inge De Bal ◽  
Aleksandra Samonek

In this paper we first develop a logic independent account of relevant implication. We propose a stipulative denition of what it means for a multiset of premises to relevantly L-imply a multiset of conclusions, where L is a Tarskian consequence relation: the premises relevantly imply the conclusions iff there is an abstraction of the pair <premises, conclusions> such that the abstracted premises L-imply the abstracted conclusions and none of the abstracted premises or the abstracted conclusions can be omitted while still maintaining valid L-consequence.          Subsequently we apply this denition to the classical logic (CL) consequence relation to obtain NTR-consequence, i.e. the relevant CL-consequence relation in our sense, and develop a sequent calculus that is sound and complete with regard to relevant CL-consequence. We present a sound and complete sequent calculus for NTR. In a next step we add rules for an object language relevant implication to thesequent calculus. The object language implication reflects exactly the NTR-consequence relation. One can see the resulting logic NTR-> as a relevant logic in the traditional sense of the word.       By means of a translation to the relevant logic R, we show that the presented logic NTR is very close to relevance logics in the Anderson-Belnap-Dunn-Routley-Meyer tradition. However, unlike usual relevant logics, NTR is decidable for the full language, Disjunctive Syllogism (A and ~AvB relevantly imply B) and Adjunction (A and B relevantly imply A&B) are valid, and neither Modus Ponens nor the Cut rule are admissible.



2021 ◽  
Vol 18 (5) ◽  
pp. 154-288
Author(s):  
Robert Meyer

The purpose of this paper is to formulate first-order Peano arithmetic within the resources of relevant logic, and to demonstrate certain properties of the system thus formulated. Striking among these properties are the facts that (1) it is trivial that relevant arithmetic is absolutely consistent, but (2) classical first-order Peano arithmetic is straightforwardly contained in relevant arithmetic. Under (1), I shall show in particular that 0 = 1 is a non-theorem of relevant arithmetic; this, of course, is exactly the formula whose unprovability was sought in the Hilbert program for proving arithmetic consistent. Under (2), I shall exhibit the requisite translation, drawing some Goedelian conclusions therefrom. Left open, however, is the critical problem whether Ackermann’s rule γ is admissible for theories of relevant arithmetic. The particular system of relevant Peano arithmetic featured in this paper shall be called R♯. Its logical base shall be the system R of relevant implication, taken in its first-order form RQ. Among other Peano arithmetics we shall consider here in particular the systems C♯, J♯, and RM3♯; these are based respectively on the classical logic C, the intuitionistic logic J, and the Sobocinski-Dunn semi-relevant logic RM3. And another feature of the paper will be the presentation of a system of natural deduction for R♯, along lines valid for first-order relevant theories in general. This formulation of R♯ makes it possible to construct relevantly valid arithmetical deductions in an easy and natural way; it is based on, but is in some respects more convenient than, the natural deduction formulations for relevant logics developed by Anderson and Belnap in Entailment.



1987 ◽  
Vol 52 (2) ◽  
pp. 526-529 ◽  
Author(s):  
Steve Giambrone ◽  
Robert K. Meyer ◽  
Alasdair Urquhart

Semilattice semantics for relevant logics were discovered independently by Routley and Urquhart over 10 years ago. A semilattice semantics was first published in [10], where the weak theory of implication of [8] and [3] (i.e., R →, the pure implication fragment of the system R of relevant implication) is shown to be consistent and complete with respect to it. That result was extended in [11], But the semantics is explored in greatest detail in [12]. As reported in [4], Fine outfitted the positive semilattice semantics for R+ with a suitable Hilbert-style axiomatisation. (We refer to the system as ◡R+.) In 1980 Charlwood supplied a subscripted system of natural deduction. (See [1] and [2].) A subscripted Gentzen system was devised in [5] and [6].Obviously, the central idea of the semilattice semantics is to impose relevant-style valuations on a semilattice (with an identity) used as the underlying model structure. However, in [12] the contractionless semantics are obtained (quite reasonably) by dropping the idempotence postulate and thus changing the relatively simple semilattice structure into a commutative monoid. Here we show that the semilattice structure can be regained for positive, contractionless relevant implication. Although we have no proofs as yet, we think that this semantics will pave the way for showing completeness for the corresponding subscripted Gentzen and natural deduction systems, as well as the Hilbert-style axiomatization, ◡RW+.



2021 ◽  
pp. 1-22
Author(s):  
SHAWN STANDEFER

Abstract Anderson and Belnap presented indexed Fitch-style natural deduction systems for the relevant logics R, E, and T. This work was extended by Brady to cover a range of relevant logics. In this paper I present indexed tree natural deduction systems for the Anderson–Belnap–Brady systems and show how to translate proofs in one format into proofs in the other, which establishes the adequacy of the tree systems.



2017 ◽  
Vol 10 (4) ◽  
pp. 663-681
Author(s):  
GUILLERMO BADIA

AbstractAnalogues of Scott’s isomorphism theorem, Karp’s theorem as well as results on lack of compactness and strong completeness are established for infinitary propositional relevant logics. An “interpolation theorem” (of a particular sort introduced by Barwise and van Benthem) for the infinitary quantificational boolean logic L∞ω holds. This yields a preservation result characterizing the expressive power of infinitary relevant languages with absurdity using the model-theoretic relation of relevant directed bisimulation as well as a Beth definability property.



Author(s):  
Andrew Tedder ◽  
Nicholas Ferenz
Keyword(s):  


2013 ◽  
Vol 113 (2) ◽  
pp. 309-319 ◽  
Author(s):  
Tarek A. Bismar ◽  
Mohammed Alshalalfa ◽  
Lars F. Petersen ◽  
Liang Hong Teng ◽  
Travis Gerke ◽  
...  


1989 ◽  
pp. 179-184
Author(s):  
Zane Parks ◽  
Michael Byrd
Keyword(s):  


2021 ◽  
pp. 225-242
Author(s):  
Greg Restall


Sign in / Sign up

Export Citation Format

Share Document