excerpt.tex

\section{Focused Sequent Calculus}

Focused sequent calculus has several class of proposition\footnote{We are
writing $\Neg{a},\Pos{a}$ for negative and positive atoms respectively. You may
also see these written as $\Neg{P},\Pos{P}$.} and context. We summarize them
below, noting that $\Pos{\Omega}$ ranges over ordered lists, whereas $\Gamma$
ranges over multisets:
\begin{grammar}
  negative & \Neg{A} &
  \Neg{a} \mid \NegTop \mid \NegAnd{\Neg{A}}{\Neg{B}} \mid \Imp{\Pos{A}}{\Neg{B}} \mid \Up{\Pos{A}}
  \\
  positive & \Pos{A} &
  \Pos{a} \mid \PosTop \mid \Bot \mid \PosAnd{\Pos{A}}{\Pos{B}} \mid \Or{\Pos{A}}{\Pos{B}} \mid \Down{\Neg{A}}
  \\
  inv.\ antecedents & \InvCx & \cdot \mid \InvCx,\Pos{A}
  \\
  stable antecedents & \Gamma & \cdot \mid \Gamma,\Neg{A} \mid \Gamma,\Pos{a}
  \\
  stable succedent & \rho & \Pos{A} \mid \Neg{a}
  \\
\end{grammar}

Focused sequent calculus features several forms of judgment:
\begin{judgment-summary}
  right inversion & \RInv
  \\
  left inversion & \LInv
  \\
  stable & \Stab
  \\
  right focus & \RFoc
  \\
  left focus & \LFoc
\end{judgment-summary}

\paragraph{Right inversion}
\begin{mathpar}
  \infer[\Right{a}]{
    \RInv{\Neg{a}}
  }{
    \LInv{\Neg{a}}
  }
  \and
  \infer[\Right{\Up}]{
    \RInv{\Up{\Pos{A}}}
  }{
    \LInv{\Pos{A}}
  }
  \and
  \infer[\Right{\Imp}]{
    \RInv[\InvCx]{\Imp{\Pos{A}}{\Neg{B}}}
  }{
    \RInv[\InvCx,\Pos{A}]{\Neg{B}}
  }
  \and
  \infer[\Right{\NegAnd}]{
    \RInv{\NegAnd{\Neg{A}}{\Neg{B}}}
  }{
    \RInv{\Neg{A}}
    &
    \RInv{\Neg{B}}
  }
  \and
  \infer[\Right{\NegTop}]{
    \RInv{\NegTop}
  }{
  }
\end{mathpar}


\paragraph{Left inversion}
\begin{mathpar}
  \infer[\RuleStable]{
    \LInv{\cdot}
  }{
    \Stab
  }
  \and
  \infer[\Left{a}]{
    \LInv<\Gamma>{\InvCx,\Pos{a}}
  }{
    \LInv<\Gamma,\Pos{a}>{\InvCx}
  }
  \and
  \infer[\Left{\Down}]{
    \LInv<\Gamma>{\InvCx,\Down{\Neg{A}}}
  }{
    \LInv<\Gamma,\Neg{A}>{\InvCx}
  }
  \and
  \infer[\Left{\Top}]{
    \LInv{\InvCx,\Top}
  }{
    \LInv{\InvCx}
  }
  \and
  \infer[\Left{\Bot}]{
    \LInv{\InvCx,\Bot}
  }{
  }
  \and
  \infer[\Left{\Or}]{
    \LInv{\InvCx,\Or{\Pos{A}}{\Pos{B}}}
  }{
    \LInv{\InvCx,\Pos{A}}
    &
    \LInv{\InvCx,\Pos{B}}
  }
  \and
  \infer[\Left{\PosAnd}]{
    \LInv{\InvCx,\PosAnd{\Pos{A}}{\Pos{B}}}
  }{
    \LInv{\InvCx,\Pos{A},\Pos{B}}
  }
\end{mathpar}


\paragraph{Stable}
\begin{mathpar}
  \infer[\RuleFocR]{
    \Stab{\Pos{A}}
  }{
    \RFoc{\Pos{A}}
  }
  \and
  \infer[\RuleFocL]{
    \Stab<\Gamma>
  }{
    \Neg{A}\in\Gamma
    &
    \LFoc<\Gamma>{\Neg{A}}
  }
\end{mathpar}


\paragraph{Right focus}

\begin{mathpar}
  \infer[\RuleIdPos]{
    \RFoc{\Pos{a}}
  }{
    \Pos{a}\in\Gamma
  }
  \and
  \infer[\Right{\Down}]{
    \RFoc{\Down{\Neg{A}}}
  }{
    \RInv[\cdot]{\Neg{A}}
  }
  \and
  \infer[\Right{\PosTop}]{
    \RFoc{\PosTop}
  }{
  }
  \and
  \infer[\Right{\Or}_1]{
    \RFoc{\Or{\Pos{A}}{\Pos{B}}}
  }{
    \RFoc{\Pos{A}}
  }
  \and
  \infer[\Right{\Or}_2]{
    \RFoc{\Or{\Pos{A}}{\Pos{B}}}
  }{
    \RFoc{\Pos{B}}
  }
  \and
  \infer[\Right{\PosAnd}]{
    \RFoc{\PosAnd{\Pos{A}}{\Pos{B}}}
  }{
    \RFoc{\Pos{A}}
    &
    \RFoc{\Pos{B}}
  }
