\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*{multiplicative disjunction}

\hypertarget{multiplicative_disjunction}{}\section*{{Multiplicative disjunction}}\label{multiplicative_disjunction}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak
\noindent\hyperlink{explanations}{Explanations}\dotfill \pageref*{explanations} \linebreak
\noindent\hyperlink{in_terms_of_resources}{In terms of resources}\dotfill \pageref*{in_terms_of_resources} \linebreak
\noindent\hyperlink{as_a_delayed_or_nondeterministic_choice}{As a delayed or nondeterministic choice}\dotfill \pageref*{as_a_delayed_or_nondeterministic_choice} \linebreak
\noindent\hyperlink{in_game_semantics}{In game semantics}\dotfill \pageref*{in_game_semantics} \linebreak
\noindent\hyperlink{disentangling_additivity_from_disjunctive_syllogism}{Disentangling additivity from disjunctive syllogism}\dotfill \pageref*{disentangling_additivity_from_disjunctive_syllogism} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak


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

In [[linear logic]]/[[linear type theory]], and also sometimes in other [[substructural logics]] such as [[relevance logic]], the \textbf{multiplicative disjunction} (also called \textbf{negative disjunction}, \textbf{intensional disjunction}, or \textbf{fission}) is a [[logical connective]] that is [[dual]] to the [[multiplicative conjunction]]. In linear logic it is often written following Girard as $A\invamp B$, but a multitude of other symbols have also been used for it, including $\oplus,\bullet,\odot,\Box,\sharp,*$.

It is probably the rarest of the binary connectives of linear logic to appear semantically. The additive conjunction and additive disjunction are categorically [[products]] and [[coproducts]], while the [[multiplicative conjunction]] is the [[tensor product]] of a [[monoidal category]] and the [[linear implication]] is the [[internal-hom]] of a [[closed category]]; but the multiplicative disjunction only appears nontrivially (i.e. without coinciding with one of the others) in a [[star-autonomous category]] (or more generally a [[linearly distributive category]]) that is not [[compact closed category|compact]]. Syntactically, this means that it mainly appears when the multiplicative connectives are ``classical'', i.e. the multiplicative [[negation]] is involutive.

It is probably also the hardest to understand intuitively of any of the linear logic connectives. We include several intuitive explanations below.

\hypertarget{definition}{}\subsection*{{Definition}}\label{definition}

In terms of the [[multiplicative conjunction]] $\otimes$ and an involutive multiplicative [[negation]] $\neg$, the multiplicative disjunction can be defined as

\begin{displaymath}
A \invamp B \coloneqq \neg (\neg A \otimes \neg B)
\end{displaymath}
Categorically, this means that it is obtained from the tensor product in a [[star-autonomous category]] by applying the self-duality.

When classical linear logic is expressed with multiple-conclusion [[sequent calculus]], its left and right rules are

\begin{displaymath}
\frac{\Gamma \vdash \Delta,A,B}{\Gamma \vdash \Delta, A\invamp B}  \qquad 
\frac{\Gamma,A \vdash \Delta \quad \Gamma',B\vdash \Delta'}{\Gamma,\Gamma',A\invamp B \vdash \Delta,\Delta'}
\end{displaymath}
\hypertarget{explanations}{}\subsection*{{Explanations}}\label{explanations}

Here we collect some possible ways to understand $\invamp$ intuitively.

\hypertarget{in_terms_of_resources}{}\subsubsection*{{In terms of resources}}\label{in_terms_of_resources}

When linear logic is interpreted as tracking the usage of resources, we can interpret $A\invamp B$ as saying that only one of $A$ or $B$ will happen, but we don't know which, so we have to allocate enough resources to deal with each of them separately. For example, a military general who knows that he will be attacked from either the east or the north must divide his forces between both fronts, even if the attack will only come from one direction; thus what he has is ``attack from east $\invamp$ attack from north''. (If he had spies out that would be able to inform him in advance where the attack was coming from so that he could concentrate his forces there, then he would instead have an additive disjunction ``attack from east $\oplus$ attack from north''.)

\hypertarget{as_a_delayed_or_nondeterministic_choice}{}\subsubsection*{{As a delayed or nondeterministic choice}}\label{as_a_delayed_or_nondeterministic_choice}

