summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/fitch/fitchdoc.tex
diff options
context:
space:
mode:
Diffstat (limited to 'macros/latex/contrib/fitch/fitchdoc.tex')
-rw-r--r--macros/latex/contrib/fitch/fitchdoc.tex515
1 files changed, 362 insertions, 153 deletions
diff --git a/macros/latex/contrib/fitch/fitchdoc.tex b/macros/latex/contrib/fitch/fitchdoc.tex
index 1889721dd0..5a16d90f15 100644
--- a/macros/latex/contrib/fitch/fitchdoc.tex
+++ b/macros/latex/contrib/fitch/fitchdoc.tex
@@ -18,16 +18,16 @@
% Original Author: Peter Selinger, Dalhousie University
% Created: Jan 14, 2002
-% Modified: Sep 4, 2023
-% Version: 0.6
-% Copyright: (C) 2002-2023 Peter Selinger
+% Modified: Dec 17, 2023
+% Version: 1.0
+% Copyright: (C) 2002-2023 Peter Selinger, Richard Zach
% Filename: fitch.sty
% Documentation: fitchdoc.tex
% https://github.com/OpenLogicProject/fitch/
\documentclass{ltxdoc}
-\usepackage{fitch,graphicx,showexpl,fullpage}
+\usepackage{fitch,graphicx,showexpl}
\lstset{%
basicstyle=\ttfamily\small,
@@ -39,15 +39,23 @@
captionpos=t
}
+\addtolength{\oddsidemargin}{-1cm}
+\addtolength{\textwidth}{2cm}
+
+\newcommand\NewIn[1]{\leavevmode
+ \marginpar{\hfill\fbox{\fbox{New in #1}}\hspace*{1em}}\ignorespaces}
+
\title{\texttt{fitch.sty}: Fitch-style natural deduction macros}
-\author{Peter Selinger\\Dalhousie University\thanks{The current
-maintainer of this package is \href{https://richardzach.org}{Richard
-Zach}. The package repository is at
-\url{https://github.com/OpenLogicProject/fitch/}, where you can also
-report any \href{https://github.com/OpenLogicProject/fitch/issues}{issues} with it.}}
+\author{Peter Selinger\\Dalhousie University \and Richard
+Zach\\University of Calgary\thanks{The current maintainer of this
+package is \href{https://richardzach.org}{Richard Zach}. The package
+repository is at \url{https://github.com/OpenLogicProject/fitch/},
+where you can also report any
+\href{https://github.com/OpenLogicProject/fitch/issues}{issues} with
+it.}}
-\date{Version 0.6\\ September 4, 2023}
+\date{Version 1.0\\ December 17, 2023}
\begin{document}
\maketitle
@@ -55,16 +63,15 @@ report any \href{https://github.com/OpenLogicProject/fitch/issues}{issues} with
\section{Overview}
This document describes how to use the {\tt fitch.sty} macros for
-typesetting Fitch-style natural deduction derivations. To load the macros,
-simply put \verb!\usepackage{fitch}! into the preamble of your
+typesetting Fitch-style natural deduction derivations. To load the
+macros, simply put |\usepackage{fitch}| into the preamble of your
{\LaTeX} file.
Here is a natural deduction derivation, together with the code that
produced it:
\begin{LTXexample}
-\[
-\begin{nd}
+$\begin{nd}
\hypo {1} {P\vee Q}
\hypo {2} {\neg Q}
\open
@@ -78,25 +85,50 @@ produced it:
\have {8} {P} \be{7}
\close
\have {9} {P} \oe{1,3-4,aa-8}
-\end{nd}
-\]
+\end{nd}$
\end{LTXexample}
A derivation consists of \emph{lines}, and each line contains a {\em
-line number} and a \emph{formula}. Some lines also carry a {\em
+line label} and a \emph{formula}. Some lines also carry a {\em
justification}. Moreover, each line is either a \emph{hypothesis} or a
-\emph{derived formula}. Generally, derived formulas carry a
+\emph{derived formula}. Usually, derived formulas carry a
justification, whereas hypotheses do not; however, the macros do not
enforce this.
-\DescribeEnv{nd}
-Derivations are typeset inside the \verb!nd! environment, which must be
-used in math mode.
+Proofs set using |fitch.sty| will have lines numbered automatically in
+the output. It is possible to override the automatic numbering (see
+Section~\ref{subsec-customline}). You can refer to line numbers in the
+text using |\ndref| (see Section~\ref{subsec-ndref}). Various
+dimensions, formatting of justifications and line references, and the
+shorthand macros used to produce rule names can be customized (see
+Section~\ref{sec-customization}).
+
+\NewIn{1.0} Several new commands and customization options have been
+introduced in v1.0. It is mostly backwards compatible with earlier
+versions, but see section~\ref{compat}. In particular, if you
+redefined any internal |fitch| commands, you will have to change |nd*|
+to |nd@|.
+
+\section{Usage}\label{sec-usage}
+
+\DescribeEnv{nd}\DescribeEnv{nd} Derivations are typeset
+inside the |nd| environment. By default, the standard |array|
+environment is used to do this, so the |nd| environment must must be
+used in math mode, i.e., it should be surrounded by |$...$| or
+|\[...\]|.
+
+\NewIn{1.0} The environment |fitchproof| typesets the proof on its own
+in text, not math mode. Proofs will be set flush left, with the
+default |\partopsep| spacing surrounding lists added. You do not have
+to insert |$| to switch to math mode for |fitchproof|---by default.
+However, it only works if you generate proofs using the |tabular|
+environment, e.g., by loading |fitch| with the |arrayenv=tabular|
+option.
\DescribeMacro{\hypo}\DescribeMacro{\have}
-The commands \verb!\hypo! and \verb!\have! are used
-to typeset one line of the derivation; \verb!\hypo! is used for
-hypotheses, and \verb!\have! for derived formulas. Both commands take
+The commands |\hypo| and |\have| are used
+to typeset one line of the derivation; |\hypo| is used for
+hypotheses, and |\have| for derived formulas. Both commands take
a label and a formula as an argument. Note that the labels used to
identify lines in the derivation need not be actual line numbers; for
instance, in the above example, we used the label $aa$ instead of $5$.
@@ -104,41 +136,37 @@ In the output, lines are automatically numbered consecutively. Labels
may not contain any punctuation characters or spaces.
\DescribeMacro{\open}\DescribeMacro{\close}
-Subderivations are opened and closed with the commands \verb!\open! and
-\verb!\close!. Finally, the following commands are provided for
+Subderivations are opened and closed with the commands |\open| and
+|\close|. Finally, the following commands are provided for
annotating lines with justifications:
-
-\medskip
-\hfill
-\begin{tabular}{@{}ll@{}}
- \verb!\r! & reiteration \\
- \verb!\ii! & implication introduction \\
- \verb!\ie! & implication elimination \\
- \verb!\ai! & and introduction \\
- \verb!\ae! & and elimination \\
-\end{tabular}
-\hfill
-\begin{tabular}{ll}
- \verb!\oi! & or introduction \\
- \verb!\oe! & or elimination \\
- \verb!\ni! & not introduction \\
- \verb!\ne! & not elimination \\
- \verb!\be! & bottom elimination \\
+\begin{center}
+\begin{tabular}[t]{@{}ll@{}}
+ |\r| & reiteration \\
+ |\ii| & implication introduction \\
+ |\ie| & implication elimination \\
+ |\ai| & and introduction \\
+ |\ae| & and elimination \\
+ |\oi| & or introduction \\
+ |\oe| & or elimination
\end{tabular}
-\hfill
-\begin{tabular}{@{}ll@{}}
- \verb!\nne! & double negation elimination \\
- \verb!\Ai! & forall introduction \\
- \verb!\Ae! & forall elimination \\
- \verb!\Ei! & exists introduction \\
- \verb!\Ee! & exists elimination \\
+\qquad
+\begin{tabular}[t]{ll}
+ |\ni| & not introduction \\
+ |\ne| & not elimination \\
+ |\be| & bottom elimination \\
+ |\nne| & double negation elimination \\
+ |\Ai| & forall introduction \\
+ |\Ae| & forall elimination \\
+ |\Ei| & exists introduction \\
+ |\Ee| & exists elimination \\
\end{tabular}
-\hfill
-\medskip
+\end{center}
+\NewIn{1.0} These commands and what they produce can be customized,
+see Section~\ref{sec-customization}.
Each such command takes a \emph{reference list} as an argument. A
reference list is a string made from labels, commas, and hyphens, for
-instance \verb!1,3a-3b,4a-4d!.
+instance |1,3a-3b,4a-4d|.
\section{Details}
@@ -148,7 +176,7 @@ Some natural deduction derivations with quantifiers use \emph{guards}, as in
the following example:
\begin{LTXexample}
-\[
+$
\begin{nd}
\hypo {1} {\exists x\forall y.P(x,y)}
\open[v]
@@ -161,87 +189,117 @@ the following example:
\close
\have {6} {\forall y\exists x.P(x,y)} \Ai{2-5}
\end{nd}
-\]
+$
\end{LTXexample}
The guards $v$ and $u$ in line 2 were typeset by giving optional
-arguments to the \verb!\open! commands of the respective
+arguments to the |\open| commands of the respective
subderivations.
\DescribeMacro{\guard}
For most purposes, the above way of specifying guards is sufficient.
However, there is another method, which allows a more flexible
placement of guards: before any line, you can give the command
-\verb!\guard{u}! to add a guard $u$ to the top-level subderivation at
-that line, or \verb!\guard[n]{u}! to add a guard to the $n$th
+|\guard{u}| to add a guard $u$ to the top-level subderivation at
+that line, or |\guard[n]{u}| to add a guard to the $n$th
enclosing subderivation at that line. Thus, the above example could
-have also been typeset by inserting the two commands \verb!\guard{u}! and
-\verb!\guard[2]{v}! just after the second \verb!\open! statement.
+have also been typeset by inserting the two commands |\guard{u}| and
+|\guard[2]{v}| just after the second |\open| statement.
% For backward compatibility, there is a third way of specifying guards
-% by giving an optional second argument to the \verb!\hypo! and
-% \verb!\have! commands. The use of this feature is discouraged.
-
-\subsection{Generic justifications}
-
-Non-standard justifications can be created with the \verb!\by!
-command. This command takes two arguments: a name and a reference
-list. For instance, the command \verb!\by{De Morgan}{lab3,lab4}! might
-produce the output ``\mbox{De Morgan, 3, 4}''. Note that the justification
-is typeset in text mode. A comma is automatically inserted between the
-name and the reference list, unless the reference list is empty.
-
-\subsection{Label and reference list details}
-
-Labels may not contain commas, periods, semicolons, hyphens,
-parenthesis, or spaces. In a reference list, spaces are ignored (even
-within a label!), whereas commas, periods, semicolons, parenthesis,
-and hyphens are copied to the output. All other characters are
-interpreted as part of a label. Attempting to reference a label which
-has not been previously defined by any \verb!\hypo! or \verb!\have!
-command produces an error message of the form:
-
+% by giving an optional second argument to the |\hypo| and
+% |\have| commands. The use of this feature is discouraged.
+
+\subsection{Label and reference list details}\label{subsec-ndref}
+
+Labels for lines given to the |\have| and |\hypo| commands need not be
+numeric, although the package will \emph{output} them as consecutive
+numbers (see Section~\ref{subsec-customline} for how to adjust the
+numbering). Labels, however, may not contain commas, periods,
+semicolons, hyphens, parentheses, or spaces. In a reference list,
+spaces are ignored (even within a label!), whereas commas, periods,
+semicolons, parentheses, and hyphens are copied to the output. All
+other characters are interpreted as part of a label. Attempting to
+reference a label which has not been previously defined by any |\hypo|
+or |\have| command produces a \NewIn{0.6} warning message of the form:
\begin{verbatim}
- ! Package fitch Error: Undefined line reference: lab17.
+ ! Package fitch Warning: Undefined line reference: lab17.
\end{verbatim}
-
-\subsection{Referencing line numbers in the text}
-\label{subsec-ndref}
+(In earlier versions, this resulted in an error, not a warning.)
\DescribeMacro{\ndref}
-Labels defined in an \verb!nd! environment can be referenced in the
-text with the \verb!\ndref! command. This command takes a reference
+Labels defined in an |nd| environment can be referenced in the
+text with the |\ndref| command. This command takes a reference
list as an argument, and produces the corresponding output. However,
it is only possible to reference labels \emph{after} the corresponding
derivation has been typeset. There is currently no convenient way of
defining forward references. Also, if a label is used more than once,
-\verb!\ndref! will always refer to the most recent time it was used.
+|\ndref| will always refer to the most recent time it was used.
+
+\subsection{Generic justifications}
+
+\DescribeMacro{\by}
+Non-standard justifications can be created with the |\by|
+command. This command takes two arguments: a name and a reference
+list. For instance, the command |\by{De Morgan}{lab3,lab4}| might
+produce the output ``\mbox{De Morgan, 3, 4}''. Note that the justification
+is typeset in text mode.
+
+In the default justification format, a comma is automatically inserted
+between the name and the reference list, unless the reference list is
+empty. The formatting of justifications can be changed, see
+Section~\ref{sec-customization}. If the second argument (the reference
+list) is empty, only the first argument (without formatting or
+punctuation) is printed. \NewIn{1.0} If the first argument is empty,
+only the reference list is printed.
+
+Since the |\by| command outputs its first argument without additional
+formatting when the second argument is empty, you can use |\by{...}{}|
+to produce arbitrary text in the justification. You can use the
+|\ndref| command here.
+\begin{LTXexample}
+$
+\begin{nd}
+ \hypo {a} {A \Rightarrow B}
+ \by{Premise}{}
+ \hypo {b} {A} \by{Premise}{}
+ \have {c} {B}
+ \by{\ndref{a,b}
+ (but \emph{how?})}{}
+ \have {d} {A \wedge B} \by{}{b,c}
+\end{nd}
+$
+\end{LTXexample}
\subsection{Scope}
-The commands \verb!\hypo!, \verb!\have!, \verb!\open!, \verb!\close!,
-\verb!\r!, \verb!\ii!, and so forth are only available inside an
-\verb!nd! environment. These commands may have a different meaning
-elsewhere in the same document. The only commands provided by the
-\verb!fitch.sty! package which are visible outside an \verb!nd!
-environment are the command \verb!\ndref! described in
-Section~\ref{subsec-ndref}, and the command \verb!\nddim! and the
-dimension \verb!\ndindent! described in Section~\ref{subsec-nddim}.
+The commands |\hypo|, |\have|, |\open|, |\close|, |\by|, |\r|, |\ii|, and so
+forth are only available inside an |nd| environment. These commands
+may have a different meaning elsewhere in the same document. The only
+commands provided by the |fitch.sty| package which are visible
+outside an |nd| environment are the command |\ndref| described in
+Section~\ref{subsec-ndref}, the commands |\ndrules|, |\ndjustformat|,
+|\ndrefformat|, and |\nddim|, and the dimension |\ndindent| described
+in Section~\ref{sec-customization}.
\subsection{Breaking it across pages}\label{subsec-break}
-\DescribeMacro{\ndresume}
-The \verb!nd! environment is derived from the {\LaTeX} \verb!array!
+\DescribeEnv{ndresume}
+\DescribeEnv{fitchproof*}
+The |nd| environment is derived from the {\LaTeX} |array|
environment, and thus it does not break across pages automatically.
However, if a derivation is too long to fit on a single page, it is
possible to split it manually into physically independent, but
-logically consecutive subparts. For this purpose, the \verb!ndresume!
+logically consecutive subparts. For this purpose, the |ndresume|
environment is provided to continue a previously interrupted
-derivation. Here is an example:
+derivation.
+\NewIn{1.0} The environment |fitchproof*| works the same way, except typesets the
+proof just like the |fitchproof| environment (no need for math mode,
+flush left, spacing before and after). However, like |fitchproof|, it
+requires the |arrayenv=tabular| option. Here is an example:
\begin{LTXexample}
-$
-\begin{nd}
+\begin{fitchproof}[arrayenv=tabular]
\hypo {1} {P\vee Q}
\hypo {2} {\neg Q}
\open
@@ -251,40 +309,47 @@ $
\open
\hypo {aa} {Q}
\have {6} {\neg Q} \r{2}
-\end{nd}
-$
-
+\end{fitchproof}
Derivations can be interrupted and
resumed at any point.
-
-$
-\begin{ndresume}
+\begin{fitchproof*}[arrayenv=tabular]
\have {7} {\bot} \ne{aa,6}
\have {8} {P} \be{7}
\close
\have {9} {P} \oe{1,3-4,aa-8}
-\end{ndresume}
-$
+\end{fitchproof*}
\end{LTXexample}
-\subsection{Custom line numbers}
+\NewIn{1.0} You can also have derivations break across pages
+automatically. In order to do this, you have to load the
+\href{https://ctan.org/pkg/longtable}{|longtable|} package, and load
+|fitch| with the |arrayenv=longtable| option. Since the |longtable|
+environment works in text (not math) mode, you should then only use
+|fitchproof|, or the |nd| environment but \emph{not} in text mode.
+Note that the |longtable| package does not work in 2-column mode or
+inside a |multicolumn| environment. You can always produce a proof
+inside a |multicolumn| environment by passing |arrayenv=tabular| as an
+option to the |nd| or |fitchproof| environment.
+
+
+\subsection{Custom line numbers}\label{subsec-customline}
One often needs to write derivation schemas, rather than derivations.
This often requires the use of symbolic constants such as $n$, $n+1$,
-etc, instead of actual line numbers. The \verb!\have! and \verb!\hypo!
+etc, instead of actual line numbers. The |\have| and |\hypo|
commands have an optional first argument which is a symbolic constant.
-For instance, \verb!\have[n]! will cause the current line to be
+For instance, |\have[n]| will cause the current line to be
numbered with the symbolic constant $n$. Subsequent lines are
automatically numbered $n+1$ etc. An initial offset can be given as a
-second optional argument, as in \verb!\have[n][-1]!, which will cause
+second optional argument, as in |\have[n][-1]|, which will cause
the current line to be numbered $n-1$, the following line $n$, etc. In
an explicit offset is given, the symbolic constant can also be absent:
-for instance, the command \verb!\have[][7]! resets the current line
+for instance, the command |\have[][7]| resets the current line
number to $7$. The following example illustrates this behavior:
\begin{LTXexample}
-\[
-\begin{nd}
+$
+\begin{nd}[justsep=1em]
\hypo {1} {P\vee Q}
\open
\hypo {2} {P}
@@ -296,11 +361,12 @@ number to $7$. The following example illustrates this behavior:
\have [\vdots] {6} {\vdots}
\have [m] {7} {A\wedge B}
\close
- \have {8} {A\wedge B} \oe{1,2-(4),5-7}
+ \have {8} {A\wedge B}
+ \oe{1,2-(4),5-7}
\have [\vdots] {9} {\vdots}
- \have [][100] {10} {A} \ae{8}
+ \have [][100] {10} {A} \ae{8}
\end{nd}
-\]
+$
\end{LTXexample}
Note that in the justification for line $m+1$, parentheses had to be
@@ -309,83 +375,226 @@ automatically.
{\bf Exercise.} How does one typeset an empty line number?
-{\bf Solution.} Since \verb!\have[]! has a special meaning as explained
-above, we need to use \verb!\have[~]! instead.
+{\bf Solution.} Since |\have[]| has a special meaning as explained
+above, we need to use |\have[~]| instead.
\subsection{Continuation lines}\label{subsec-continuation}
Sometimes one has to typeset a very long formula that does not fit on
a single line. As of version 0.5 of the {\tt fitch.sty} macros, it is
-possible to break a formula into several lines using \verb!\\! as a
+possible to break a formula into several lines using |\\| as a
line separator. Continuation lines are automatically indented, as
shown in the following example.
\begin{LTXexample}
-\[
+$
\begin{nd}
\hypo{1} {A\wedge B}
- \hypo{2} {A\wedge B\rightarrow{} \\
+ \hypo{2} {A\wedge B\Rightarrow{} \\
C\wedge D}
\have{3} {C\wedge D} \ie{1,2}
\have{4} {A\wedge B\wedge{} \\
C\wedge D} \ai{1,3}
\end{nd}
-\]
+$
\end{LTXexample}
\DescribeMacro{\hypocont}
\DescribeMacro{\havecont}
-Alternatively, the \verb!\havecont! and \verb!\hypocont! commands can
+Alternatively, the |\havecont| and |\hypocont| commands can
be used to specify each continuation line separately, as the following
example illustrates.
\begin{LTXexample}
-\[
+$
\begin{nd}
\hypo{1} {A\wedge B}
- \hypo{2} {A\wedge B\rightarrow{}}
+ \hypo{2} {A\wedge B\Rightarrow{}}
\hypocont {C\wedge D}
\have{3} {C\wedge D} \ie{1,2}
\have{4} {A\wedge B\wedge{}} \ai{1,3}
\havecont {C\wedge D}
\end{nd}
-\]
+$
\end{LTXexample}
This latter style gives slightly more flexibility in the placement of
justifications, since each line and continuation line can have its own
-justification and its own guard (via the \verb!\guard! command). It
+justification and its own guard (via the |\guard| command). It
also allows a derivation to be interrupted between a line and its
continuation, as discussed in Section~\ref{subsec-break}.
-\subsection{Customizing dimensions}\label{subsec-nddim}
+\section{Customization}\label{sec-customization}
-\DescribeMacro{\nddim}
The relative sizes of the various elements of a natural deduction
proof are preset to reasonable values depending on the size of the
currently selected font. However, it will sometimes be necessary to
-customize these dimensions. This can be achieved with the
-\verb!\nddim! command. The syntax of the command is as follows:
+customize these dimensions. The customizable dimensions are given in
+the following diagram.
\begin{center}
- \cmd{\nddim}\marg{height}\marg{topheight}\marg{depth}\marg{labelsep}
- \marg{indent}\marg{hsep}\marg{justsep}\marg{linethickness},
+ \includegraphics{fitchdoc-dimen}
\end{center}
-where each of the eight parameters is a dimension. The meaning of the
-first seven parameters is shown in the
-following illustrations; \emph{linethickness} is simply the thickness
-of the lines.
-\[\includegraphics{fitchdoc-dimen}\]
-The default dimensions are:
+In addition, \meta{linethickness} determines the thickness of scope
+lines, and \meta{cindent} the extra indentation of continuation lines
+(as discussed in Section~\ref{subsec-continuation}). The default
+dimensions are:
+\begin{center}
+\begin{tabular}{ll@{\qquad}ll}
+ \meta{height} & 4.5ex &
+ \meta{topheight} & 3.5ex\\
+ \meta{depth} & 1.5ex &
+ \meta{labelsep} & 1em\\
+ \meta{indent} & 1.6em &
+ \meta{hsep} & .5em\\
+ \meta{justsep} & 2.5em &
+ \meta{linethickness} & .2mm\\
+ \meta{cindent} & 1em
+\end{tabular}
+\end{center}
+
+\NewIn{1.0} To change these default dimensions, pass a list of
+key-value pairs as package options, as optional arguments to the
+|nd| or |fitchproof| environment, or use the |\setkeys|
+command:
+\begin{verbatim}
+ \usepackage[justsep=1em]{fitch}
+ \begin{nd}[rules=myrules]
+ \begin{fitchproof}[linethickness=1pt]
+ \setkeys{fitch}{hsep=1em,indent=1em}\end{verbatim}
+
+In addition, the macros used to generate the table containing the
+proof, to format justifications, format line number references, and to
+initialize macros to produce justifications in the proof can be
+customized:
+\begin{center}
+ \begin{tabular}{ll}
+ option & default\\\hline
+ |rules=|\meta{macroname} & |ndrules|\\
+ |justformat=|\meta{macroname} & |ndjustformat|\\
+ |refformat=|\meta{macroname} & |ndrefformat|\\
+ |arrayenv=|\meta{envname} & |array|
+ \end{tabular}
+\end{center}
+For compatibility with earlier versions of |fitch.sty|, the default
+for \meta{arrayenv} is |array|, i.e., the table containing the proof
+is generated using an |array| environment, and must therefore occur
+inside math mode. The |fitchproof| and |fitchproof*| environments
+assume that you use a text table command instead, such as |tabular|.
+Hence, you should \emph{not} use |fitchproof| in math mode, and you
+must use the option |arrayenv=tabular| (when loading |fitch|, as an
+optional argument to |fitchproof|, or using
+|\setkeys{fitch}{arrayenv=tabular}|. Any other table environment that
+takes the same table format argument as |array| and |tabular| can be
+used here, e.g., the |longtable| environment from the |longtable|
+package (which must be loaded separately).
+
+The package defines the macros
+\DescribeMacro{\ndrules}\cmd{\ndrules}, which defines the rule
+macros given at the end of Section~\ref{sec-usage}, using
+\begin{verbatim}
+ \def\ndrules{%
+ \def\ii{\by{$\Rightarrow$I}}%
+ \def\ie{\by{$\Rightarrow$E}}%
+ \def\Ai{\by{$\forall$I}}%
+ \def\Ae{\by{$\forall$E}}%
+ \def\Ei{\by{$\exists$I}}%
+ \def\Ee{\by{$\exists$E}}%
+ \def\ai{\by{$\wedge$I}}%
+ \def\ae{\by{$\wedge$E}}%
+ \def\ai{\by{$\wedge$I}}%
+ \def\ae{\by{$\wedge$E}}%
+ \def\oi{\by{$\vee$I}}%
+ \def\oe{\by{$\vee$E}}%
+ \def\ni{\by{$\neg$I}}%
+ \def\ne{\by{$\neg$E}}%
+ \def\be{\by{$\bot$E}}%
+ \def\nne{\by{$\neg\neg$E}}%
+ \def\r{\by{R}}}
+\end{verbatim}
+\DescribeMacro{\ndjustformat}
+The macro \cmd{\ndjustformat} is defined as
+\begin{verbatim}
+ \newcommand{\ndjustformat}[2]{#1, #2}
+\end{verbatim}
+The first argument takes the rule name, the second the reference list.
+It is used to typeset the justification.
+
+\DescribeMacro{\ndrefformat}
+The macro \cmd{\ndrefformat} is defined as
+\begin{verbatim}
+ \newcommand{\ndrefformat}[1]{#1}
+\end{verbatim}
+It is used to typeset the line numbers in justifications.
+
+\cmd{\ndrules}, \cmd{\ndjustformat}, and \cmd{\ndrefformat} can
+be redefined using \cmd{\renewcommand}, or you can define your own
+commands to provide the rule names, the justification format, and line
+number format, and pass the names (without initial |\|) as an option
+to the \cmd{\usepackage} or individual \cmd{\nd} or \cmd{\fitchproof}
+commands.
+\begin{LTXexample}
+\newcommand{\myjust}[2]
+ {#2 by \textsf{#1}}
+\newcommand{\myrules}{
+ \ndrules % include standard rules
+ \def\ds{\by{DS}}}
+\renewcommand{\ndrefformat}[1]{(#1)}
+$
+\begin{nd}[rules=myrules,
+ justformat=myjust,
+ indent=1.5cm,
+ linethickness=1.5pt,
+ justsep=1cm]
+ \hypo {1} {A\vee B}
+ \hypo {2} {\neg B}
+ \open
+ \hypo {a} {B}
+ \have {3} {A} \ds{1,2}
+ \have {b} {A \wedge B} \ai{a,3}
+\end{nd}
+$
+\end{LTXexample}
+
+The boolean option |outerline| can be set to false to suppress the
+leftmost scope line. This may be useful when printing inference rules,
+e.g.,
+\begin{LTXexample}
+$
+\begin{nd}[outerline=false,
+ labelsep=0pt]
+ \open
+ \hypo [n]{1} {A}
+ \have [~]{2} {\raisebox{-1ex}{\vdots}}
+ \have [m]{3} {B}
+ \close
+ \have [~]{b} {A \Rightarrow B} \ii{1-3}
+\end{nd}
+$
+\end{LTXexample}
+
+\section{Obsolete commands and backwards compatibility}\label{compat}
+
+\DescribeMacro{\nddim}
+The dimensions can also be changed with the
+|\nddim| command. The syntax of the command is as follows:
\begin{center}
-\verb!\nddim{4.5ex}{3.5ex}{1.5ex}{1em}{1.6em}{.5em}{2.5em}{.2mm}!.
+ \cmd{\nddim}\marg{height}\marg{topheight}\marg{depth}\marg{labelsep}
+ \marg{indent}\marg{hsep}\marg{justsep}\marg{linethickness},
\end{center}
-\DescribeMacro{\ndindent}
-In addition, the dimension \verb!\ndindent!, controls
-the amount of extra indentation used on continuation lines as
-discussed in Section~\ref{subsec-continuation}. It can be changed and
-is \verb!1ex! by default.
+where each of the eight parameters is a dimension. This still works,
+but using the key-value pair options is the preferred method.
+
+\NewIn{1.0}\DescribeMacro{\ndindent} In versions before v1.0, the recommended way
+to change the extra indentation used on continuation lines was to
+change dimension |\ndindent| directly using |\setlength|. As of v1.0,
+you should use the |cindent| option instead.
+
+The original code ``hid'' the internal macros by naming
+them |\nd*...|. In v1.0 this has been changed to the standard
+|\nd@...|. Any low-level redefinition of |fitch| internals that uses
+|*| will break in v1.0.
-\subsection{Other comments}
+\section{Other comments}
The goal was to design a flexible package which would not impose any
constraints on the form of derivations, while making typesetting easy.
@@ -399,8 +608,8 @@ printed page.
\section{Copyright and license}
-This document and the accompanying \verb!fitch.sty! macros
-are {\copyright} 2002--2023 by Peter Selinger and distributed under
+This document and the accompanying |fitch.sty| macros are {\copyright}
+2002--2023 by Peter Selinger and Richard Zach and distributed under
the terms of the \href{https://www.latex-project.org/lppl/}{LPPL}.
\end{document}