summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/lplfitch
diff options
context:
space:
mode:
authorNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
committerNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
commite0c6872cf40896c7be36b11dcc744620f10adf1d (patch)
tree60335e10d2f4354b0674ec22d7b53f0f8abee672 /macros/latex/contrib/lplfitch
Initial commit
Diffstat (limited to 'macros/latex/contrib/lplfitch')
-rw-r--r--macros/latex/contrib/lplfitch/README42
-rw-r--r--macros/latex/contrib/lplfitch/lplfitch.dtx796
-rw-r--r--macros/latex/contrib/lplfitch/lplfitch.ins59
-rw-r--r--macros/latex/contrib/lplfitch/lplfitch.pdfbin0 -> 226982 bytes
4 files changed, 897 insertions, 0 deletions
diff --git a/macros/latex/contrib/lplfitch/README b/macros/latex/contrib/lplfitch/README
new file mode 100644
index 0000000000..c89659a03b
--- /dev/null
+++ b/macros/latex/contrib/lplfitch/README
@@ -0,0 +1,42 @@
+lplfitch
+========
+
+LaTeX package for typesetting Fitch-style proofs a la Language, Proof,
+and Logic, a logic textbook by Jon Barwise and John Etchemendy. It was
+originally written by John Etchemendy, with modifications by
+Dave Barker-Plummer and Richard Zach.
+
+https://github.com/rzach/lplfitch
+
+Installation
+------------
+
+Run latex on lplfitch.ins to produce lplfitch.sty
+
+Run latex on lplfitch.dxt to produce the documentation.
+
+License
+-------
+
+Copyright 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.
+
+This work has the LPPL maintenance status `maintained'.
+
+The Current Maintainer of this work is Richard Zach.
+
+This work consists of the files lplfitch.dtx and lplfitch.ins
+and the derived files lplfitch.sty and lplfitch.pdf.
+
+Versions
+--------
+
+0.9 (2013/05/16) First public beta
+
diff --git a/macros/latex/contrib/lplfitch/lplfitch.dtx b/macros/latex/contrib/lplfitch/lplfitch.dtx
new file mode 100644
index 0000000000..e0f8bb4741
--- /dev/null
+++ b/macros/latex/contrib/lplfitch/lplfitch.dtx
@@ -0,0 +1,796 @@
+% \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
diff --git a/macros/latex/contrib/lplfitch/lplfitch.ins b/macros/latex/contrib/lplfitch/lplfitch.ins
new file mode 100644
index 0000000000..5de9a57126
--- /dev/null
+++ b/macros/latex/contrib/lplfitch/lplfitch.ins
@@ -0,0 +1,59 @@
+%%
+%% Copyright (C) 2013 by Dave Barker-Plummer and Richard Zach
+%%
+%% This file may be distributed and/or modified under the conditions of
+%% the LaTeX Project Public License, either version 1.2 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.2 or later is part of all distributions of LaTeX version
+%% 1999/12/01 or later.
+%%
+
+\input docstrip.tex
+\keepsilent
+
+\usedir{tex/latex/lplfitch}
+
+\preamble
+
+This is a generated file.
+
+Copyright (C) 2013 by John Etchemendy, Dave Barker-Plummer and Richard Zach
+
+This file may be distributed and/or modified under the conditions of
+the LaTeX Project Public License, either version 1.2 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.2 or later is part of all distributions of LaTeX version
+1999/12/01 or later.
+
+\endpreamble
+
+\generate{\file{lplfitch.sty}{\from{lplfitch.dtx}{package}}}
+
+\obeyspaces
+\Msg{*************************************************************}
+\Msg{* *}
+\Msg{* To finish the installation you have to move the following *}
+\Msg{* file into a directory searched by TeX: *}
+\Msg{* *}
+\Msg{* lplfitch.sty *}
+\Msg{* *}
+\Msg{* To produce the documentation, do *}
+\Msg{* *}
+\Msg{* pdflatex lplfitch.dtx *}
+\Msg{* makeindex -s gglo.ist -o lplfitch.gls lplfitch.glo *}
+\Msg{* pdflatex lplfitch.dtx *}
+\Msg{* pdflatex lplfitch.dtx *}
+\Msg{* *}
+\Msg{* Happy TeXing! *}
+\Msg{* *}
+\Msg{*************************************************************}
+
+\endbatchfile
diff --git a/macros/latex/contrib/lplfitch/lplfitch.pdf b/macros/latex/contrib/lplfitch/lplfitch.pdf
new file mode 100644
index 0000000000..58a7f7ac17
--- /dev/null
+++ b/macros/latex/contrib/lplfitch/lplfitch.pdf
Binary files differ