Relatedly, we can interpret $A\invamp B$ as a ``delayed choice'' $A$ and $B$. That is, if I give you $A\invamp B$, then it might appear at first that what I gave you is $A$, but as you proceed to make use of $A$ I might change my mind and decide that really I wanted to give you $B$ instead. This can also be regarded as a ``nondeterministic'' choice, so that your responses to being given $A$ or $B$ have to proceed in parallel.

In particular, note that in classical linear logic it is the multiplicative disjunction, not the additive one, that is ``classical'' in the sense that it satisfies [[excluded middle]]:

\begin{displaymath}
\vdash A \invamp \neg A
\end{displaymath}
We don't have $A\oplus \neg A$ because, as in [[constructive mathematics]], we can't decide which of $A$ or $\neg A$ might hold. But we can say $A \invamp \neg A$ because that allows us to delay making a choice until we have enough information. This is similar to how constructively we can say $\neg\neg(A\vee \neg A)$ by a ``continuation-passing'' argument (see [[excluded middle]] for details).

\hypertarget{in_game_semantics}{}\subsubsection*{{In game semantics}}\label{in_game_semantics}

Imagine we play two parallel games of chess, where person A is playing white in one game and black in the other. If both players play the ``copycat strategy'', i.e. wait for the other one to open in one game and ``copy'' their moves to the other game, then we have a deadlock. In order for two simultaneous games to proceed, one player has to play

\begin{displaymath}
Chess \otimes \neg Chess
\end{displaymath}
and the other

\begin{displaymath}
Chess \invamp \neg Chess
\end{displaymath}
Here $Chess$ is the game from the perspective of white, so that the negation $\neg Chess$ is the perspective of black, and $\otimes$ denotes the [[multiplicative conjunction]]. Note that both players are playing both games --- although $\invamp$ is a disjunction, it has certain ``conjunctive properties''. But the person playing $Chess \invamp \neg Chess$ is in the stronger position, because they can play copycat in this situation, i.e. they can wait for the other to move, whereas the person playing $Chess \otimes \neg Chess$ has to play as soon as it's their turn in one of the games.

Another, stronger interpretation is that in $A\otimes B$ we can not use any information from A to play B, and vice versa, so A and B are played by two non-communicating threads. So in a sense, linear logic is a type system for concurrent processes that allows to avoid dead-locks.

\hypertarget{disentangling_additivity_from_disjunctive_syllogism}{}\subsubsection*{{Disentangling additivity from disjunctive syllogism}}\label{disentangling_additivity_from_disjunctive_syllogism}

The basic rules for proving and using a disjunction $A\vee B$ in [[intuitionistic logic]] are \emph{additivity} and \emph{proof by cases}.

\begin{itemize}%
\item If we can prove $A$, we can prove $A\vee B$. Dually, if we can prove $B$, we can prove $A\vee B$.
\item If we have $A\vee B$, then we can split any proof into two cases, assuming $A$ in one and $B$ in the other.

\end{itemize}
These are also a correct set of rules for disjunction in [[classical logic]], but an equivalent pair of rules is based instead on the [[disjunctive syllogism]]:

\begin{itemize}%
\item If assuming $\neg A$ we can prove $B$, then we can prove $A\vee B$. Dually, if assuming $\neg B$ we can prove $A$, we can prove $A\vee B$.
\item If we have $A\vee B$ and also $\neg A$, then we can conclude $B$. Dually, if we have $A\vee B$ and also $\neg B$, then we can conclude $A$.

\end{itemize}
In linear logic, these two sets of rules are no longer equivalent: additivity and proof by cases characterize the [[additive disjunction]], while the disjunctive syllogism rules characterize the multiplicative disjunction.

In particular, note that the traditional argument for [[ex contradictione quodlibet]] depends fundamentally on having a single disjunction that obeys both additivity and the disjunctive syllogism. (More simply, linear logic also distinguishes between the additive [[falsity]] --- the unit for the additive disjunction --- which satisfies [[ex falso quodlibet]], and the multiplicative falsity --- the unit for the multiplicative disjunction --- which doesn't.) Thus, one might expect linear logic to be a [[paraconsistent logic]], and indeed it is (in an appropriate sense).

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

[[!include logic symbols -- table]]

[[!redirects multiplicative disjunction]] [[!redirects multiplicative disjunctions]] [[!redirects intensional disjunction]] [[!redirects intensional disjunctions]] [[!redirects negative disjunction]] [[!redirects negative disjunctions]] [[!redirects fission]]



\end{document}