\end{mathpar}

\paragraph{Left focus}

\begin{mathpar}
  \infer[\RuleIdNeg]{
    \LFoc{\Neg{a}}{\Neg{a}}
  }{
  }
  \and
  \infer[\Left{\Up}]{
    \LFoc{\Up{\Pos{A}}}
  }{
    \LInv{\Pos{A}}
  }
  \and
  \infer[\Left{\Imp}]{
    \LFoc{\Imp{\Pos{A}}{\Neg{B}}}
  }{
    \RFoc{\Pos{A}}
    &
    \LFoc{\Neg{B}}
  }
  \and
  \infer[\Left{\NegAnd}_1]{
    \LFoc{\NegAnd{\Neg{A}}{\Neg{B}}}
  }{
    \LFoc{\Neg{A}}
  }
  \and
  \infer[\Left{\NegAnd}_2]{
    \LFoc{\NegAnd{\Neg{A}}{\Neg{B}}}
  }{
    \LFoc{\Neg{B}}
  }
\end{mathpar}

macros.sty

\RequirePackage{stmaryrd}
\RequirePackage{perfectcut}
\RequirePackage{xparse}

\NewDocumentCommand\Parens{m}{\perfectparens{#1}}
\NewDocumentCommand\Squares{m}{\perfectbrackets{#1}}

\NewDocumentCommand\limplies{}{\supset}

\NewDocumentCommand\Highlight{O{Red} m}{
  \fcolorbox{#1!30}{#1!5}{$\displaystyle #2$}%
}


\NewDocumentCommand\JdgLbl{m}{\textit{#1}}

\NewDocumentCommand\HypV{m}{#1\ \JdgLbl{valid}}
\NewDocumentCommand\HypT{m}{#1\ \JdgLbl{true}}

\NewDocumentCommand\ModalValid{D<>{\Delta} G{A}}{%
  #1 \vdash #2\ \JdgLbl{valid}%
}

\NewDocumentCommand\ModalTrue{D<>{\Delta} O{\Gamma} G{A}}{%
  #1; #2 \vdash #3\ \JdgLbl{true}%
}

\NewDocumentCommand\ModalPoss{D<>{\Delta} O{\Gamma} G{A}}{%
  #1; #2 \vdash #3\ \JdgLbl{poss}%
}


\NewDocumentCommand\RuleName{m}{\textsf{#1}}
\NewDocumentCommand\Intro{m}{{#1}\RuleName{I}}
\NewDocumentCommand\Elim{m}{{#1}\RuleName{E}}
\NewDocumentCommand\Right{m}{{#1}\RuleName{R}}
\NewDocumentCommand\Left{m}{{#1}\RuleName{L}}

\NewDocumentCommand\InvCx{}{\Pos{\Omega}}
\NewDocumentCommand\RuleFocR{}{\RuleName{focR}}
\NewDocumentCommand\RuleFocL{}{\RuleName{focL}}
\NewDocumentCommand\RuleIdPos{}{\Pos{\RuleName{id}}}
\NewDocumentCommand\RuleIdNeg{}{\Neg{\RuleName{id}}}
\NewDocumentCommand\RuleLax{}{\RuleName{lax}}
\NewDocumentCommand\RuleStable{}{\RuleName{stable}}
\NewDocumentCommand\RuleValid{}{\RuleName{valid}}
\NewDocumentCommand\RulePoss{}{\RuleName{poss}}
\NewDocumentCommand\RuleHypT{}{\RuleName{hyp}}
\NewDocumentCommand\RuleHypV{}{\RuleName{hypv}}

\NewDocumentCommand\GenericModality{m m m}{
  #1\IfValueT{#3}{
    \IfBooleanTF{#2}{\Parens{#3}}{#3}
  }
}

\NewDocumentCommand\LBox{s g}{%
  \GenericModality{\square}{#1}{#2}
}

\NewDocumentCommand\LDia{s g}{%
  \GenericModality{\Diamond}{#1}{#2}
}

\NewDocumentCommand\Lax{s g}{%
  \GenericModality{\bigcirc}{#1}{#2}
}


\NewDocumentCommand\LaxTrue{O{\Gamma} G{A}}{%
  #1 \vdash #2\ \JdgLbl{true}
}

\NewDocumentCommand\LaxLax{O{\Gamma} G{A}}{%
  #1 \vdash #2\ \JdgLbl{lax}
}





\NewDocumentCommand\ldash{}{\mathrel{{\vdash}\kern-0.45em{\vdash}}}

% default ordered context name
\NewDocumentCommand\OCx{}{\Omega} % in case we want to switch the notation

% ordered truth
\NewDocumentCommand\OTrue{O{\OCx} G{A}}{%
  #1 \ldash{}#2\ \JdgLbl{true}
}

\NewDocumentCommand\BinaryConnective{m m m}{
  \IfValueTF{#2}{%
    #2\mathbin{#1}#3%
  }{%
    {#1}%
  }%
}

\NewDocumentCommand\Fuse{g G{}}{%
  \BinaryConnective{\bullet}{#1}{#2}
}

\NewDocumentCommand\Imp{g G{}}{%
  \BinaryConnective{\limplies}{#1}{#2}
}

\NewDocumentCommand\Twist{g G{}}{%
  \BinaryConnective{\circ}{#1}{#2}
}

\NewDocumentCommand\Tensor{g G{}}{%
  \BinaryConnective{\otimes}{#1}{#2}
}

\NewDocumentCommand\With{g G{}}{%
  \BinaryConnective{\binampersand}{#1}{#2}
}


\NewDocumentCommand\Plus{g G{}}{%
  \BinaryConnective{\oplus}{#1}{#2}
}

\NewDocumentCommand\RImp{g G{}}{%
  \BinaryConnective{\twoheadrightarrow}{#1}{#2}
}

\NewDocumentCommand\LImp{g G{}}{%
  \BinaryConnective{\rightarrowtail}{#1}{#2}
}

\NewDocumentCommand\Lolli{g G{}}{%
  \BinaryConnective{\multimap}{#1}{#2}
}

\NewDocumentCommand{\One}{}{\mathbf{1}}
\NewDocumentCommand{\Zero}{}{\mathbf{0}}
\NewDocumentCommand{\Top}{}{\top}

% usage: \Subst{D}{u}{E} ===> [D/u]E
\NewDocumentCommand\Subst{m m m}{%
  \Squares*{#1/#2}#3%
}




%default linear context name
\NewDocumentCommand\LCx{}{\Gamma} % in case we want to switch the notation

\NewDocumentCommand\LTrue{O{\LCx} G{A}}{%
  #1 \ldash{}#2\ \JdgLbl{true}
}



\NewDocumentEnvironment{grammar}{}{%
  \begin{center}%
    \begin{tabular}{>{\itshape(}l<{)} >{$}l<{$} @{\quad $\Coloneqq$\quad } >{$}l<{$}}%
}{%
    \end{tabular}%
  \end{center}%
}

\NewDocumentEnvironment{judgment-summary}{}{%
  \begin{center}%
    \begin{tabular}{>{\itshape(}l<{)} @{\qquad} >{$}l<{$}}%
}{%
    \end{tabular}%
  \end{center}%
}

\NewDocumentCommand\Pol{m m}{#2^{\color{Gray}#1}}
\NewDocumentCommand\Neg{m}{\Pol{-}{#1}}
\NewDocumentCommand\Pos{m}{\Pol{+}{#1}}

\NewDocumentCommand\Or{g G{}}{\BinaryConnective{\lor}{#1}{#2}}
\NewDocumentCommand\PosAnd{g G{}}{\BinaryConnective{\Pos{\land\!}}{#1}{#2}}
\NewDocumentCommand\NegAnd{g G{}}{\BinaryConnective{\Neg{\land\!}}{#1}{#2}}
\NewDocumentCommand\PosTop{}{\Pos{\top}}
\NewDocumentCommand\Bot{}{\bot}
\NewDocumentCommand\NegTop{}{\Neg{\top}}
\NewDocumentCommand\Up{G{}}{{\uparrow}#1}
\NewDocumentCommand\Down{G{}}{{\downarrow}#1}

\NewDocumentCommand\Mute{m}{{\color{Black!60} #1}}

\NewDocumentCommand\SequentArrow{o}{%
  \IfValueTF{#1}{%
    \stackrel{{\color{RoyalBlue}\mathsf{#1}}}{\longrightarrow}%
  }{%
    \mathrel{\longrightarrow}%
  }%
}

\NewDocumentCommand\RInv{D<>{\Gamma} O{\Pos{\Omega}} G{\Neg{A}}}{%
  \Mute{#1}; \Mute{#2} \SequentArrow[R] #3
}

\NewDocumentCommand\LInv{D<>{\Gamma} G{\Pos{\Omega}} G{\rho}}{%
  \Mute{#1}; {#2} \SequentArrow[L] \Mute{#3}
}

\NewDocumentCommand\Stab{D<>{\Gamma} G{\rho}}{%
  {#1} \SequentArrow #2
}

\NewDocumentCommand\Focus{m}{
  {\color{FireBrick}\Squares{#1}}
}

\NewDocumentCommand\RFoc{D<>{\Gamma} G{\Pos{A}}}{%
  \Mute{#1} \SequentArrow \Focus{#2}
}

\NewDocumentCommand\LFoc{D<>{\Gamma} G{\Neg{A}} G{\rho}}{%
  \Mute{#1},\Focus{#2} \SequentArrow \Mute{#3}
}