Relevance logics, also known as relevant logics, are non-classical logics? designed to avoid what some consider to be paradoxical about classical implication. In particular, certain hypothetical propositions in which antecedent and consequent are irrelevant to one another occur as tautologies in classical logic, whereas one might consider that a claim that ‘$P$ implies $Q$’ suggests that the truth of $P$ gives us reason to accept the truth of $Q$.
There are a number of logics that have been considered in the context of “relevance”. Many of them can, at least roughly, be regarded as substructural logics like linear logic. Unlike linear logic, most relevance logics permit the contraction rule, but not the weakening rule. Thus in a sense they are the “dual” of affine logic which permits weakening but not contraction.
Generally speaking, most relevance logics contain the following logical connectives:
Other connectives that sometimes appear in relevance logics include:
This description may give the impression that relevance logics could be obtained from linear logic by adding contraction and perhaps removing some undesired connectives. This is close to true, but many relevance logics have additional features that this would not capture. One notable one is that the additive conjunction still distributes over the additive disjunction:
although this is not true in linear logic, and simply adding contraction does not make it true. (It is true linearly — and relevance-ly — that the multiplicative conjunction distributes over additive disjunction, but adding contraction does not collapse the two conjunctions.) It can of course be added as an axiom, but it is often better to give a modified sequent calculus that makes it true automatically, by using bunches. One such sequent calculus can be found in (Mints); see also bunched logic and display logic.
Some relevance logics also do without contraction. This has been found particularly helpful in making them paraconsistent/nontrivial even in the presence of things like the comprehension rule of naive set theory?.
Historically, relevance logics have usually been formulated first as Hilbert systems, and only later have equivalent sequent calculus and natural deduction systems been found.
The logic R+ (“positive R”) contains $\wedge,\vee,\to$ only, with contraction and the distributive law. Fusion $\circ$ is sometimes added, since it can be characterized as an adjoint to $\to$, and likewise the nullary connectives. This logic can be formalized by a sequent calculus with bunches on the left whose structural connectives represent $\wedge$ and $\circ$, and single formulas on the right; see (Mints).
The logic R adds to R+ a multiplicative classical negation $\sim$. It is not clear whether it has a good sequent calculus, although if we also include an additive classical negation $\neg$ (which can be shown to be a conservative extension) then it can be represented in display logic. It is also similar to “classical bunched implication” with contraction added, in which case it may be easier to omit the additive negation. For a Hilbert system, see SEP.
Just as linear logic (with the exchange rule, but not contraction or weakening) has semantics in symmetric monoidal categories, and ordinary logic has semantics in cartesian monoidal categories (both perhaps with extra structure, such as being closed or star-autonomous), affine logic has semantics in semicartesian monoidal categories while relevance logics (with contraction) have semantics in relevance monoidal categories. The monoidal product represents the multiplicative conjunction; of course, the other connectives then have to be added in an appropriately related way.
G. E. Mints. Cut-elimination theorem for relevant logics, Zap. Nauchn. Sem. LOMI, 1972, Volume 32, Pages 90–97. (math-net.ru). An English translation appears in the Journal of Soviet Mathematics 6 (1976) pp.422-8. (doi)