\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{relevance logic}

\hypertarget{relevance_logics}{}\section*{{Relevance logics}}\label{relevance_logics}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{general_description}{General description}\dotfill \pageref*{general_description} \linebreak
\noindent\hyperlink{some_relevance_logics}{Some relevance logics}\dotfill \pageref*{some_relevance_logics} \linebreak
\noindent\hyperlink{the_logic_r}{The logic R}\dotfill \pageref*{the_logic_r} \linebreak
\noindent\hyperlink{categorical_semantics}{Categorical semantics}\dotfill \pageref*{categorical_semantics} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

\textbf{Relevance logics}, also known as \textbf{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$.

\hypertarget{general_description}{}\subsection*{{General description}}\label{general_description}

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]]:

\begin{itemize}%
\item A [[logical conjunction]] and a [[logical disjunction]], usually written $\wedge$ and $\vee$. These are \emph{additive} connectives, like those written $\&$ and $\oplus$ in linear logic.
\item An [[implication]], usually written $\to$. This is a \emph{multiplicative} or \emph{intensional} connective, like the [[linear implication]] $\multimap$ of linear logic.
\item A [[negation]], often written $\sim$ but sometimes $\neg$. This is also a multiplicative/intensional connective. Most relevance logics are ``multiplicatively classical'' in that the [[double negation law]] $\sim\sim A\to A$ holds. It follows that $\wedge$ and $\vee$ satisfy all the [[de Morgan laws]] with respect to $\sim$.

\end{itemize}
Other connectives that sometimes appear in relevance logics include:

\begin{itemize}%
\item A [[biconditional]] $A\leftrightarrow B$, usually defined as $(A\to B) \wedge (B\to A)$, combining the multiplicative implications with the additive conjunction.
\item A multiplicative [[truth]], like linear logic's $\mathbf{1}$. This can be defined as $A\to A$.
\item An additive truth and an additive falsity, like linear logic's $\top$ and $\mathbf{0}$. There does not appear to be any consensus in the relevance logic community on the notations for the nullary connectives, so on this page we will use the linear logic notations.
\item A [[multiplicative conjunction]] like linear logic's $\otimes$, usually called \emph{fusion} or \emph{cotenability} and denoted by $\circ$ or $*$. Assuming multiplicative classicality, this is definable from the relevant implication as $\sim (A\to\sim B)$. It can also be characterized as an adjoint to $\to$, that is $A\circ B \to C$ if and only if $A\to (B\to C)$.
\item More rarely, a [[multiplicative disjunction]] like linear logic's $\invamp$, sometimes called \emph{fission} (but for which there does not seem to be a standard notation). This is also classically definable from $\to$ as $\sim A \to B$. Note that multiplicative DNE $\sim\sim A\to A$ is then equivalent to multiplicative [[excluded middle]] $A\invamp \sim A$. The multiplicative falsity (linear logic $\bot$) seems to be rarely mentioned.
\item Also rarely (and apparently controversially), an additive negation $\neg$, which might be ``additively classical'' in the sense that $A\vee \neg A$.
\item A [[modal operator]] $\Box$ akin to [[necessity]]. The operation $\top \to A$ also sometimes behaves like necessity (note the mismatch of the additive $\top$ with the multiplicative $\to$).

\end{itemize}
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 [[distributive lattice|distributes]] over the [[additive disjunction]]:

\begin{displaymath}
A \wedge (B\vee C) \leftrightarrow (A\wedge B) \vee (A\wedge C)
\end{displaymath}
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 (\hyperlink{Mints}{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 logic|paraconsistent/nontrivial]] even in the presence of things like the [[comprehension rule]] of [[naive set theory]].

\hypertarget{some_relevance_logics}{}\subsection*{{Some relevance logics}}\label{some_relevance_logics}

Historically, relevance logics have usually been formulated first as [[Hilbert systems]], and only later have equivalent [[sequent calculus]] and [[natural deduction]] systems been found.

\hypertarget{the_logic_r}{}\subsubsection*{{The logic R}}\label{the_logic_r}

The logic R+ (``\textbf{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 (\hyperlink{Mints}{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 \href{http://plato.stanford.edu/entries/logic-relevance/logicr.html}{SEP}.

\hypertarget{categorical_semantics}{}\subsection*{{Categorical semantics}}\label{categorical_semantics}

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 monoidal category|closed]] or [[star-autonomous category|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.

\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[linear logic]]
\item [[bunched logic]]
\item Some relevance logics are also [[paraconsistent logic|paraconsistent]].

\end{itemize}
\hypertarget{references}{}\subsection*{{References}}\label{references}

\begin{itemize}%
\item \href{http://plato.stanford.edu/entries/logic-relevance/}{Stanford Encyclopedia of Philosophy}


\item G. E. Mints. Cut-elimination theorem for relevant logics, Zap. Nauchn. Sem. LOMI, 1972, Volume 32, Pages 90--97. (\href{http://www.mathnet.ru/php/archive.phtml?wshow=paper&jrnid=znsl&paperid=2569&option_lang=eng}{math-net.ru}). An English translation appears in the Journal of Soviet Mathematics 6 (1976) pp.422-8. (\href{http://doi.org/10.1007/BF01084083}{doi})



\end{itemize}
\begin{itemize}%
\item Peter W. O'Hearn and David J. Pym. The Logic of Bunched Implications. \emph{Bulletin of Symbolic Logic} 5(2):215-244. (\href{http://www.lsv.ens-cachan.fr/~demri/OHearnPym99.pdf}{pdf}) (\href{https://dx.doi.org/10.2307%2F421090}{doi})

\end{itemize}
[[!redirects relevance logics]] [[!redirects relevant logic]] [[!redirects relevant logics]]



\end{document}