texlive[69160] Master/texmf-dist: fitch (18dec23)
commits+karl at tug.org
commits+karl at tug.org
Mon Dec 18 21:56:00 CET 2023
Revision: 69160
https://tug.org/svn/texlive?view=revision&revision=69160
Author: karl
Date: 2023-12-18 21:56:00 +0100 (Mon, 18 Dec 2023)
Log Message:
-----------
fitch (18dec23)
Modified Paths:
--------------
trunk/Master/texmf-dist/doc/latex/fitch/README.md
trunk/Master/texmf-dist/doc/latex/fitch/fitch.hacker.txt
trunk/Master/texmf-dist/doc/latex/fitch/fitchdoc.pdf
trunk/Master/texmf-dist/doc/latex/fitch/fitchdoc.tex
trunk/Master/texmf-dist/tex/latex/fitch/fitch.sty
Modified: trunk/Master/texmf-dist/doc/latex/fitch/README.md
===================================================================
--- trunk/Master/texmf-dist/doc/latex/fitch/README.md 2023-12-18 20:55:50 UTC (rev 69159)
+++ trunk/Master/texmf-dist/doc/latex/fitch/README.md 2023-12-18 20:56:00 UTC (rev 69160)
@@ -7,8 +7,10 @@
Fitch-style natural deduction is a system for writing proofs in
propositional logic and predicate logic. This is a set of easy-to-use
LaTeX macros originally written by Peter Selinger. It is used, e.g.,
-in the various versions of _forall x_ by PD Magnus (e.g., the [original](https://www.fecundity.com/logic/download.html),
-[Cambridge](http://www.homepages.ucl.ac.uk/~uctytbu/OERs.html), and [Calgary](https://forallx.openlogicproject.org) versions)
+in the various versions of _forall x_ by PD Magnus (e.g., the
+[original](https://www.fecundity.com/logic/download.html),
+[Cambridge](http://www.homepages.ucl.ac.uk/~uctytbu/OERs.html), and
+[Calgary](https://forallx.openlogicproject.org) versions)
With these macros, one can typeset natural deduction proofs in Fitch
style, as in the following example:
@@ -36,6 +38,14 @@
## Changes
+**v1.0-beta, October 15, 2023** Adds `outerline` option; improves
+`\by`; fixes spacing when using `tabular`
+
+**v1.0-alpha, Sept 30, 2023** This is an alpha release that adds key-value
+options to the package and commands for customization. It is not fully
+compatible with the 0.x versions (see documentation). Please report
+any issues or suggestions.
+
**v0.6, Sept 4, 2023.** Updated the documentation and license (from
GPL to LPPL). The code is essentially unchanged.
@@ -51,13 +61,19 @@
## Related packages
-- The [`lplfitch`](https://ctan.org/pkg/lplfitch) packages produces
- Fitch-style roofs in the format used in Barwise & Etchemendy's textbook
- _Language, Proof, and Logic_.
-- The [`natded`](https://ctan.org/pkg/natded) package produces natural
- deduction roofs in the style of Jaśkowski, or that of Kalish and
- Montague.
+- [`logicproof`](https://ctan.org/pkg/logicproof): natural deduction
+ with boxed subproofs in the style of Huth and Ryan's _Logic in
+ Computer Science_.
+- [`lplfitch`](https://ctan.org/pkg/lplfitch): Fitch-style proofs in
+ the format used in Barwise & Etchemendy's textbook _Language, Proof,
+ and Logic_.
+- [`natded`](https://ctan.org/pkg/natded): natural deduction proofs
+ in the style of Jaśkowski, or that of Kalish and Montague.
+- [`synproof`](https://ctan.org/pkg/synproof): natural deduction
+ proofs in the style of Gamut's _Logic,
+ Language, and Meaning_.
+
Additional packages for proofs, including Johan Klüwer's, are
available at a [page maintained by Alex Kocurek](https://www.actual.world/latex/)
Modified: trunk/Master/texmf-dist/doc/latex/fitch/fitch.hacker.txt
===================================================================
--- trunk/Master/texmf-dist/doc/latex/fitch/fitch.hacker.txt 2023-12-18 20:55:50 UTC (rev 69159)
+++ trunk/Master/texmf-dist/doc/latex/fitch/fitch.hacker.txt 2023-12-18 20:56:00 UTC (rev 69160)
@@ -5,7 +5,7 @@
GENERAL
-Global identifiers defined by this package start with '\nd*'. The only
+Global identifiers defined by this package start with '\nd@'. The only
exceptions are \ndref, \nddim, \ndindent, and the "nd" and "ndresume"
latex environments.
@@ -22,16 +22,16 @@
We start with some macros to facilitate automatic line numbering, and
for referencing of lines by labels. The macros defined here are:
-\nd*reset to reset the line number count. \nd*num{x}, to generate the
-next line number and store it in reference x; \nd*ref{x} to print the
+\nd at reset to reset the line number count. \nd at num{x}, to generate the
+next line number and store it in reference x; \nd at ref{x} to print the
line number referenced by x, \ndref{xxx} to parse a list of
references, separated by commas, periods, and hyphens, and translate
all references to line numbers. Note: \ndref ignores spaces in its
argument, but puts a space after each comma or period in the
-output. Also note: \nd*ref can be useful outside a natded environment,
+output. Also note: \nd at ref can be useful outside a natded environment,
and thus it has a user accessible name. Most general ``line numbers''
actually consist of a name (such as ``n'') and a number (such as
-``2''), to produce output such as $n+2$. \nd*set{n}{m} is called to
+``2''), to produce output such as $n+2$. \nd at set{n}{m} is called to
set the letter to n and the number to m. As special cases, if the
second argument is empty, it is not set, and if the first argument is
\relax, it is not set.
@@ -38,20 +38,20 @@
Example for references:
-\nd*reset \nd*num{x}; \nd*num{y}; \nd*numopt{n+1}{z}; \nd*num{zz};
-\nd*ref{y}; \ndref{x, y-zz, z}
+\nd at reset \nd at num{x}; \nd at num{y}; \nd at numopt{n+1}{z}; \nd at num{zz};
+\nd at ref{y}; \ndref{x, y-zz, z}
will produce: 1; 2; n+1; 3; 2; 1, 2-3, n+1
LAYER A
Layer A provides primitive picture elements which can be combined into
-natural deduction derivations. These are: \nd*t to make a topmost
-vertical line segment; \nd*v to make a continuation vertical line
-segment, \nd*i to produce the indentation for a subproof, \nd*s to
+natural deduction derivations. These are: \nd at t to make a topmost
+vertical line segment; \nd at v to make a continuation vertical line
+segment, \nd at i to produce the indentation for a subproof, \nd at s to
produce the horizontal space between a vertical line and a formula,
-\nd*u{x} to underline x with appropriate spacing for a
-hypothesis. \nd*f{x} typesets the formula x with the appropriate
-vertical spacing. \nd*g{x} is like \nd*i, except it puts a guard in
+\nd at u{x} to underline x with appropriate spacing for a
+hypothesis. \nd at f{x} typesets the formula x with the appropriate
+vertical spacing. \nd at g{x} is like \nd at i, except it puts a guard in
the space it creates. These elements are spaced so that they are
appropriate as left-aligned array entries. Line numberings and
justifications must be provided manually in this layer. All explicit
@@ -62,15 +62,15 @@
\[
\begin{array}{lll}
- 1 & \nd*t\nd*s\nd*f {P\vee Q} \\
- 2 & \nd*v\nd*s\nd*u {\neg Q} \\
- 3 & \nd*v\nd*i\nd*t\nd*s\nd*u {P} \\
- 4 & \nd*v\nd*i\nd*v\nd*s\nd*f {P} & \mbox{by 3} \\
- 5 & \nd*v\nd*i\nd*t\nd*s\nd*u {Q} \\
- 6 & \nd*v\nd*i\nd*v\nd*s\nd*f {\neg Q} & \mbox{by 2} \\
- 7 & \nd*v\nd*i\nd*v\nd*s\nd*f {\bot} & \mbox{by 5, 6} \\
- 8 & \nd*v\nd*i\nd*v\nd*s\nd*f {P} & \mbox{by 7} \\
- 9 & \nd*v\nd*s\nd*f {P} & \mbox{by 1, 3-4, 5-8} \\
+ 1 & \nd at t\nd at s\nd at f {P\vee Q} \\
+ 2 & \nd at v\nd at s\nd at u {\neg Q} \\
+ 3 & \nd at v\nd at i\nd at t\nd at s\nd at u {P} \\
+ 4 & \nd at v\nd at i\nd at v\nd at s\nd at f {P} & \mbox{by 3} \\
+ 5 & \nd at v\nd at i\nd at t\nd at s\nd at u {Q} \\
+ 6 & \nd at v\nd at i\nd at v\nd at s\nd at f {\neg Q} & \mbox{by 2} \\
+ 7 & \nd at v\nd at i\nd at v\nd at s\nd at f {\bot} & \mbox{by 5, 6} \\
+ 8 & \nd at v\nd at i\nd at v\nd at s\nd at f {P} & \mbox{by 7} \\
+ 9 & \nd at v\nd at s\nd at f {P} & \mbox{by 1, 3-4, 5-8} \\
\end{array}
\]
@@ -77,53 +77,53 @@
LISTS
This is a bit of a hack. We implement linked lists as follows: a list
-is either \nd*nil, or \nd*cons{T}{H}, where T is another list, and H
+is either \nd at nil, or \nd at cons{T}{H}, where T is another list, and H
is some arbitrary code. Note that lists grow to the right. The
following macros operate on a list that is stored in a macro \list.
-\nd*push\list{item} pushes the item onto the list
-\nd*pop\list{item} pops and discards the last item from the list
-\nd*item\list{command} applies command to each element of the list
-\nd*modify\list\n{elt} modifies the \n-th element of the
+\nd at push\list{item} pushes the item onto the list
+\nd at pop\list{item} pops and discards the last item from the list
+\nd at item\list{command} applies command to each element of the list
+\nd at modify\list\n{elt} modifies the \n-th element of the
list, if there is such an element. Here \n is a counter. Elements
are counted from the right, starting from 1.
-We use lists of items of the forms \nd*t, \nd*v, \nd*i, and \nd*g{...}
+We use lists of items of the forms \nd at t, \nd at v, \nd at i, and \nd at g{...}
to represent the current indentation level and format (see Layer A,
-above). The function \nd*cont computes the indentation for the
-following line by replacing all items of the form \nd*t by \nd*v and
-\nd*g{...} by \nd*i.
+above). The function \nd at cont computes the indentation for the
+following line by replacing all items of the form \nd at t by \nd at v and
+\nd at g{...} by \nd at i.
With the list syntax, a derivation can be expressed like this:
\[
\begin{array}{lll}
- \gdef\stack{\nd*nil}
+ \gdef\stack{\nd at nil}
\newcount\n
- \nd*push\stack{\nd*t}
- 1 & \nd*iter\stack\relax\nd*s\nd*u {\neg\exists xP(x)} \\
- \nd*cont\stack
- \nd*push\stack{\nd*i}
- \nd*push\stack{\nd*t}
- \nd*n=2\nd*modify\stack\n{\nd*g{u}}
- \nd*push\stack{\nd*i}
- \nd*push\stack{\nd*t}
- 2 & \nd*iter\stack\relax\nd*s\nd*u {P(u)} \\
- \nd*cont\stack
- 3 & \nd*iter\stack\relax\nd*s\nd*f {\exists xP(x)} \\
- \nd*cont\stack
- 4 & \nd*iter\stack\relax\nd*s\nd*f {\neg\exists xP(x)} \\
- \nd*cont\stack
- 5 & \nd*iter\stack\relax\nd*s\nd*f {\bot} \\
- \nd*cont\stack
- \nd*pop\stack
- \nd*pop\stack
- 6 & \nd*iter\stack\relax\nd*s\nd*f {\neg P(u)} \\
- \nd*cont\stack
- \nd*pop\stack
- \nd*pop\stack
- 7 & \nd*iter\stack\relax\nd*s\nd*f {\forall y\neg P(y)} \\
- \nd*cont\stack
+ \nd at push\stack{\nd at t}
+ 1 & \nd at iter\stack\relax\nd at s\nd at u {\neg\exists xP(x)} \\
+ \nd at cont\stack
+ \nd at push\stack{\nd at i}
+ \nd at push\stack{\nd at t}
+ \nd at n=2\nd at modify\stack\n{\nd at g{u}}
+ \nd at push\stack{\nd at i}
+ \nd at push\stack{\nd at t}
+ 2 & \nd at iter\stack\relax\nd at s\nd at u {P(u)} \\
+ \nd at cont\stack
+ 3 & \nd at iter\stack\relax\nd at s\nd at f {\exists xP(x)} \\
+ \nd at cont\stack
+ 4 & \nd at iter\stack\relax\nd at s\nd at f {\neg\exists xP(x)} \\
+ \nd at cont\stack
+ 5 & \nd at iter\stack\relax\nd at s\nd at f {\bot} \\
+ \nd at cont\stack
+ \nd at pop\stack
+ \nd at pop\stack
+ 6 & \nd at iter\stack\relax\nd at s\nd at f {\neg P(u)} \\
+ \nd at cont\stack
+ \nd at pop\stack
+ \nd at pop\stack
+ 7 & \nd at iter\stack\relax\nd at s\nd at f {\forall y\neg P(y)} \\
+ \nd at cont\stack
\end{array}
\]
@@ -130,23 +130,23 @@
LAYER B
Layer B is simply a wrapper around layer A. It provides commands
-\nd*beginb, \nd*resumeb, \nd*endb, \nd*openb, \nd*closeb, \nd*guardb,
-\nd*hypob, and \nd*haveb which abstract from the layer A
+\nd at beginb, \nd at resumeb, \nd at endb, \nd at openb, \nd at closeb, \nd at guardb,
+\nd at hypob, and \nd at haveb which abstract from the layer A
primitives. This includes automatic line numbering, and automatic
-indentation. \nd*hypocontb and \nd*havecontb are like \nd*hypob and
-\nd*haveb, except that they introduce continuation lines that are
-slightly indented and have no line number/label. \nd*beginb and
-\nd*endb enclose a natural deduction in layer B syntax. \nd*resumeb is
-like \nd*beginb, except that it resumes a deduction in progress (for
-instance, after a manual page break). \nd*openb and \nd*closeb open,
-respectively close, a subproof. \nd*guardb{n}{g} adds the guard g to
+indentation. \nd at hypocontb and \nd at havecontb are like \nd at hypob and
+\nd at haveb, except that they introduce continuation lines that are
+slightly indented and have no line number/label. \nd at beginb and
+\nd at endb enclose a natural deduction in layer B syntax. \nd at resumeb is
+like \nd at beginb, except that it resumes a deduction in progress (for
+instance, after a manual page break). \nd at openb and \nd at closeb open,
+respectively close, a subproof. \nd at guardb{n}{g} adds the guard g to
the nth enclosing subderivation (counted from 1 from the
-inside). \nd*hypob introduces a hypothesis, and \nd*haveb introduces a
+inside). \nd at hypob introduces a hypothesis, and \nd at haveb introduces a
non-hypothesis line in a proof. Line numbering is integrated, but
justifications must still be given manually. Also, proof lines must
still be terminated by '\\'. An idiosyncracy of this layer is that in
a list of several hypotheses, all but the last one must be called with
-\nd*haveb, not \nd*hypob, to avoid drawing a horizontal line under
+\nd at haveb, not \nd at hypob, to avoid drawing a horizontal line under
each of them.
Example of a derivation using layer B syntax. Note that the "line
@@ -154,40 +154,40 @@
numbers in the output.
\[
- \nd*beginb
- \nd*haveb {1}{P\vee Q} \\
- \nd*hypob {2}{\neg Q} \\
- \nd*openb
- \nd*hypob {3}{P} \\
- \nd*haveb {4}{P} \mbox{by \ndref{3}} \\
- \nd*closeb
- \nd*openb
- \nd*hypob {5}{Q} \\
- \nd*haveb {6}{\neg Q} \mbox{by \ndref{2}} \\
- \nd*haveb {6a}{\bot} \mbox{by \ndref{5,6}} \\
- \nd*haveb {6b}{P} \mbox{by \ndref{6a}} \\
- \nd*closeb
- \nd*haveb {8}{P} \mbox{by \ndref{1,3-4,5-6b}} \\
- \nd*endb
+ \nd at beginb
+ \nd at haveb {1}{P\vee Q} \\
+ \nd at hypob {2}{\neg Q} \\
+ \nd at openb
+ \nd at hypob {3}{P} \\
+ \nd at haveb {4}{P} \mbox{by \ndref{3}} \\
+ \nd at closeb
+ \nd at openb
+ \nd at hypob {5}{Q} \\
+ \nd at haveb {6}{\neg Q} \mbox{by \ndref{2}} \\
+ \nd at haveb {6a}{\bot} \mbox{by \ndref{5,6}} \\
+ \nd at haveb {6b}{P} \mbox{by \ndref{6a}} \\
+ \nd at closeb
+ \nd at haveb {8}{P} \mbox{by \ndref{1,3-4,5-6b}} \\
+ \nd at endb
\]
Here is another example, using a guard.
\[
- \nd*beginb
- \nd*hypob {1}{\neg\exists xP(x)} \\
- \nd*openb
- \nd*guardb {1}{u}
- \nd*openb
- \nd*hypob {2}{P(u)} \\
- \nd*haveb {3}{\exists xP(x)} \mbox{by \ndref{2}} \\
- \nd*haveb {4}{\neg\exists xP(x)} \mbox{by \ndref{1}} \\
- \nd*haveb {5}{\bot} \mbox{by \ndref{3,4}}\\
- \nd*closeb
- \nd*haveb {6}{\neg P(u)} \mbox{by \ndref{2-5}}\\
- \nd*closeb
- \nd*haveb {7}{\forall y\neg P(y)} \mbox{by \ndref{2-6}}\\
- \nd*endb
+ \nd at beginb
+ \nd at hypob {1}{\neg\exists xP(x)} \\
+ \nd at openb
+ \nd at guardb {1}{u}
+ \nd at openb
+ \nd at hypob {2}{P(u)} \\
+ \nd at haveb {3}{\exists xP(x)} \mbox{by \ndref{2}} \\
+ \nd at haveb {4}{\neg\exists xP(x)} \mbox{by \ndref{1}} \\
+ \nd at haveb {5}{\bot} \mbox{by \ndref{3,4}}\\
+ \nd at closeb
+ \nd at haveb {6}{\neg P(u)} \mbox{by \ndref{2-5}}\\
+ \nd at closeb
+ \nd at haveb {7}{\forall y\neg P(y)} \mbox{by \ndref{2-6}}\\
+ \nd at endb
\]
LAYER C
@@ -197,42 +197,42 @@
layer C, it is no more necessary to explicitly give '\\', and all
hypotheses are denoted \hypo. Layer C also provides a convenient
syntax for writing justification labels. Further, layer C provides
-``multi-line'' commands, thus e.g. \nd*mhypoc{a}{x\\y\\z} is an
-abbreviation for \nd*hypoc{a}{x}\nd*hypocontc{y}\nd*hypocontc{z}. In
-addition there is a \nd*by command for writing justification labels,
-in the style of \nd*by{$\vee$E}{1,2-4,5-6}.
+``multi-line'' commands, thus e.g. \nd at mhypoc{a}{x\\y\\z} is an
+abbreviation for \nd at hypoc{a}{x}\nd at hypocontc{y}\nd at hypocontc{z}. In
+addition there is a \nd at by command for writing justification labels,
+in the style of \nd at by{$\vee$E}{1,2-4,5-6}.
-Commands exported by layer C are: \nd*hypoc, \nd*havec, \nd*hypocontc,
-\nd*havecontc, \nd*mhypoc, \nd*mhavec, \nd*mhypocontc, \nd*mhavecontc,
-\nd*by, \nd*beginc, \nd*resumec, \nd*endc, \nd*openc, \nd*closec,
-\nd*guardc.
+Commands exported by layer C are: \nd at hypoc, \nd at havec, \nd at hypocontc,
+\nd at havecontc, \nd at mhypoc, \nd at mhavec, \nd at mhypocontc, \nd at mhavecontc,
+\nd at by, \nd at beginc, \nd at resumec, \nd at endc, \nd at openc, \nd at closec,
+\nd at guardc.
The layer C macros work by storing each line in a data structure
-\ppp,\nd*typ,\nd*byt. The line is ejected when the beginning of the
+\ppp,\nd at typ,\nd at byt. The line is ejected when the beginning of the
next line is read, and once at the very end. In this way, we can put
in the correct line breaks (whether or not the line carries a
justification), and a hypothesis does not get typeset until we know
-whether it is followed by another hypothesis. \nd*sto stores a new
-line, \nd*clr clears the current line, \nd*cmd outputs the current
+whether it is followed by another hypothesis. \nd at sto stores a new
+line, \nd at clr clears the current line, \nd at cmd outputs the current
line.
Example of layer C syntax:
\[
- \nd*beginc
- \nd*hypoc {1}{\neg\exists xP(x)}
- \nd*openc
- \nd*guardc {1}{u}
- \nd*openc
- \nd*hypoc {2}{P(u)}
- \nd*havec {3}{\exists xP(x)} \nd*by{$\exists$I}{2}
- \nd*havec {4}{\neg\exists xP(x)} \nd*by{R}{1}
- \nd*havec {5}{\bot} \nd*by{$\neg$E}{3,4}
- \nd*closec
- \nd*havec {6}{\neg P(u)} \nd*by{$\neg$I}{2-5}
- \nd*closec
- \nd*havec {7}{\forall y\neg P(y)} \nd*by{$\forall$I}{2-6}
- \nd*endc
+ \nd at beginc
+ \nd at hypoc {1}{\neg\exists xP(x)}
+ \nd at openc
+ \nd at guardc {1}{u}
+ \nd at openc
+ \nd at hypoc {2}{P(u)}
+ \nd at havec {3}{\exists xP(x)} \nd at by{$\exists$I}{2}
+ \nd at havec {4}{\neg\exists xP(x)} \nd at by{R}{1}
+ \nd at havec {5}{\bot} \nd at by{$\neg$E}{3,4}
+ \nd at closec
+ \nd at havec {6}{\neg P(u)} \nd at by{$\neg$I}{2-5}
+ \nd at closec
+ \nd at havec {7}{\forall y\neg P(y)} \nd at by{$\forall$I}{2-6}
+ \nd at endc
\]
LAYER D
@@ -250,24 +250,24 @@
nd, except that it continues a proof in progress (with continuous
nesting and labeling).
-The macros \nd*hypod, \nd*haved, \nd*opend, \nd*guardd are essentially
+The macros \nd at hypod, \nd at haved, \nd at opend, \nd at guardd are essentially
the user-level macros, but with all optional argument spelled-out. The
versions without the final "d" allow the optional arguments to be
omitted.
-The functions \nd*optarg and \nd*optargg are used to handle optional
-arguments. Usage: \nd*optarg{default}{continuation}xxx - reads an
+The functions \nd at optarg and \nd at optargg are used to handle optional
+arguments. Usage: \nd at optarg{default}{continuation}xxx - reads an
optional argument, supplies default if necessary, then continues with
continuation. Continuation expects optional argument between
-[...]. I.e., \nd*optarg{d}{c}[xxx] => c[xxx], and \nd*optarg{d}{c}x =>
-c[d]x if x != '['. Behavior is undefined if x is {[...}. \nd*optargg
+[...]. I.e., \nd at optarg{d}{c}[xxx] => c[xxx], and \nd at optarg{d}{c}x =>
+c[d]x if x != '['. Behavior is undefined if x is {[...}. \nd at optargg
is similar except it takes two continuations: first one for optional
argument present, second for not present. It takes no default value.
-The function \nd*five{\a} reads five, partly optional arguments of the
+The function \nd at five{\a} reads five, partly optional arguments of the
shape [][]{}[]{}, then call \a with these arguments.
-Finally, \nd*init puts all the commands which are visible inside an
+Finally, \nd at init puts all the commands which are visible inside an
nd-environment in the current name space.
Example of a derivation using layer D syntax. As before, the "line
Modified: trunk/Master/texmf-dist/doc/latex/fitch/fitchdoc.pdf
===================================================================
(Binary files differ)
Modified: trunk/Master/texmf-dist/doc/latex/fitch/fitchdoc.tex
===================================================================
--- trunk/Master/texmf-dist/doc/latex/fitch/fitchdoc.tex 2023-12-18 20:55:50 UTC (rev 69159)
+++ trunk/Master/texmf-dist/doc/latex/fitch/fitchdoc.tex 2023-12-18 20:56:00 UTC (rev 69160)
@@ -18,9 +18,9 @@
% 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/
@@ -27,7 +27,7 @@
\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,8 +63,8 @@
\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
@@ -63,8 +71,7 @@
produced it:
\begin{LTXexample}
-\[
-\begin{nd}
+$\begin{nd}
\hypo {1} {P\vee Q}
\hypo {2} {\neg Q}
\open
@@ -78,25 +85,50 @@
\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 @@
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 \\
+\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!\oi! & or introduction \\
- \verb!\oe! & or elimination \\
- \verb!\ni! & not introduction \\
- \verb!\ne! & not elimination \\
- \verb!\be! & bottom 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
-\begin{tabular}{@{}ll@{}}
- \verb!\nne! & double negation elimination \\
- \verb!\Ai! & forall introduction \\
- \verb!\Ae! & forall elimination \\
- \verb!\Ei! & exists introduction \\
- \verb!\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 @@
the following example:
\begin{LTXexample}
-\[
+$
\begin{nd}
\hypo {1} {\exists x\forall y.P(x,y)}
\open[v]
@@ -161,11 +189,11 @@
\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}
@@ -172,76 +200,106 @@
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.
+% by giving an optional second argument to the |\hypo| and
+% |\have| commands. The use of this feature is discouraged.
-\subsection{Generic justifications}
+\subsection{Label and reference list details}\label{subsec-ndref}
-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:
-
+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}
+(In earlier versions, this resulted in an error, not a warning.)
-\subsection{Referencing line numbers in the text}
-\label{subsec-ndref}
-
\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 @@
\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,84 +375,227 @@
{\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}
-\verb!\nddim{4.5ex}{3.5ex}{1.5ex}{1em}{1.6em}{.5em}{2.5em}{.2mm}!.
+\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}
-\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.
-\subsection{Other comments}
+\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}
+ \cmd{\nddim}\marg{height}\marg{topheight}\marg{depth}\marg{labelsep}
+ \marg{indent}\marg{hsep}\marg{justsep}\marg{linethickness},
+\end{center}
+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 at ...|. Any low-level redefinition of |fitch| internals that uses
+|*| will break in v1.0.
+
+\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.
With this package, it is in fact possible to typeset incomplete,
@@ -399,8 +608,8 @@
\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}
Modified: trunk/Master/texmf-dist/tex/latex/fitch/fitch.sty
===================================================================
--- trunk/Master/texmf-dist/tex/latex/fitch/fitch.sty 2023-12-18 20:55:50 UTC (rev 69159)
+++ trunk/Master/texmf-dist/tex/latex/fitch/fitch.sty 2023-12-18 20:56:00 UTC (rev 69160)
@@ -18,9 +18,9 @@
% Original Author: Peter Selinger, Dalhousie University
% Created: Jan 14, 2002
-% Modified: Sep 4, 2023
-% Version: 0.6
-% Copyright: (C) 2002-2005 Peter Selinger
+% Modified: December 17, 2023
+% Version: 1.0
+% Copyright: (C) 2002-2005 Peter Selinger, Richard Zach
% Filename: fitch.sty
% Documentation: fitchdoc.tex
% https://github.com/OpenLogicProject/fitch/
@@ -50,159 +50,222 @@
% \]
\NeedsTeXFormat{LaTeX2e}
-\ProvidesPackage{fitch}[2023-09-04 v0.6 Macros for Fitch-style natural deduction]
+\ProvidesPackage{fitch}[2023-12-17 v1.0 Macros for Fitch-style natural deduction]
-{\chardef\x=\catcode`\*
-\catcode`\*=11
-\global\let\nd*astcode\x}
-\catcode`\*=11
+% Define keyval options
+\RequirePackage{kvoptions}
+
+\SetupKeyvalOptions{
+family = fitch,
+prefix = nd@ % prefix with nd@ for compatibility with old code
+}
+
+\DeclareStringOption[ndrules]{rules}
+\DeclareStringOption[array]{arrayenv}
+\DeclareStringOption[ndjustformat]{justformat}
+\DeclareStringOption[ndrefformat]{refformat}
+
+\DeclareStringOption[4.5ex]{height}[4.5ex]
+\DeclareStringOption[3.5ex]{topheight}[3.5ex]
+\DeclareStringOption[1.5ex]{depth}[1.5ex]
+\DeclareStringOption[1em]{labelsep}[1em]
+\DeclareStringOption[1.6em]{indent}[1.6em]
+\DeclareStringOption[1.5ex]{hsep}[1.5ex]
+\DeclareStringOption[2.5em]{justsep}[2.5em]
+\DeclareStringOption[.2mm]{linethickness}[.2mm]
+\DeclareStringOption[1em]{cindent}[1em]
+\DeclareBoolOption[true]{outerline}
+
+% user command to redefine dimensions
+\def\nddim#1#2#3#4#5#6#7#8{
+ \setkeys{fitch}{
+ height=#1,
+ topheight=#2,
+ depth=#3,
+ labelsep=#4,
+ indent=#5,
+ hsep=#6,
+ justsep=#7,
+ linethickness=#8
+ }
+}
+
+\DeclareLocalOptions{
+ rules,
+ arrayenv,
+ justformat,
+ refformat,
+ height,
+ topheight,
+ depth,
+ labelsep,
+ indent,
+ hsep,
+ justsep,
+ linethickness,
+ cindent,
+ outerline
+}
+
+\ProcessLocalKeyvalOptions{fitch}
+
+% Actual fitch.sty code
+
+\newlength{\nd at dim}
+
% References
-\newcount\nd*ctr
-\def\nd*render{\expandafter\ifx\expandafter\nd*x\nd*base\nd*x\the\nd*ctr\else\nd*base\ifnum\nd*ctr<0\the\nd*ctr\else\ifnum\nd*ctr>0+\the\nd*ctr\fi\fi\fi}
-\expandafter\def\csname nd*-\endcsname{}
+\newcount\nd at ctr
+\def\nd at render{\expandafter\ifx\expandafter\nd at x\nd at base\nd at x\the\nd at ctr\else\nd at base\ifnum\nd at ctr<0\the\nd at ctr\else\ifnum\nd at ctr>0+\the\nd at ctr\fi\fi\fi}
+\expandafter\def\csname nd at -\endcsname{}
-\def\nd*num#1{\nd*numo{\nd*render}{#1}\global\advance\nd*ctr1}
-\def\nd*numopt#1#2{\nd*numo{$#1$}{#2}}
-\def\nd*numo#1#2{\edef\x{#1}\mbox{$\x$}\expandafter\global\expandafter\let\csname nd*-#2\endcsname\x}
-\def\nd*ref#1{\expandafter\let\expandafter\x\csname nd*-#1\endcsname\ifx\x\relax%
- \PackageWarning{fitch}{Undefined line reference: #1}\mbox{\textbf{??}}\else\mbox{$\x$}\fi}
-\def\nd*noop{}
-\def\nd*set#1#2{\ifx\relax#1\nd*noop\else\global\def\nd*base{#1}\fi\ifx\relax#2\relax\else\global\nd*ctr=#2\fi}
-\def\nd*reset{\nd*set{}{1}}
-\def\nd*refa#1{\nd*ref{#1}}
-\def\nd*aux#1#2{\ifx#2-\nd*refa{#1}--\def\nd*c{\nd*aux{}}%
- \else\ifx#2,\nd*refa{#1}, \def\nd*c{\nd*aux{}}%
- \else\ifx#2;\nd*refa{#1}; \def\nd*c{\nd*aux{}}%
- \else\ifx#2.\nd*refa{#1}. \def\nd*c{\nd*aux{}}%
- \else\ifx#2)\nd*refa{#1})\def\nd*c{\nd*aux{}}%
- \else\ifx#2(\nd*refa{#1}(\def\nd*c{\nd*aux{}}%
- \else\ifx#2\nd*end\nd*refa{#1}\def\nd*c{}%
- \else\def\nd*c{\nd*aux{#1#2}}%
- \fi\fi\fi\fi\fi\fi\fi\nd*c}
-\def\ndref#1{\nd*aux{}#1\nd*end}
+\def\nd at num#1{\nd at numo{\nd at render}{#1}\global\advance\nd at ctr1}
+\def\nd at numopt#1#2{\nd at numo{$#1$}{#2}}
+\def\nd at numo#1#2{\edef\x{#1}\mbox{$\x$}\expandafter\global\expandafter\let\csname nd at -#2\endcsname\x}
+\def\nd at ref#1{\expandafter\let\expandafter\x\csname nd at -#1\endcsname\ifx\x\relax%
+ \PackageWarning{fitch}{Undefined line reference: #1}\mbox{\textbf{??}}\else\csname\nd at refformat\endcsname{\mbox{$\x$}}\fi}
+\def\nd at noop{}
+\def\nd at set#1#2{\ifx\relax#1\nd at noop\else\global\def\nd at base{#1}\fi\ifx\relax#2\relax\else\global\nd at ctr=#2\fi}
+\def\nd at reset{\nd at set{}{1}}
+\def\nd at refa#1{\nd at ref{#1}}
+\def\nd at aux#1#2{\ifx#2-\nd at refa{#1}--\def\nd at c{\nd at aux{}}%
+ \else\ifx#2,\nd at refa{#1}, \def\nd at c{\nd at aux{}}%
+ \else\ifx#2;\nd at refa{#1}; \def\nd at c{\nd at aux{}}%
+ \else\ifx#2.\nd at refa{#1}. \def\nd at c{\nd at aux{}}%
+ \else\ifx#2)\nd at refa{#1})\def\nd at c{\nd at aux{}}%
+ \else\ifx#2(\nd at refa{#1}(\def\nd at c{\nd at aux{}}%
+ \else\ifx#2\nd at end\nd at refa{#1}\def\nd at c{}%
+ \else\def\nd at c{\nd at aux{#1#2}}%
+ \fi\fi\fi\fi\fi\fi\fi\nd at c}
+\def\ndref#1{\nd at aux{}#1\nd at end}
% Layer A
-% define various dimensions (explained in fitchdoc.tex):
-\newlength{\nd*dim}
-\newdimen\nd*depthdim
-\newdimen\nd*hsep
-\newdimen\ndindent
-\ndindent=1em
-% user command to redefine dimensions
-\def\nddim#1#2#3#4#5#6#7#8{\nd*depthdim=#3\relax\nd*hsep=#6\relax%
-\def\nd*height{#1}\def\nd*thickness{#8}\def\nd*initheight{#2}%
-\def\nd*indent{#5}\def\nd*labelsep{#4}\def\nd*justsep{#7}}
% set initial dimensions
-\nddim{4.5ex}{3.5ex}{1.5ex}{1em}{1.6em}{.5em}{2.5em}{.2mm}
+%\nddim{4.5ex}{3.5ex}{1.5ex}{1em}{1.6em}{.5em}{2.5em}{.2mm}
-\def\nd*v{\rule[-\nd*depthdim]{\nd*thickness}{\nd*height}}
-\def\nd*t{\rule[-\nd*depthdim]{0mm}{\nd*height}\rule[-\nd*depthdim]{\nd*thickness}{\nd*initheight}}
-\def\nd*i{\hspace{\nd*indent}}
-\def\nd*s{\hspace{\nd*hsep}}
-\def\nd*g#1{\nd*f{\makebox[\nd*indent][c]{$#1$}}}
-\def\nd*f#1{\raisebox{0pt}[0pt][0pt]{$#1$}}
-\def\nd*u#1{\makebox[0pt][l]{\settowidth{\nd*dim}{\nd*f{#1}}%
- \addtolength{\nd*dim}{2\nd*hsep}\hspace{-\nd*hsep}\rule[-\nd*depthdim]{\nd*dim}{\nd*thickness}}\nd*f{#1}}
+\def\nd at v{\rule[-\nd at depth]{\nd at linethickness}{\nd at height}}
+\def\nd at h{\rule[-\nd at depth]{0mm}{\nd at height}} % strut
+\def\nd at t{\rule[-\nd at depth]{\nd at linethickness}{\nd at topheight}}
+\def\nd at i{\hspace{\nd at indent}}
+\def\nd at s{\hspace{\nd at hsep}}
+\def\nd at g#1{\nd at f{\makebox[\nd at indent][c]{$#1$}}}
+\def\nd at f#1{\raisebox{0pt}[0pt][0pt]{$#1$}}
+\def\nd at u#1{\makebox[0pt][l]{\settowidth{\nd at dim}{\nd at f{#1}}%
+ \addtolength{\nd at dim}{\nd at hsep}\addtolength{\nd at dim}{\nd at hsep}%
+ \hspace{-\nd at hsep}\rule[-\nd at depth]{\nd at dim}{\nd at linethickness}}\nd at f{#1}}
% Lists
-\def\nd*push#1#2{\expandafter\gdef\expandafter#1\expandafter%
- {\expandafter\nd*cons\expandafter{#1}{#2}}}
-\def\nd*pop#1{{\def\nd*nil{\gdef#1{\nd*nil}}\def\nd*cons##1##2%
+\def\nd at push#1#2{\expandafter\gdef\expandafter#1\expandafter%
+ {\expandafter\nd at cons\expandafter{#1}{#2}}}
+\def\nd at pop#1{{\def\nd at nil{\gdef#1{\nd at nil}}\def\nd at cons##1##2%
{\gdef#1{##1}}#1}}
-\def\nd*iter#1#2{{\def\nd*nil{}\def\nd*cons##1##2{##1#2{##2}}#1}}
-\def\nd*modify#1#2#3{{\def\nd*nil{\gdef#1{\nd*nil}}\def\nd*cons##1##2%
- {\advance#2-1 ##1\advance#2 1 \ifnum#2=1\nd*push#1{#3}\else%
- \nd*push#1{##2}\fi}#1}}
+\def\nd at iter#1#2{{\def\nd at nil{}\def\nd at cons##1##2{##1#2{##2}}#1}}
+\def\nd at modify#1#2#3{{\def\nd at nil{\gdef#1{\nd at nil}}\def\nd at cons##1##2%
+ {\advance#2-1 ##1\advance#2 1 \ifnum#2=1\nd at push#1{#3}\else%
+ \nd at push#1{##2}\fi}#1}}
-\def\nd*cont#1{{\def\nd*t{\nd*v}\def\nd*v{\nd*v}\def\nd*g##1{\nd*i}%
- \def\nd*i{\nd*i}\def\nd*nil{\gdef#1{\nd*nil}}\def\nd*cons##1##2%
- {##1\expandafter\nd*push\expandafter#1\expandafter{##2}}#1}}
+\def\nd at cont#1{{\def\nd at t{\nd at v}\def\nd at v{\nd at v}\def\nd at g##1{\nd at i}%
+ \def\nd at i{\nd at i}\def\nd at nil{\gdef#1{\nd at nil}}\def\nd at cons##1##2%
+ {##1\expandafter\nd at push\expandafter#1\expandafter{##2}}#1}}
% Layer B
-\newcount\nd*n
-\def\nd*beginb{\begingroup\nd*reset\gdef\nd*stack{\nd*nil}\nd*push\nd*stack{\nd*t}%
- \begin{array}{l@{\hspace{\nd*labelsep}}l@{\hspace{\nd*justsep}}l}}
-\def\nd*resumeb{\begingroup\begin{array}{l@{\hspace{\nd*labelsep}}l@{\hspace{\nd*justsep}}l}}
-\def\nd*endb{\end{array}\endgroup}
-\def\nd*hypob#1#2{\nd*f{\nd*num{#1}}&\nd*iter\nd*stack\relax\nd*cont\nd*stack\nd*s\nd*u{#2}&}
-\def\nd*haveb#1#2{\nd*f{\nd*num{#1}}&\nd*iter\nd*stack\relax\nd*cont\nd*stack\nd*s\nd*f{#2}&}
-\def\nd*havecontb#1#2{&\nd*iter\nd*stack\relax\nd*cont\nd*stack\nd*s\nd*f{\hspace{\ndindent}#2}&}
-\def\nd*hypocontb#1#2{&\nd*iter\nd*stack\relax\nd*cont\nd*stack\nd*s\nd*u{\hspace{\ndindent}#2}&}
+\newcount\nd at n
+\def\nd at beginb{%
+ \begingroup
+ \nd at reset
+ \gdef\nd at stack{\nd at nil}%
+ \nd at push\nd at stack{\nd at h}%
+ \ifnd at outerline
+ \nd at push\nd at stack{\nd at t}\fi
+ \begin{\nd at arrayenv}{l@{\hspace{\nd at labelsep}}l@{\hspace{\nd at justsep}}l}}
+\def\nd at resumeb{%
+ \begingroup
+ \begin{\nd at arrayenv}{l@{\hspace{\nd at labelsep}}l@{\hspace{\nd at justsep}}l}}
+\def\nd at endb{\end{\nd at arrayenv}\endgroup}
+\def\nd at hypob#1#2{\nd at f{\nd at num{#1}}&\nd at iter\nd at stack\relax\nd at cont\nd at stack\nd at s\nd at u{#2}&}
+\def\nd at haveb#1#2{\nd at f{\nd at num{#1}}&\nd at iter\nd at stack\relax\nd at cont\nd at stack\nd at s\nd at f{#2}&}
+\def\nd at havecontb#1#2{&\nd at iter\nd at stack\relax\nd at cont\nd at stack\nd at s\nd at f{\hspace{\nd at cindent}#2}&}
+\def\nd at hypocontb#1#2{&\nd at iter\nd at stack\relax\nd at cont\nd at stack\nd at s\nd at u{\hspace{\nd at cindent}#2}&}
-\def\nd*openb{\nd*push\nd*stack{\nd*i}\nd*push\nd*stack{\nd*t}}
-\def\nd*closeb{\nd*pop\nd*stack\nd*pop\nd*stack}
-\def\nd*guardb#1#2{\nd*n=#1\multiply\nd*n by 2 \nd*modify\nd*stack\nd*n{\nd*g{#2}}}
+\def\nd at openb{\nd at push\nd at stack{\nd at i}\nd at push\nd at stack{\nd at t}}
+\def\nd at closeb{\nd at pop\nd at stack\nd at pop\nd at stack}
+\def\nd at guardb#1#2{\nd at n=#1\multiply\nd at n by 2 \nd at modify\nd at stack\nd at n{\nd at g{#2}}}
% Layer C
-\def\nd*clr{\gdef\nd*cmd{}\gdef\nd*typ{\relax}}
-\def\nd*sto#1#2#3{\gdef\nd*typ{#1}\gdef\nd*byt{}%
- \gdef\nd*cmd{\nd*typ{#2}{#3}\nd*byt\\}}
-\def\nd*chtyp{\expandafter\ifx\nd*typ\nd*hypocontb\def\nd*typ{\nd*havecontb}\else\def\nd*typ{\nd*haveb}\fi}
-\def\nd*hypoc#1#2{\nd*chtyp\nd*cmd\nd*sto{\nd*hypob}{#1}{#2}}
-\def\nd*havec#1#2{\nd*cmd\nd*sto{\nd*haveb}{#1}{#2}}
-\def\nd*hypocontc#1{\nd*chtyp\nd*cmd\nd*sto{\nd*hypocontb}{}{#1}}
-\def\nd*havecontc#1{\nd*cmd\nd*sto{\nd*havecontb}{}{#1}}
-\def\nd*by#1#2{\ifx\nd*x#2\nd*x\gdef\nd*byt{\mbox{#1}}\else\gdef\nd*byt{\mbox{#1, \ndref{#2}}}\fi}
+\def\nd at clr{\gdef\nd at cmd{}\gdef\nd at typ{\relax}}
+\def\nd at sto#1#2#3{\gdef\nd at typ{#1}\gdef\nd at byt{}%
+ \gdef\nd at cmd{\nd at typ{#2}{#3}\nd at byt\\}}
+\def\nd at chtyp{\expandafter\ifx\nd at typ\nd at hypocontb\def\nd at typ{\nd at havecontb}\else\def\nd at typ{\nd at haveb}\fi}
+\def\nd at hypoc#1#2{\nd at chtyp\nd at cmd\nd at sto{\nd at hypob}{#1}{#2}}
+\def\nd at havec#1#2{\nd at cmd\nd at sto{\nd at haveb}{#1}{#2}}
+\def\nd at hypocontc#1{\nd at chtyp\nd at cmd\nd at sto{\nd at hypocontb}{}{#1}}
+\def\nd at havecontc#1{\nd at cmd\nd at sto{\nd at havecontb}{}{#1}}
+\def\nd at by#1#2{\ifx\nd at x#2\nd at x\gdef\nd at byt{\mbox{#1}}\else\ifx\nd at x#1\nd at x\gdef\nd at byt{\mbox{\ndref{#2}}}\else\gdef\nd at byt{\mbox{\csname\nd at justformat\endcsname{#1}{\ndref{#2}}}}\fi\fi\ignorespaces}
% multi-line macros
-\def\nd*mhypoc#1#2{\nd*mhypocA{#1}#2\\\nd*stop\\}
-\def\nd*mhypocA#1#2\\{\nd*hypoc{#1}{#2}\nd*mhypocB}
-\def\nd*mhypocB#1\\{\ifx\nd*stop#1\else\nd*hypocontc{#1}\expandafter\nd*mhypocB\fi}
-\def\nd*mhavec#1#2{\nd*mhavecA{#1}#2\\\nd*stop\\}
-\def\nd*mhavecA#1#2\\{\nd*havec{#1}{#2}\nd*mhavecB}
-\def\nd*mhavecB#1\\{\ifx\nd*stop#1\else\nd*havecontc{#1}\expandafter\nd*mhavecB\fi}
-\def\nd*mhypocontc#1{\nd*mhypocB#1\\\nd*stop\\}
-\def\nd*mhavecontc#1{\nd*mhavecB#1\\\nd*stop\\}
+\def\nd at mhypoc#1#2{\nd at mhypocA{#1}#2\\\nd at stop\\}
+\def\nd at mhypocA#1#2\\{\nd at hypoc{#1}{#2}\nd at mhypocB}
+\def\nd at mhypocB#1\\{\ifx\nd at stop#1\else\nd at hypocontc{#1}\expandafter\nd at mhypocB\fi}
+\def\nd at mhavec#1#2{\nd at mhavecA{#1}#2\\\nd at stop\\}
+\def\nd at mhavecA#1#2\\{\nd at havec{#1}{#2}\nd at mhavecB}
+\def\nd at mhavecB#1\\{\ifx\nd at stop#1\else\nd at havecontc{#1}\expandafter\nd at mhavecB\fi}
+\def\nd at mhypocontc#1{\nd at mhypocB#1\\\nd at stop\\}
+\def\nd at mhavecontc#1{\nd at mhavecB#1\\\nd at stop\\}
-\def\nd*beginc{\nd*beginb\nd*clr}
-\def\nd*resumec{\nd*resumeb\nd*clr}
-\def\nd*endc{\nd*cmd\nd*endb}
-\def\nd*openc{\nd*cmd\nd*clr\nd*openb}
-\def\nd*closec{\nd*cmd\nd*clr\nd*closeb}
-\let\nd*guardc\nd*guardb
+\def\nd at beginc{\nd at beginb\nd at clr}
+\def\nd at resumec{\nd at resumeb\nd at clr}
+\def\nd at endc{\nd at cmd\nd at endb}
+\def\nd at openc{\nd at cmd\nd at clr\nd at openb}
+\def\nd at closec{\nd at cmd\nd at clr\nd at closeb}
+\let\nd at guardc\nd at guardb
% Layer D
% macros with optional arguments spelled-out
-\def\nd*hypod[#1][#2]#3[#4]#5{\ifx\relax#4\relax\else\nd*guardb{1}{#4}\fi\nd*mhypoc{#3}{#5}\nd*set{#1}{#2}}
-\def\nd*haved[#1][#2]#3[#4]#5{\ifx\relax#4\relax\else\nd*guardb{1}{#4}\fi\nd*mhavec{#3}{#5}\nd*set{#1}{#2}}
-\def\nd*havecont#1{\nd*mhavecontc{#1}}
-\def\nd*hypocont#1{\nd*mhypocontc{#1}}
-\def\nd*base{undefined}
-\def\nd*opend[#1]#2{\nd*cmd\nd*clr\nd*openb\nd*guard{#1}#2}
-\def\nd*close{\nd*cmd\nd*clr\nd*closeb}
-\def\nd*guardd[#1]#2{\nd*guardb{#1}{#2}}
+\def\nd at hypod[#1][#2]#3[#4]#5{\ifx\relax#4\relax\else\nd at guardb{1}{#4}\fi\nd at mhypoc{#3}{#5}\nd at set{#1}{#2}\ignorespaces}
+\def\nd at haved[#1][#2]#3[#4]#5{\ifx\relax#4\relax\else\nd at guardb{1}{#4}\fi\nd at mhavec{#3}{#5}\nd at set{#1}{#2}\ignorespaces}
+\def\nd at havecont#1{\nd at mhavecontc{#1}}
+\def\nd at hypocont#1{\nd at mhypocontc{#1}}
+\def\nd at base{undefined}
+\def\nd at opend[#1]#2{\nd at cmd\nd at clr\nd at openb\nd at guard{#1}#2}
+\def\nd at close{\nd at cmd\nd at clr\nd at closeb}
+\def\nd at guardd[#1]#2{\nd at guardb{#1}{#2}}
% Handling of optional arguments.
-\def\nd*optarg#1#2#3{\ifx[#3\def\nd*c{#2#3}\else\def\nd*c{#2[#1]{#3}}\fi\nd*c}
-\def\nd*optargg#1#2#3{\ifx[#3\def\nd*c{#1#3}\else\def\nd*c{#2{#3}}\fi\nd*c}
+\def\nd at optarg#1#2#3{\ifx[#3\def\nd at c{#2#3}\else\def\nd at c{#2[#1]{#3}}\fi\nd at c}
+\def\nd at optargg#1#2#3{\ifx[#3\def\nd at c{#1#3}\else\def\nd at c{#2{#3}}\fi\nd at c}
-\def\nd*five#1{\nd*optargg{\nd*four{#1}}{\nd*two{#1}}}
-\def\nd*four#1[#2]{\nd*optarg{0}{\nd*three{#1}[#2]}}
-\def\nd*three#1[#2][#3]#4{\nd*optarg{}{#1[#2][#3]{#4}}}
-\def\nd*two#1{\nd*three{#1}[\relax][]}
+\def\nd at five#1{\nd at optargg{\nd at four{#1}}{\nd at two{#1}}}
+\def\nd at four#1[#2]{\nd at optarg{0}{\nd at three{#1}[#2]}}
+\def\nd at three#1[#2][#3]#4{\nd at optarg{}{#1[#2][#3]{#4}}}
+\def\nd at two#1{\nd at three{#1}[\relax][]}
-\def\nd*have{\nd*five{\nd*haved}}
-\def\nd*hypo{\nd*five{\nd*hypod}}
-\def\nd*open{\nd*optarg{}{\nd*opend}}
-\def\nd*guard{\nd*optarg{1}{\nd*guardd}}
+\def\nd at have{\nd at five{\nd at haved}}
+\def\nd at hypo{\nd at five{\nd at hypod}}
+\def\nd at open{\nd at optarg{}{\nd at opend}}
+\def\nd at guard{\nd at optarg{1}{\nd at guardd}}
-\def\nd*init{%
- \let\open\nd*open%
- \let\close\nd*close%
- \let\hypo\nd*hypo%
- \let\have\nd*have%
- \let\hypocont\nd*hypocont%
- \let\havecont\nd*havecont%
- \let\by\nd*by%
- \let\guard\nd*guard%
+\def\nd at init{%
+ \let\open\nd at open%
+ \let\close\nd at close%
+ \let\hypo\nd at hypo%
+ \let\have\nd at have%
+ \let\hypocont\nd at hypocont%
+ \let\havecont\nd at havecont%
+ \let\by\nd at by%
+ \let\guard\nd at guard%
+ \csname\nd at rules\endcsname
+}
+
+% Define default rule names
+
+\def\ndrules{%
\def\ii{\by{$\Rightarrow$I}}%
\def\ie{\by{$\Rightarrow$E}}%
\def\Ai{\by{$\forall$I}}%
@@ -219,13 +282,34 @@
\def\ne{\by{$\neg$E}}%
\def\be{\by{$\bot$E}}%
\def\nne{\by{$\neg\neg$E}}%
- \def\r{\by{R}}%
-}
+ \def\r{\by{R}}}
-\newenvironment{nd}{\begingroup\nd*init\nd*beginc}{\nd*endc\endgroup}
-\newenvironment{ndresume}{\begingroup\nd*init\nd*resumec}{\nd*endc\endgroup}
+% default justification format
-\catcode`\*=\nd*astcode
+\newcommand{\ndjustformat}[2]{#1, #2}
+% default line number format
+
+\newcommand{\ndrefformat}[1]{#1}
+
+% User-level commands for proofs
+
+\newenvironment{nd}[1][]
+ {\begingroup
+ \setkeys{fitch}{#1}%
+ \nd at init\nd at beginc\ignorespaces}
+ {\nd at endc\endgroup}
+\newenvironment{ndresume}[1][]
+ {\begingroup
+ \setkeys{fitch}{#1}%
+ \nd at init\nd at resumec\ignorespaces}
+ {\nd at endc\endgroup}
+\newenvironment{fitchproof}[1][]
+ {\begin{list}{}{\setlength{\leftmargin}{0pt}}\item\begin{nd}[#1]}
+ {\end{nd}\end{list}}
+\newenvironment{fitchproof*}[1][]
+ {\begin{list}{}{\setlength{\leftmargin}{0pt}}\item\begin{ndresume}[#1]}
+ {\end{ndresume}\end{list}}
+
% End of file fitch.sty
More information about the tex-live-commits
mailing list.