recitation-source.tex

\documentclass{article}
\usepackage{libertine}
\usepackage[usenames,dvipsnames,svgnames,table]{xcolor}
\usepackage{amsmath, amssymb, proof, microtype, hyperref}
\usepackage{mathpartir} % for mathpar, not for proofs

\usepackage{perfectcut}
\newcommand\Parens[1]{\perfectparens{#1}}
\newcommand\Squares[1]{\perfectbrackets{#1}}

\newcommand\limplies{\supset}
\newcommand\true[1]{#1\ \textit{true}}

\newcommand\Intro[1]{{#1}\textsf{I}}
\newcommand\Elim[1]{{#1}\textsf{E}}


\setlength{\fboxsep}{1pt}%

\newcommand\Highlight[2]{
  \fcolorbox{#1!30}{#1!10}{$\displaystyle #2$}%
}

\newcommand\Reduce[2]{%
  {#1}%
  \quad
  \longrightarrow_{\mathsf{R}}%
  \quad%
  {#2}%
}

%aligned
\newcommand\AReduce[2]{%
  {#1}%
  &\longrightarrow_{\mathsf{R}}%
  {#2}%
}


\newcommand\Expand[2]{%
  {#1}%
  \quad
  \longrightarrow_{\mathsf{E}}%
  \quad%
  {#2}%
}

\newcommand\AExpand[2]{%
  {#1}%
  &\longrightarrow_{\mathsf{E}}%
  {#2}%
}


\newcommand\Pair[2]{\perfectunary{CurrentHeight}{\langle}{\rangle}{{#1},{#2}}}
\newcommand\Fst[1]{\mathsf{fst}\Parens{#1}}
\newcommand\Snd[1]{\mathsf{snd}\Parens{#1}}
\newcommand\Inl[1]{\mathsf{inl}\Parens{#1}}
\newcommand\Inr[1]{\mathsf{inr}\Parens{#1}}
\newcommand\Fn[2]{\mathsf{fn}\ {#1}\Rightarrow{#2}}

\newcommand\Case[5]{%
  \mathsf{case}\ {#1}\ \mathsf{of}\ \Inl{#2}\Rightarrow{#3}\mid\Inr{#4}\Rightarrow{#5}%
}

\newcommand\Subst[3]{
  \perfectbinary{IncreaseHeight}{[}{/}{]}{#1}{#2}#3
}


\RequirePackage{xcolor}

\title{Recitation 3: Harmony}
\author{Course Staff}
\date{}

\begin{document}
\maketitle

Proof-theoretic harmony is a necessary, but not sufficient, condition
for the well-behavedness of a logic; harmony ensures that the
connectives are \emph{locally} well-behaved, and is closely related to
the critical cases of cut and identity elimination which we may
discuss later on. Therefore, when designing or extending a logic,
checking harmony is a first step.

From the verificationist standpoint, a connective is \emph{harmonious}
if its elimination rules are neither too strong nor too weak in
relation to its introduction rules. The first condition is called
\emph{local soundness} and the second condition is called \emph{local
  completeness}. The content of the soundness condition is a method to
reduce or simplify proofs, and the content of completeness is a method
to expand any arbitrary proof into a canonical proof (i.e.\ one that
ends in an introduction rule).

\section{Conjunction}

Local soundness for conjunction is witnessed by the following two
reduction rules:
\begin{mathpar}
  \Reduce{
    \infer[\Elim{\land}_1]{
      A\true%
    }{
      \infer[\Intro{\land}]{
        A\land{}B\true%
      }{
        \Highlight{Red}{
          \deduce{A\true}{\mathcal{D}}
        }
        &
        \deduce{B\true}{\mathcal{E}}
      }
    }
  }{
    \Highlight{Red}{
      \deduce{A\true}{\mathcal{D}}
    }
  }
  \\
  \Reduce{
    \infer[\Elim{\land}_2]{
      B\true%
    }{
      \infer[\Intro{\land}]{
        A\land{}B\true%
      }{
        \deduce{A\true}{\mathcal{D}}
        &
        \Highlight{Red}{\deduce{B\true}{\mathcal{E}}}
      }
    }
  }{
    \Highlight{Red}{
      \deduce{B\true}{\mathcal{E}}
    }
  }
\end{mathpar}

Local completeness is witnessed by the following expansion rule:
\begin{mathpar}
  \Expand{
    \Highlight{Red}{\deduce{A\land{}B\true}{\mathcal{D}}}
  }{
    \infer[\Intro{\land}]{
      A\land{}B\true%
    }{
      \infer[\Elim{\land}_1]{
        A\true%
      }{
        \Highlight{Red}{\deduce{A\land{}B\true}{\mathcal{D}}}
      }
      &
      \infer[\Elim{\land}_2]{
        B\true%
      }{
        \Highlight{Red}{\deduce{A\land{}B\true}{\mathcal{D}}}
      }
    }
  }
\end{mathpar}

When regarded as generating relations on \emph{programs} rather than
proofs, the reduction and expansion rules can be recast into another
familiar format:
\begin{align*}
  \AReduce{\Fst{\Pair{\Highlight{Red}{M}}{N}}}{\Highlight{Red}{M}}
  \\
  \AReduce{\Snd{\Pair{M}{\Highlight{Red}{N}}}}{\Highlight{Red}{N}}
  \\
  \AExpand{\Highlight{Red}{M}}{
    \Pair{
      \Fst{\Highlight{Red}{M}}
    }{
      \Snd{\Highlight{Red}{M}}
    }
  }
\end{align*}

\section{Disjunction}

Instructions: present local soundness for proofs, and ask the students
to come up with the version for programs. Next, elicit from the students
both local completeness for programs and for proofs.

\begin{align*}
  \AReduce{
    \infer[\Elim{\lor}^{u,v}]{
      C\true%
    }{
      \infer[\Intro{\lor}_1]{
        A\lor{}B\true%
      }{
        \Highlight{Red}{
          \deduce{A\true}{\mathcal{D}}
        }
      }
      &
      \Highlight{Blue}{
        \deduce[\mathcal{E}]{
          C\true%
        }{
          \infer[u]{
            A\true
          }{
          }
        }
      }
      &
      \deduce[\mathcal{F}]{
        C\true%
      }{
        \infer[v]{
          B\true
        }{
        }
      }      
    }
  }{
    \Highlight{Blue}{
      \deduce[\mathcal{E}]{
        C\true%
      }{
        \infer[u]{
          A\true%
        }{
          \Highlight{Red}{
            \mathcal{D}
          }
        }
      }
    }
  }
  \\
  \AReduce{
    \infer[\Elim{\lor}^{u,v}]{
      C\true%
    }{
      \infer[\Intro{\lor}_2]{
        A\lor{}B\true%
      }{
        \Highlight{Red}{
          \deduce{B\true}{\mathcal{D}}
        }
      }
      &
      \deduce[\mathcal{E}]{
        C\true%
      }{
        \infer[u]{
          A\true
        }{
        }
      }
      &
      \Highlight{Blue}{
        \deduce[\mathcal{F}]{
          C\true%
        }{
          \infer[v]{
            B\true
          }{
          }
        }      
      }
      \quad
    }
  }{
    \Highlight{Blue}{
      \deduce[\mathcal{F}]{
        C\true%
      }{
        \infer[v]{
          B\true%
        }{
          \Highlight{Red}{
            \mathcal{D}
          }
        }
      }
    }
  }
  \\
  \AReduce{
    \Case{
      \Inl{\Highlight{Red}{M}}
    }{u}{
      \Highlight{Blue}{L}
    }{v}{R}
  }{
    \Highlight{Blue}{
      \Subst{\Highlight{Red}{M}}{u}{L}
    }
  }
  \\
  \AReduce{
    \Case{
      \Inr{\Highlight{Red}{M}}
    }{u}{L}{v}{
      \Highlight{Blue}{R}
    }
  }{
    \Highlight{Blue}{
      \Subst{\Highlight{Red}{M}}{v}{R}
    }
  }
\end{align*}

\begin{align*}
  \AExpand{
    \Highlight{Red}{
      \deduce{A\lor{}B\true}{\mathcal{D}}%
    }
  }{
    \infer[\Elim{\lor}^{u,v}]{
      A\lor{}B\true%
    }{
      \Highlight{Red}{
        \deduce{A\lor{}B\true}{\mathcal{D}}%
      }
      &
      \infer[\Intro{\lor}_1]{
        A\lor{}B\true%
      }{
        A\true%
      }
      &
      \infer[\Intro{\lor}_2]{
        A\lor{}B\true%
      }{
        B\true%
      }
    }
  }
  \\
  \AExpand{
    \Highlight{Red}{M}
  }{
    \Case{
      \Highlight{Red}{M}
    }{u}{\Inl{u}}{v}{\Inr{v}}
  }
\end{align*}

\section{Implication}

Elicit both local soundness and local completeness from students in
both proof and program notation.

\begin{align*}
  \AReduce{
    \infer[\Elim{\limplies}]{
      B
    }{
      \infer[\Intro{\limplies}^u]{
        A\limplies{}B\true%
      }{
        \Highlight{Red}{
          \deduce[\mathcal{D}]{
            B\true%
          }{
            \infer[u]{
              A\true%
            }{
            }
          }
        }
      }
      &
      \Highlight{Blue}{\deduce{A\true}{\mathcal{E}}}
    }
  }{
    \Highlight{Red}{
      \deduce[\mathcal{D}]{
        B\true%
      }{
        \infer[u]{
          A\true%
        }{
          \Highlight{Blue}{\mathcal{E}}
        }
      }
    }
  }
  \\
  \AReduce{
    \Parens{\Fn{u}{\Highlight{Red}{M}}}\Parens{\Highlight{Blue}{N}}
  }{
    \Highlight{Red}{\Subst{\Highlight{Blue}{N}}{u}{M}}
  }
\end{align*}

\begin{align*}
  \AExpand{
    \Highlight{Red}{\deduce{A\limplies{}B\true}{\mathcal{D}}}
  }{
    \infer[\Intro{\limplies}^u]{
      A\limplies{}B\true%
    }{
      \infer[\Elim{\limplies}]{
        B\true%
      }{
        \Highlight{Red}{\deduce{A\limplies{}B\true}{\mathcal{D}}}
        &
        \infer[u]{
          A\true%
        }{
        }
      }
    }
  }
  \\
  \AExpand{
    \Highlight{Red}{M}
  }{
    \Fn{u}{\Highlight{Red}{M}\Parens{u}}
  }
\end{align*}

\section{Experiment: Alternative Implication}
\newcommand\LetApp[4]{\mathsf{let}\ {#1} = {#2}\Parens{#3}\ \mathsf{in}\ #4}

What if we replaced the $\Elim{\limplies}$ rule with the following elimination rule:
\[
  \infer[\Elim{\limplies}^u]{
    C\true%
  }{
    A\limplies{}B\true%
    &
    A\true%
    &
    \infer*{
      C\true%
    }{
      \infer[u]{
        B\true%
      }{
      }
    }
  }
\]

The program/proof term assignment is as follows:
\[
  \infer[\Elim{\limplies}^u]{
    \LetApp{u}{L}{M}{N}:C%
  }{
    L:A\limplies{}B%
    &
    M:A%
    &
    \infer*{
      N:C%
    }{
      \infer[u]{
        u:B%
      }{
      }
    }
  }
\]


Can we show local soundness and completeness for this version of the
implication connective?

\begin{align*}
  \AReduce{
    \infer[\Elim{\limplies}^u]{
      C\true
    }{
      \infer[\Intro{\limplies}^v]{
        A\limplies{}B\true%
      }{
        \Highlight{Red}{
          \deduce[\mathcal{D}]{B\true}{
            \infer[v]{A\true}{}
          }
        }
      }
      &
      \Highlight{Blue}{\deduce{A\true}{\mathcal{E}}}
      &
      \Highlight{Green}{
        \deduce[\mathcal{F}]{C\true}{
          \infer[u]{B\true}{}
        }
      }
      \quad
    }
  }{
    \Highlight{Green}{
      \deduce[\mathcal{F}]{C\true}{
        \infer[u]{B\true}{
          \Highlight{Red}{
            \deduce[\mathcal{D}]{B\true}{
              \infer[v]{A\true}{
                \Highlight{Blue}{\deduce{A\true}{\mathcal{E}}}
              }
            }
          }
        }
      }
    }
  }
  \\
  \AReduce{
    \LetApp{u}{
      \Highlight{Red}{\Fn{v}{L}}
    }{
      \Highlight{Blue}{M}
    }{
      \Highlight{Green}{N}
    }
  }{
    \Highlight{Green}{
      \Subst{
        \Highlight{Red}{
          \Subst{\Highlight{Blue}{M}}{v}{L}
        }
      }{u}{N}
    }
  }
\end{align*}

\begin{align*}
  \AExpand{
    \Highlight{Red}{
      \deduce{A\limplies{}B\true}{\mathcal{D}}
    }
  }{
    \infer[\Intro{\limplies}^u]{
      A\limplies{}B\true%
    }{
      \infer[\Elim{\limplies}^v]{
        B\true%
      }{
        \Highlight{Red}{
          \deduce{A\limplies{}B\true}{\mathcal{D}}
        }
        &
        \infer[u]{
          A\true%
        }{}
        &
        \infer[v]{
          B\true%
        }{}
      }
    }
  }
  \\
  \AExpand{
    \Highlight{Red}{M}
  }{
    \Fn{u}{
      \LetApp{v}{
        \Highlight{Red}{M}
      }{u}{v}
    }
  }
\end{align*}

\end{document}

Your indentation is unreadable.

@jozefg at least my typesetting is not literally one BIG bad hbox