Skip to content

Commit

Permalink
finalize v1.0
Browse files Browse the repository at this point in the history
  • Loading branch information
@rzach
rzach committed Dec 17, 2023
1 parent 759722d commit a23fbfe
Show file tree
Hide file tree
Showing 3 changed files with 189 additions and 165 deletions.
256 changes: 128 additions & 128 deletions fitch.hacker.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ which is provided in the file fitchdoc.tex.

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.

Expand All @@ -22,36 +22,36 @@ 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
\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,
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
``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}
\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
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
\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
Expand All @@ -62,132 +62,132 @@ 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} \\
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 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
\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{...}
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.
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}
\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
\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
\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
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
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
\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
\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
\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
Expand All @@ -197,42 +197,42 @@ 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}.
``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.
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
\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
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
\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
Expand All @@ -250,24 +250,24 @@ 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 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
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
[...]. 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
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
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
Expand Down
Loading

0 comments on commit a23fbfe

Please sign in to comment.