add v.0.5 files unchanged

.gitignore

@@ -299,3 +299,6 @@ TSWLatexianTemp*
 # option is specified. Footnotes are the stored in a file with suffix Notes.bib.
 # Uncomment the next line to have this generated file ignored.
 #*Notes.bib
+
+*.pdf
+*.ps

README.md

@@ -0,0 +1,76 @@
+# fitch.sty
+
+# LaTeX macros for Fitch style natural deduction
+
+Fitch-style natural deduction is a system for writing proofs in
+propositional logic and predicate logic. We use it in our logic courses
+at the University of Ottawa. This is a set of easy-to-use LaTeX macros
+that I wrote for making handouts for my classes.
+
+With these macros, one can typeset natural deduction proofs in Fitch
+style, as in the following example:
+
+![](fitchexample.png){border="0"}
+
+```
+\begin{nd}
+  \hypo {1} {\forall y \neg P(y)}
+  \open          
+    \hypo {2} {\exists x P(x)}
+    \open[u]       
+      \hypo {3} {P(u)}
+      \have {4}{\forall y \neg P(y)}  \r{1}
+      \have {5} {\neg P(u)}           \Ae{4}
+      \have {6} {\bot}                \ne{3,5}
+    \close
+    \have {6a} {\bot}                 \Ee{2,3-6}
+  \close
+  \have {7} {\neg \exists x P(x)}     \ni{2-6a}
+\end{nd}         
+```
+
+The output is shown above, and the corresponding LaTeX code below.
+
+## News
+
+**Version 0.5, Feb 8, 2005.** The ability to handle multi-line formulas
+was added.
+
+## Download
+
+-   Complete source: [fitch-0.5.tgz](fitch-0.5.tgz).
+-   The documentation: [ps](fitchdoc.ps), [pdf](fitchdoc.pdf).
+-   The macros: [fitch.sty](fitch.sty).
+
+## Version
+
+Version 0.5, Feb 8, 2005
+
+## Author
+
+Peter Selinger, University of Ottawa
+
+## Web links
+
+A similar package by another author is
+
+-   [Johan Klüwer\'s Fitch Style
+    Package](http://folk.uio.no/johanw/FitchSty.html).
+
+## LICENSE
+
+Copyright (C) 2002-2005 Peter Selinger
+
+This program is free software; you can redistribute it and/or modify it
+under the terms of the GNU General Public License as published by the
+Free Software Foundation; either version 2, or (at your option) any
+later version.
+
+This program is distributed in the hope that it will be useful, but
+WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
+Public License for more details.
+
+You should have received a copy of the GNU General Public License along
+with this program; if not, write to the Free Software Foundation, Inc.,
+59 Temple Place, Suite 330, Boston, MA 02111-1307, USA.

fitch.hacker.txt

@@ -0,0 +1,314 @@
+This file describes the internals of the macros in fitch.sty. It is
+intended for programmers who might want to hack this package. For
+information on how to use the package, please see the user guide,
+which is provided in the file fitchdoc.tex.
+
+GENERAL
+
+Global identifiers defined by this package start with '\nd*'. The only
+exceptions are \ndref, \nddim, \ndindent, and the "nd" and "ndresume"
+latex environments.
+
+The macros provided by this package mix TeX and LaTeX primitives.
+LaTeX is used for \rule, \settowidth, \addtolength, \hspace...  All
+macros are assumed to be called in math mode.
+
+Translation proceeds through several layers of macros. Each layer
+consist of macros which expand into macros of the previous layer. Each
+layer may have some global state and initialization functions. Only
+the topmost layer (layer D) is directly user-accessible.
+
+REFERENCES
+
+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
+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,
+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
+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.
+
+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}
+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
+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
+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
+spacing information is contained in this layer; higher layers
+manipulate only layer A primitives.
+
+Example of a derivation using layer A syntax:
+
+\[ 
+\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}  \\
+\end{array}
+\]
+
+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 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
+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{...}
+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.
+
+With the list syntax, a derivation can be expressed like this:
+
+\[ 
+\begin{array}{lll}
+  \gdef\stack{\nd*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
+\end{array}
+\]
+
+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
+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
+the nth enclosing subderivation (counted from 1 from the
+inside). \nd*hypob introduces a hypothesis, and \nd*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
+each of them.
+
+Example of a derivation using layer B syntax. Note that the "line
+numbers" are really labels, which will be replaced by consecutive line
+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
+\]
+
+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
+\]
+
+LAYER C
+
+Layer C is a wrapper around layer B. It takes care of buffering
+information and putting it correctly into an array. Specifically, in
+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}.
+
+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.
+
+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
+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
+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
+\]
+
+LAYER D
+
+Layer D is the syntax used by the end user. It is implemented as a
+wrapper around layer C, providing three additional conveniences: (1) a
+latex environment, (2) guard as optional argument to \have, \hypo, or
+\open, (3) optional relabeling arguments. The user level commands are
+similar to those of layer C: they are called \begin{nd}, \end{nd},
+\open, \close, \hypo, \have, \guard, \by.  For convenience, a number
+of abbreviations are also provided for writing justifications. For
+instance \ie for \by{$\Rightarrow$E} etc. These commands are only
+visible inside an nd-environment; thus they do not interfere with the
+global name space. There is also an environment ndresume which is like
+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 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
+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
+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
+shape [][]{}[]{}, then call \a with these arguments.
+
+Finally, \nd*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
+numbers" are really labels, which will be replaced by consecutive line
+numbers in the output.
+
+\[
+\begin{nd}
+  \hypo{1}  {P\vee Q}   
+  \hypo{2}  {\neg Q}                         
+  \open                              
+  \hypo{3a} {P}
+  \have{3b} {P}        \r{3a}
+  \close                   
+  \open
+  \hypo{4a} {Q}
+  \have{4b} {\neg Q}   \r{2}
+  \have{4c} {\bot}     \ne{4a,4b}
+  \have{4d} {P}        \be{4c}
+  \close                             
+  \have{5}  {P}        \oe{1,3a-3b,4a-4d}                 
+\end{nd}
+\]
+
+Another example of layer D syntax, using guards and relabelings:
+
+\[
+\begin{nd}
+  \hypo          {1} {P\vee Q}
+  \open[u]
+  \hypo          {2} {P}
+  \have [\vdots] {3} {\vdots}
+  \have [n][-1]  {4} {A\wedge B}
+  \close
+  \open
+  \hypo          {5} {Q}
+  \have [\vdots] {6} {\vdots}
+  \have [m]      {7} {A\wedge B}
+  \close
+  \have          {8} {A\wedge B}  \oe{1,2-(4),5-7}
+  \have [\vdots] {9} {\vdots}
+  \have [][100] {10} {A}          \ae{8}
+\end{nd}
+\]