lplfitch.dtx

% \iffalse meta-comment
%
% Copyright (C) 2013 by John Etchemendy, Dave Barker-Plummer, 
% and Richard Zach
% -------------------------------------------------------
% 
% This work may be distributed and/or modified under the
% conditions of the LaTeX Project Public License, either version 1.3
% of this license or (at your option) any later version.
% The latest version of this license is in
%   http://www.latex-project.org/lppl.txt
% and version 1.3 or later is part of all distributions of LaTeX
% version 2005/12/01 or later.
%
% \fi
%
% \iffalse
%<*driver>
\ProvidesFile{lplfitch.dtx}
%</driver>
%<package>\NeedsTeXFormat{LaTeX2e}[1999/12/01]
%<package>\ProvidesPackage{lplfitch}
%<*package>
    [2013/05/16 v0.9 LPL Fitch style]
%</package>
%
%<*driver>
\documentclass{ltxdoc}
\usepackage{lplfitch}[2013/05/16]
\usepackage{hyperref}
\EnableCrossrefs         
\CodelineIndex
\RecordChanges
\begin{document}
  \DocInput{lplfitch.dtx}
  \PrintChanges
  \PrintIndex
\end{document}
%</driver>
% \fi
%
% \CheckSum{0}
%
% \CharacterTable
%  {Upper-case    \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z
%   Lower-case    \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z
%   Digits        \0\1\2\3\4\5\6\7\8\9
%   Exclamation   \!     Double quote  \"     Hash (number) \#
%   Dollar        \$     Percent       \%     Ampersand     \&
%   Acute accent  \'     Left paren    \(     Right paren   \)
%   Asterisk      \*     Plus          \+     Comma         \,
%   Minus         \-     Point         \.     Solidus       \/
%   Colon         \:     Semicolon     \;     Less than     \<
%   Equals        \=     Greater than  \>     Question mark \?
%   Commercial at \@     Left bracket  \[     Backslash     \\
%   Right bracket \]     Circumflex    \^     Underscore    \_
%   Grave accent  \`     Left brace    \{     Vertical bar  \|
%   Right brace   \}     Tilde         \~}
%
%
% \changes{v0.1}{Aeons ago}{Initial version}
% \changes{v0.9}{2012/05/16}{First public beta}
%
% \GetFileInfo{lplfitch.dtx}
%
% \DoNotIndex{\newcommand,\newenvironment}
%
% \title{The \textsf{lplfitch} package\thanks{This document
%   corresponds to \textsf{lplproof}~\fileversion, dated \filedate.}}
% \author{John Etchemendy \and Dave Barker-Plummer \and Richard Zach}
%
% \maketitle
%
% \section{Introduction}
%
% The package |lplfitch| provides macros for typesetting natural
% deduction proofs in ``Fitch'' style, with subproofs indented and
% offset by scope lines.  It produces proofs in the format used in the
% textbook \href{http://lpl.stanford.edu/}{\textit{Language, Proof,
% and Logic}} by Dave Barker-Plummer, Jon Barwise, and John
% Etchemendy.  The package was originally written by John
% Etchemendy. The current version incorporates changes by Dave
% Barker-Plummer and Richard Zach.
%
% \section{Fitch Proofs by Example}
% \label{sect:proofs-by-example}
%
% In this section we will describe how to typeset the Fitch-style
% natural deduction proof shown in figure~\ref{fig:example-proof}.
% This proof uses all of the macros that we have developed for
% typesetting proofs and therefore serves as a good illustration.
%
% \begin{figure}
% \fitchprf{}{
%     \subproof{\pline[1.]{\uni{x}{(Cube(x)\lif Small(x))}}}{
%         \subproof{\pline[2.]{\exi{x}{Cube(x)}}}{
%             \boxedsubproof[3.]{a}{Cube(a)}{
%                 \pline[4.]{Cube(a)\lif Small(a)}[\lalle{1}]\\
%                 \pline[5.]{Small(a)}[\life{4}{3}]\\
%                 \pline[6.]{\exi{x}{Small(x)}}[\lexii{5}]
%             }
%             \pline[7.]{\exi{x}{Small(x)}}[\lexie{2}{3--6}]
%         }
%         \pline[8.]{\exi{x}{Cube(x)}\lif \exi{x}{Small(x)}}[\lifi{2--7}]
%     }
%     \pline[9.]{\brokenform{(\uni{x}{(Cube(x)\lif Small(x))}\lif}{
%         \formula{(\exi{x}{Cube(x)} \lif \exi{x}{Small(x)})}}}[\lifi{1--8}] 
% }
% \caption{An Example Proof}
% \label{fig:example-proof}
% \end{figure}
%
% The commands for producing this proof are given in
% figure~\ref{fig:proof-eg-cmds}.  This proof is a little hard to take
% in all at once, and so in the remainder of this section we will
% describe the development of this proof, which we hope is of use to
% readers.
%
%\begin{figure}
%\begin{verbatim}
% \fitchprf{}{
%     \subproof{\pline[1.]{\uni{x}{(Cube(x)\lif Small(x))}}}{
%         \subproof{\pline[2.]{\exi{x}{Cube(x)}}}{
%             \boxedsubproof[3.]{a}{Cube(a)}{
%                 \pline[4.]{Cube(a)\lif Small(a)}[\lalle{1}]\\
%                 \pline[5.]{Small(a)}[\life{4}{3}]\\
%                 \pline[6.]{\exi{x}{Small(x)}}[\lexii{5}]
%             }
%             \pline[7.]{\exi{x}{Small(x)}}[\lexie{2}{3--6}]
%         }
%         \pline[8.]{\exi{x}{Cube(x)}\lif \exi{x}{Small(x)}}[\lifi{2--7}]
%     }
%     \pline[9.]{\brokenform{(\uni{x}{(Cube(x)\lif Small(x))}\lif}{
%         \formula{(\exi{x}{Cube(x)} \lif \exi{x}{Small(x)})}}}[\lifi{1--8}] 
% }
% \end{verbatim}
% \caption{The commands for producing the proof of
% figure~\ref{fig:example-proof}}
% \label{fig:proof-eg-cmds}
% \end{figure}
%
% We recommend developing the commands to typeset a proof from the
% inside out, starting with the most deeply nested subproof.  We also
% recommend ignoring justifications until the proof is complete,
% primarily for simplicity but also because the line numbers are not
% known until the complete proof structure is present.
%
% We begin by writing the lines of the innermost subproof (lines 3--6
% of the main proof).
%
% \begin{quote}
% \begin{tabular}{ll}
% |\pline{Cube(a)}| & \formula{Cube(a)}\\
% |\pline{Cube(a)\lif Small(a)}| & \formula{Cube(a)\lif Small(a)}\\
% |\pline{Small(a)}| & \formula{Small(a)}\\
% |\pline{\exi{x}{Small(x)}}| & \formula{\exi{x}{Small(x)}}
% \end{tabular}
% \end{quote}
%
% The macro |\pline| produces a single line of the proof.  The
% mandatory argument to |\pline| is the formula to appear within the
% step.  You will notice that we have used the macro |\lif| to produce
% an conditional arrow, and |\exi| to produce an existentially
% quantified formula.  These are members of a suite of macros that we
% find convenient for producing formulae.  These are described in
% section~\ref{sect:formulae}.
%
% The |\pline| macro may only be used inside a proof context.  We
% construct such a context by using the |\fitchprf| macro.  This macro
% has two mandatory arguments, corresponding to the premises and the
% body of the proof.  Each argument is a list of lines, separated by a
% newline (|\\|) command.  We therefore embed the lines of our example
% proof like this:
%
% \begin{verbatim}
% \fitchprf{\pline{Cube(a)}}{
%     \pline{Cube(a) \lif Small(a)}\\
%     \pline{Small(a)}\\
%     \pline{\exi{x}{Small(x)}}
% }\end{verbatim}
%
% Typesetting a document containing this command results in
% the proof:
% \begin{quote}
% \fitchprf{\pline{Cube(a)}}{
%     \pline{Cube(a) \lif Small(a)}\\
%     \pline{Small(a)}\\
%     \pline{\exi{x}{Small(x)}}
% }
% \end{quote}
%
% Our next step is to embed this proof as a subproof within the larger
% proof.  This is simply achieved.  We first change the use of
% |\fitchprf| to a |\subproof| command, and then treat this as a line
% of the body of another |\fitchprf| command.  The result of doing
% this is:
%
% \begin{verbatim}
% \fitchprf{\pline{\exi{x}{Cube(x)}}}{
%     \subproof{\pline{Cube(a)}}{
%         \pline{Cube(a)\lif Small(a)}\\
%         \pline{Small(a)}\\
%         \pline{\exi{x}{Small(x)}}
%     }
%     \pline{\exi{x}{Small(x)}}
% }\end{verbatim}
%
% \noindent which yields the proof:
%
% \begin{quote}
% \fitchprf{\pline{\exi{x}{Cube(x)}}}{
%     \subproof{\pline{Cube(a)}}{
%         \pline{Cube(a)\lif Small(a)}\\
%         \pline{Small(a)}\\
%         \pline{\exi{x}{Small(x)}}
%     }
%     \pline{\exi{x}{Small(x)}}
% }
% \end{quote}
%
% \noindent The new outer |\fitchprf| has two elements in the second
% argument, one of which is the subproof that we just wrote and the
% second is a formula.  As we embedded the subproof in the body of the
% main proof we changed the command from |\fitchprf| to |\subproof|,
% the definitions of these two macros are almost identical but for the
% adjustment of vertical spacing after the use of a |\subproof|
% command.  Note that no |\\| command is required after the use of a
% |\subproof| command.
%
% Two further applications of this technique give us the command:
%
% \begin{verbatim}
% \fitchprf{}{
%     \subproof{\pline{\uni{x}{(Cube(x)\lif Small(x))}}}{
%         \subproof{\pline{\exi{x}{Cube(x)}}}{
%             \subproof{\pline{Cube(a)}}{
%                 \pline{Cube(a)\lif Small(a)}\\
%                 \pline{Small(a)}\\
%                 \pline{\exi{x}{Small(x)}}
%             }
%             \pline{\exi{x}{Small(x)}}
%         }
%         \pline{\exi{x}{Cube(x)}\lif \exi{x}{Small(x)}}
%     }
%     \pline{\brokenform{(\uni{x}{(Cube(x)\lif Small(x))}\lif}{
%         \formula{(\exi{x}{Cube(x)} \lif \exi{x}{Small(x)})}}}
% }
% \end{verbatim}
%
% \noindent which produces the proof
%
% \begin{quote}
% \fitchprf{}{
%     \subproof{\pline{\uni{x}{(Cube(x)\lif Small(x))}}}{
%         \subproof{\pline{\exi{x}{Cube(x)}}}{
%             \subproof{\pline{Cube(a)}}{
%                 \pline{Cube(a)\lif Small(a)}\\
%                 \pline{Small(a)}\\
%                 \pline{\exi{x}{Small(x)}}
%             }
%             \pline{\exi{x}{Small(x)}}
%         }
%         \pline{\exi{x}{Cube(x)}\lif \exi{x}{Small(x)}}
%     }
%     \pline{\brokenform{(\uni{x}{(Cube(x)\lif Small(x))}\lif}{
%         \formula{(\exi{x}{Cube(x)} \lif \exi{x}{Small(x)})}}}
% }
% \end{quote}
%
% Notice that the last line contains a long formula, and we have used
% the |\brokenform| command to typeset this formula.  The
% |\brokenform| command takes two arguments, the first is the first
% part of the formula, which will be typeset left justified in the
% space available, while the second argument contains the remaining
% pieces of the formula which will appear in subsequent lines.  These
% lines should be separated by uses of the |\\| command, and each line
% should (usually) be a |\formula|.  These lines will be typeset right
% justified in the available space.
%
% \subsection{Adding Line Numbers}
%
% The |\pline| command takes an optional argument which is the number
% of the line within the proof.  We can simply add these now that we
% have all of the lines of the proof.
%
% \begin{verbatim}
% \fitchprf{}{
%     \subproof{\pline[1.]{\uni{x}{(Cube(x)\lif Small(x))}}}{
%         \subproof{\pline[2.]{\exi{x}{Cube(x)}}}{
%             \subproof{\pline[3.]{Cube(a)}}{
%                 \pline[4.]{Cube(a)\lif Small(a)}\\
%                 \pline[5.]{Small(a)}\\
%                 \pline[6.]{\exi{x}{Small(x)}}
%             }
%             \pline[7.]{\exi{x}{Small(x)}}
%         }
%         \pline[8.]{\exi{x}{Cube(x)}\lif \exi{x}{Small(x)}}
%     }
%     \pline[9.]{\brokenform{(\uni{x}{(Cube(x)\lif Small(x))}\lif}{
%         \formula{(\exi{x}{Cube(x)} \lif \exi{x}{Small(x)})}}}
% }\end{verbatim}
% \noindent which results in the proof:
% \begin{quote}
% \fitchprf{}{
%     \subproof{\pline[1.]{\uni{x}{(Cube(x)\lif Small(x))}}}{
%         \subproof{\pline[2.]{\exi{x}{Cube(x)}}}{
%             \subproof{\pline[3.]{Cube(a)}}{
%                 \pline[4.]{Cube(a)\lif Small(a)}\\
%                 \pline[5.]{Small(a)}\\
%                 \pline[6.]{\exi{x}{Small(x)}}
%             }
%             \pline[7.]{\exi{x}{Small(x)}}
%         }
%         \pline[8.]{\exi{x}{Cube(x)}\lif \exi{x}{Small(x)}}
%     }
%     \pline[9.]{\brokenform{(\uni{x}{(Cube(x)\lif Small(x))}\lif}{
%         \formula{(\exi{x}{Cube(x)} \lif \exi{x}{Small(x)})}}}
% }
% \end{quote}
%
% In the eventual proof, a boxed constant is introduced at line~3.  We
% can convert the simple subproof into a boxed subproof.  We use the
% |\boxedsubproof| macro to achieve this.  The conversion is
% straightforward, we replace the first argument of the |\subproof|
% command which was |{\pline[3.]{Cube(a)}}}| by the three arguments
% |[3.]{a}{Cube(a)}| obtaining
%
% \begin{verbatim}
% \boxedsubproof[3.]{a}{Cube(a)}{
%     \pline[4.]{Cube(a)\lif Small(a)}\\
%     \pline[5.]{Small(a)}\\
%     \pline[6.]{\exi{x}{Small(x)}}
% }\end{verbatim}
%
% \subsection{Adding Justifications}
%
% The final thing that we need to do to complete the desired proof is
% the addition of justifications.  To produce a justified line we need
% to then add the optional justification argument.
%
% \begin{verbatim}\pline[5.]{Small(a)}[\ife{4}{3}]\end{verbatim}
%
% \noindent The \verb|\ife| macro produces a justification using the
% $\lif$-elimination rule of the logic.  This is one of a suite of
% macros that we developed to produce justifications in a uniform
% manner.  These are described in section~\ref{sect:justifications}.
%
% \subsection{Command Reference}
% 
% The |\pline| command can be used to typeset proof lines. It takes
% the formula as a mandatory argument, and line number and
% justification as optional arguments: |\pline|\oarg{line
% number}\marg{formula}\oarg{justification}.  The variant |\fpline|
% works the same, except it produces a focus slider.  In case you want
% to typeset a line in an argument or proof that is not typeset as a
% formula (e.g., plain text), use the |\tline| command. It takes a
% line number as optional argument.
%
% \subsection{Obsolete Commands}
%
% The original version of |lplfitch| set lines of proofs using two
% separate macros, the |\nline| and |\jline| commands.  They are
% superceded by the |\pline| command and are included for backward
% compatibility only.
%
% A numbered line is produced by |\nline|, with the optional argument
% the line number.  A justified line is produced using the
% \verb|\jline| macro, which has one mandatory and one optional
% argument.  The optional argument contains the justification, while
% the mandatory argument must contain {\em all} of the arguments
% previously given to \verb|\nline|.  So the command
%
% \begin{verbatim}\nline[5.]{Small(a)}\end{verbatim}
% 
% \noindent produces exactly the same output as
%
% \begin{verbatim}\jline{[5.]{Small(a)}}\end{verbatim}
% 
% \noindent but notice that both the arguments to \verb|\nline| are
% passed within the single argument to \verb|\jline|. To produce a
% justified line using |\jline|, you would also include the
% justification as an optional argument, say,
%
% \begin{verbatim}\jline{[5.]{Small(a)}}[\life{2}{3}]\end{verbatim}
%
% \section{Logical Formulae}
% \label{sect:formulae}
%
% We set our formulae using sans-serif font and we also need to be in
% math mode because the use of logical connectives.  The
% \verb|\formula| command takes a formula to set as its argument, and
% handles both font and mode change.  If the LPL convention of sans-serif
% formulas is not desired, you can simly redefine |\formula| as
% \begin{verbatim}\renewcommand{\formula}[1]{\ensuremath{#1}}\end{verbatim}
%
% Many of the commands that follow require that they are used in a
% formula, or math, context.
%
% \subsection{Connectives}
%
% We introduce our own (usually) shorter names for logical
% connectives.  All of these commands require a formula context.
%
% \begin{center}
% \begin{tabular}{lc}
% \bf Usage & \bf Output\\
% \hline\\
% \verb|\land| & \formula{\land}\\
% \verb|\lor| & \formula{\lor}\\
% \verb|\lif| & \formula{\lif}\\
% \verb|\liff| & \formula{\liff}\\
% \verb|\lnot| & \formula{\lnot}\\
% \verb|\lfalse| & \formula{\lfalse}\\
% \verb|\lall| & \formula{\lall}\\
% \verb|\lis| & \formula{\lis}
% \end{tabular}
% \end{center}
%
% \subsection{Quantified Formulae}
%
% So that we don't have to think about spacing when setting quantified
% formulae, we defined the commands |\exi| and |\uni|.  Use
% |\exi{x}{P(x)}| to obtain \formula{\exi{x}{P(x)}}, and
% |\uni{x}{\exi{y}{(P(x)\lif Q(x,y))}}| for
% \formula{\uni{x}{\exi{y}{(P(x)\lif Q(x,y))}}}, for example.  |\exi|
% and |\uni| require a formula context.
%
% \section{Justifications}
% \label{sect:justifications}
%
% Here are the macros that we have developed to typeset justifications
% within a proof.  These do not require a formula context.
%
% \begin{center}
% \begin{tabular}{ll}
% \bf Usage & \bf Output\\
% \hline\\
% |\landi{2, 3}| &\landi{2, 3}\\
% |\lande{4}|&\lande{4}\\
% |\lori{5}| & \lori{5}\\
% |\lore{6}{7--9}{11--13}| &\lore{6}{7--9}{11--13}\\
% |\lnoti{14--15}| &\lnoti{14-15}\\
% |\lnote{16}| &\lnote{16}\\
% |\lfalsei{17}{19}| &\lfalsei{17}{19}\\
% |\lfalsee{20}|&\lfalsee{20}\\
% |\lifi{21--25}| &\lifi{21--25}\\
% |\life{27}{30}| &\life{27}{30}\\
% |\liffi{33--37}{40-50}|&\liffi{33--37}{40--50}\\
% |\liffe{55}{57}| &\liffe{55}{57}\\
% |\reit{4}|&\reit{4}\\
% |\eqi| &\eqi\\
% |\eqe{7}{11}|&\eqe{7}{11}\\
% |\lalli{9--12}|&\lalli{9--12}\\
% |\lalle{13}|&\lalle{13}\\
% |\lexii{15}| &\lexii{15}\\
% |\lexie{17}{18-30}| &\lexie{17}{18--30}\\
% \end{tabular}
% \end{center}
%
% \section{Other Macros}
% \label{sect:other-macros}
%
% \subsection{Arguments}
%
% When you want to typeset an argument, for example when setting an
% exercise requiring the proof of some conclusion from a collection of
% premises, you should use the |\fitcharg| command.  This command
% takes two arguments, both mandatory, the premise lines which are set
% above the Fitch bar, and the conclusion lines, which go below.
% Here's an example.  The argument
%
%\begin{quote}
%  \fitcharg{\formula{P(a)}\\ \formula{Q(a)}}{\formula{S(a)}}
%\end{quote}
%
%\noindent is typeset by the command:
%\begin{verbatim}\fitcharg{
%     \formula{P(a)}\\ 
%     \formula{Q(a)}
% }{
%     \formula{S(a)}
% }\end{verbatim}
% \noindent Notice that multiple lines are separated by a use of the
% \LaTeX\ command |\\|.
%
% \subsection{Fitch Contexts}
%
% The |\fitchctx| command is used for setting proof fragments which do
% not include the horizontal Fitch bar.  We use these, for example,
% when formally describing the inference rules of our logic.  The
% command below, for example, typesets our description of the rule of
% conditional proof.
%
% Notice here that we use the command |\ellipsesline| to produce a
% line of the ``proof'' containing a vertical ellipses (using the
% |\pline{\vdots}| results in the ellipses not being centered on the
% line).
%
% Another new feature of this situation is the use of the |\fpline|
% command.  This command works just like the |\pline| command and
% produces exactly what the |\pline| command would, except that a
% focus slider appears to the left of the Fitch bar in question.  The
% |\fpline| command does not work in the argument lines of
% |\fitchprf|  or |\fitcharg|.
%
% \begin{verbatim}
% \fitchctx{
%     \subproof{\pline[$n$.]{P}}{
%         \ellipsesline\\
%         \pline[$m$.]{Q}
%     }
%     \fpline{P \lif Q}[\lifi{$n$--$m$}]
% }
% \end{verbatim}
%
% \begin{quote}
% \fitchctx{
%     \subproof{\pline[$n$.]{P}}{
%         \ellipsesline\\
%         \pline[$m$.]{Q}
%     }
%     \fpline{P \lif Q}[\lifi{$n$--$m$}]
% }
% \end{quote}
%
% \section{Other Packages}
%
% Two other \LaTeX{} packages provide functionality to typeset
% Fitch-style proofs. They differ from |lplfitch| in that they set the
% line numbers close to the left edge of the proof, while |lplfitch|
% sets them close to the formula.  Another difference is that subroofs
% can easily be copied and work the same regardless of the depth of
% nesting.
%
% Peter Selinger's package is
% available at
%\begin{quote}
% \href{http://www.mathstat.dal.ca/~selinger/fitch/}{|http://www.mathstat.dal.ca/\~{
% }selinger/fitch/|},
% \end{quote}
% and that by Johan Kl\"uwer at
% \begin{quote}
% \href{http://folk.uio.no/johanw/FitchSty.html}{|http://folk.uio.no/johanw/FitchSty.html|}.
% \end{quote}
%
% \StopEventually{}
%
% \section{Implementation}
%
%    \begin{macrocode}
\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{lplfitch}[2013/05/07 -- Fitch Proofs a la LPL]
%    \end{macrocode}
%
% \begin{macro}{\formula}
% Typesets a formula (in math mode, letters typeset in sans-serif as in LPL
%    \begin{macrocode}
\newcommand*{\formula}[1]{\ensuremath{\sf{#1}}}
%    \end{macrocode}
% \end{macro}
%
% \subsection{Connectives and Quantifiers}
% We provide convenient and short commands for logical symbols.
%    \begin{macrocode}
\newcommand*\lif{\rightarrow}
\newcommand*\liff{\leftrightarrow}
\newcommand*\lfalse{\bot}
\newcommand*\lall{\forall}
\newcommand*\lis{\exists}
%    \end{macrocode}
% The following provide for commands for setting quantified formulae, inserting correct space
% between variable and formula.  It can be redifined using |\renewcommand| if you want to use them but
% want quantifiers set differently (e.g., with parentheses)
%    \begin{macrocode}
\newcommand*{\quant}[3]{#1 #2\;#3}
\newcommand*{\exi}[2]{\quant{\lis}{#1}{#2}}
\newcommand*{\uni}[2]{\quant{\lall}{#1}{#2}}
%    \end{macrocode}
% \subsection{Justifications}
%
% The folowing commands are used to generate justifications, e.g.,
% |\landi{1, 2}| produces ``\landi{1, 2}''.
%    \begin{macrocode}
\newcommand*\intro[1]{\formula{#1\,}{\bf Intro:}}
\newcommand*\elim[1]{\formula{#1\,}{\bf Elim:}}

\newcommand*\landi[1]{\intro{\land} #1}
\newcommand*\lande[1]{\elim{\land} #1}
\newcommand*\lori[1]{\intro{\lor} #1}
\newcommand*\lore[3]{\elim{\lor} #1, #2, #3}
\newcommand*\lnoti[1]{\intro{\lnot} #1} 
\newcommand*\lnote[1]{\elim{\lnot} #1}

\newcommand*\lfalsei[2]{\intro{\lfalse} #1, #2}
\newcommand*\lfalsee[1]{\elim{\lfalse} #1}

\newcommand*\lifi[1]{\intro{\lif} #1}
\newcommand*\life[2]{\elim{\lif} #1, #2}

\newcommand*\liffi[2]{\intro{\liff} #1, #2}
\newcommand*\liffe[2]{\elim{\liff} #1, #2}

\newcommand*\reit[1]{{\bf Reit:} #1}

\newcommand*\eqi[0]{$=\,${\bf Intro}}
\newcommand*\eqe[2]{\elim{=} #1, #2}

\newcommand*\lalli[1]{\intro{\lall} #1}
\newcommand*\lalle[1]{\elim{\lall} #1}

\newcommand*\lexii[1]{\intro{\lis} #1}
\newcommand*\lexie[2]{\elim{\lis} #1, #2}
%    \end{macrocode}
%
% \subsection{Dimensions}
%
% The following dimensions can be redefined with |\setlength|
%
% \begin{macro}{\fitchargwidth}
% Width of formulas in arguments
%    \begin{macrocode}
\newlength{\fitchargwidth}  
\setlength{\fitchargwidth}{3.5in}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\fitchprfwidth}
% Width of formulas in proofs
%    \begin{macrocode}
\newlength{\fitchprfwidth}
\setlength{\fitchprfwidth}{3.0in}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\fitchctxwidth}
% Width of formulas in Fitch contexts
%    \begin{macrocode}
\newlength{\fitchctxwidth}  
\setlength{\fitchctxwidth}{1in}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\fitchsep}
% Distance between scope line and formula
%    \begin{macrocode}
\newlength{\fitchsep}   
\setlength{\fitchsep}{10pt}
%    \end{macrocode}
% \end{macro}
%
% \subsection{Contexts, Arguments, Proofs}
%
% \begin{macro}{\fitchctx} Typesets a Fitch context, e.g., specification of 
% a rule, in which a focus slider is typeset to the left of the conclusion 
%    \begin{macrocode} 
\newcommand{\fitchctx}[1]{%
	\advance \fitchctxwidth by -\fitchsep%
	\advance \fitchctxwidth by .5pt%
	\begin{tabular}[t]{r@{}|p{\fitchctxwidth}@{}l}
 		\phantom{\slider}  \\[-1.75ex]
 		#1 \\[-1.75ex] & & 
 	\end{tabular}
	\advance \fitchctxwidth by \fitchsep%
	\advance \fitchctxwidth by -.5pt%
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\fitchprf} Typesets a fitch proof
%    \begin{macrocode}
\newcommand{\fitchprf}[2]{%
	\advance \fitchprfwidth by -\fitchsep%
	\advance \fitchprfwidth by .5pt%
	\hspace*{.35em}%
	\begin{tabular}[t]{|p{0pt}@{}p{\fitchprfwidth}@{\hspace*{\fitchsep}}l}
 		\multicolumn{3}{@{}l@{}}{\ }\\[-2.35ex]
		  #1 \\ 
		  \ \\[-2.5ex] \cline{1-1}\\[-2ex]
		  #2 \\ \multicolumn{3}{@{}l@{}} \ \\[-2.35ex]
	 \end{tabular}
	\advance \fitchprfwidth by \fitchsep%
}
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\fitcharg} Typesets an argument (without line
% numbers). Takes two arguments, the premises and conclusion lines of
% the argument.
%    \begin{macrocode}
\newcommand{\fitcharg}[2]{
	\advance \fitchargwidth by -\fitchsep%
	\hspace*{.35em}
	\begin{tabular}[t]{|p{\fitchsep}@{}p{\fitchargwidth}@{}}
		\multicolumn{2}{@{}l@{}}{\ }\\[-2.35ex]
		#1 \\ 
		\ \\[-2.5ex] \cline{1-1}\\[-2ex]
 		#2 \\ \multicolumn{2}{@{}l@{}} \ \\[-2.35ex]
	\end{tabular}
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\slider} Typesets the focus arrow.
%    \begin{macrocode}
\newcommand*{\slider}{\mbox{$\triangleright \;$}}
%    \end{macrocode}
% \end{macro}
% 
% \begin{macro}{\pline} Typesets a proof line with an optional line
% number (before the formula argument) and an optional justification
% (after the formula argument)
%    \begin{macrocode}
\def\pline{\@ifnextchar[\@plinenum{\@plinenum[\@empty]}} 
\def\@plinenum[#1]#2{\@ifnextchar[{\@plinex{#1}{#2}}{%
    \@plinex{#1}{#2}[\@empty]}} 
\def\@plinex#1#2[#3]{ & #1\formula{\; #2} & #3} 
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\fpline} Like |pline| except produces a focus slider
% on the left
%    \begin{macrocode}
\newcommand*\fpline{\slider\pline} 
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\tline} Typesets proof line containing text with an
% optional line number.
%    \begin{macrocode}
\newcommand*{\tline}[2][{}]{ & #1\hspace{.6em}{#2}}
%    \end{macrocode}
% \end{macro}
%
% The following macros |\nline|, |\jline|, and |\fline|
% are the commands provided in the original version
% of |lplfitch| and are included for backwards compatibility. 
%    \begin{macrocode}
\newcommand*{\nline}[2][{}]{ & #1\formula{\;#2}}
%    \end{macrocode}
% justified line (justification optional)
% |\jline[justification]{args for line}|
%    \begin{macrocode}
\newcommand*{\jline}[2][{}]{\nline#2 & #1}
%    \end{macrocode}
% focused line
%    \begin{macrocode}
\newcommand*{\fline}[1]{\slider \jline#1}
%    \end{macrocode}
%
% \begin{macro}{\ellipsesline}
% Producing vertical ellipses in a line on their own.
% This takes care of centering the ellipses in their line.
%    \begin{macrocode}
\newcommand*{\ellipsesline}[0]{\nline{\;\raise.65ex\hbox{\vdots}}}
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\subproof}
% This command sets a subproof within a proof.
% The arguments are the line before, and the lines after
% the horizontal fitch bar.
%    \begin{macrocode}
\newcommand{\subproof}[2]{&\fitchprf{#1}{#2}\\}
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\boxedsubproof}
% Produces a new boxed subproof.
% |\boxedsubproof|\oarg{n}\marg{c}\marg{premise}\marg{body}, where
% \meta{n} is the number of the premise line, \meta{c} is the
% constant(s) to be boxed, \meta{premise} is the premise of the
% subproof, and \meta{body} contains the lines of the subproof.
%    \begin{macrocode}
\newcommand{\boxedsubproof}[4][{}]{
     \subproof{\nline[#1]{\fbox{\formula{#2}}\;#3}}{#4}
}
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\brokenform}
% A crude attempt at dealing with a formula which need to be broken to
% fit in the proof.  We take two arguments, the first line of the
% formula which is left justified, and the remainder of the lines,
% which are right justified.  The first argument is set as a
% |\formula| but the second is not (as it may contain line breaks
% itself).
%    \begin{macrocode}
\newcommand{\brokenform}[2]{
   \advance\fitchprfwidth by-\fitchsep
   \begin{tabular}[c]{rp{\fitchprfwidth}}
    \multicolumn{1}{p{\fitchprfwidth}@{}}{\formula{#1}}\\
    \formula{#2}
   \end{tabular}
   \advance\fitchprfwidth by\fitchsep
}
%    \end{macrocode}
% \end{macro}
%
% \Finale
\endinput