summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/doc/latex
diff options
context:
space:
mode:
authorKarl Berry <karl@freefriends.org>2023-09-05 20:05:11 +0000
committerKarl Berry <karl@freefriends.org>2023-09-05 20:05:11 +0000
commitf886123ec8e5ba2e4ffe6ce9cd57a88a803ae502 (patch)
tree337b238cb20061c2217fdff6094ca1f1e194f330 /Master/texmf-dist/doc/latex
parentb47027a7c4103e9c77f75e62761b446adcfb62fb (diff)
fitch (5sep23)
git-svn-id: svn://tug.org/texlive/trunk@68179 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Master/texmf-dist/doc/latex')
-rw-r--r--Master/texmf-dist/doc/latex/fitch/README.md82
-rw-r--r--Master/texmf-dist/doc/latex/fitch/fitch.hacker.txt314
-rw-r--r--Master/texmf-dist/doc/latex/fitch/fitchdoc-dimen.pdfbin0 -> 7325 bytes
-rw-r--r--Master/texmf-dist/doc/latex/fitch/fitchdoc.pdfbin0 -> 248637 bytes
-rw-r--r--Master/texmf-dist/doc/latex/fitch/fitchdoc.tex406
-rw-r--r--Master/texmf-dist/doc/latex/fitch/fitchexample.pngbin0 -> 4727 bytes
6 files changed, 802 insertions, 0 deletions
diff --git a/Master/texmf-dist/doc/latex/fitch/README.md b/Master/texmf-dist/doc/latex/fitch/README.md
new file mode 100644
index 00000000000..1208f4f2dd2
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/fitch/README.md
@@ -0,0 +1,82 @@
+# fitch.sty
+
+LaTeX macros for Fitch style natural deduction
+
+## Usage
+
+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)
+
+With these macros, one can typeset natural deduction proofs in Fitch
+style, as in the following example:
+
+![](fitchexample.png)
+
+```
+\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.
+
+## Changes
+
+**v0.6, Sept 4, 2023.** Updated the documentation and license (from
+GPL to LPPL). The code is essentially unchanged.
+
+**v0.5, Feb 8, 2005.** The ability to handle multi-line formulas
+was added.
+
+## Download
+
+The package is available on CTAN as
+[`fitch`](https://ctan.org/pkg/fitch).
+
+The code is [maintained on Github](https://github.com/OpenLogicProject/fitch/).
+
+## 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.
+
+Additional packages for proofs, including Johan Klüwer's, are
+available at a [page maintained by Alex Kocurek](https://www.actual.world/latex/)
+
+## People
+
+Peter Selinger, Dalhousie University, is the original author.
+
+Richard Zach, University of Calgary, it the current maintainer.
+
+## License
+
+Copyright (C) 2002-2023 Peter Selinger
+
+This work may be distributed and/or modified under the conditions of
+the LaTeX Project Public License, either version 1.3 of this license
+or (at your option) any later version. The latest version of this
+license is in
+
+ https://www.latex-project.org/lppl.txt
+
+and version 1.3c or later is part of all distributions of LaTeX
+version 2008 or later. \ No newline at end of file
diff --git a/Master/texmf-dist/doc/latex/fitch/fitch.hacker.txt b/Master/texmf-dist/doc/latex/fitch/fitch.hacker.txt
new file mode 100644
index 00000000000..df4af5c4da6
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/fitch/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}
+\]
diff --git a/Master/texmf-dist/doc/latex/fitch/fitchdoc-dimen.pdf b/Master/texmf-dist/doc/latex/fitch/fitchdoc-dimen.pdf
new file mode 100644
index 00000000000..33f61cb99e6
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/fitch/fitchdoc-dimen.pdf
Binary files differ
diff --git a/Master/texmf-dist/doc/latex/fitch/fitchdoc.pdf b/Master/texmf-dist/doc/latex/fitch/fitchdoc.pdf
new file mode 100644
index 00000000000..c0948c9096a
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/fitch/fitchdoc.pdf
Binary files differ
diff --git a/Master/texmf-dist/doc/latex/fitch/fitchdoc.tex b/Master/texmf-dist/doc/latex/fitch/fitchdoc.tex
new file mode 100644
index 00000000000..1889721dd09
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/fitch/fitchdoc.tex
@@ -0,0 +1,406 @@
+%% fitchdoc.tex
+%% Macros for Fitch-style natural deduction (documentation)
+%% Copyright 2002-2023 Peter Selinger
+%
+% This work may be distributed and/or modified under the
+% conditions of the LaTeX Project Public License, either version 1.3
+% of this license or (at your option) any later version.
+% The latest version of this license is in
+% https://www.latex-project.org/lppl.txt
+% and version 1.3c or later is part of all distributions of LaTeX
+% version 2008 or later.
+%
+% This work has the LPPL maintenance status `maintained'.
+%
+% The Current Maintainer of this work is Richard Zach <rzach@ucalgary.ca>
+%
+% This work consists of the files fitch.sty and fitchdoc.tex.
+
+% Original Author: Peter Selinger, Dalhousie University
+% Created: Jan 14, 2002
+% Modified: Sep 4, 2023
+% Version: 0.6
+% Copyright: (C) 2002-2023 Peter Selinger
+% Filename: fitch.sty
+% Documentation: fitchdoc.tex
+% https://github.com/OpenLogicProject/fitch/
+
+\documentclass{ltxdoc}
+
+\usepackage{fitch,graphicx,showexpl,fullpage}
+
+\lstset{%
+ basicstyle=\ttfamily\small,
+ commentstyle=\itshape\ttfamily\small,
+ showspaces=false,
+ showstringspaces=false,
+ breaklines=true,
+ breakautoindent=true,
+ captionpos=t
+}
+
+\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.}}
+
+\date{Version 0.6\\ September 4, 2023}
+
+\begin{document}
+\maketitle
+
+\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
+{\LaTeX} file.
+
+Here is a natural deduction derivation, together with the code that
+produced it:
+
+\begin{LTXexample}
+\[
+\begin{nd}
+ \hypo {1} {P\vee Q}
+ \hypo {2} {\neg Q}
+ \open
+ \hypo {3} {P}
+ \have {4} {P} \r{3}
+ \close
+ \open
+ \hypo {aa} {Q}
+ \have {6} {\neg Q} \r{2}
+ \have {7} {\bot} \ne{aa,6}
+ \have {8} {P} \be{7}
+ \close
+ \have {9} {P} \oe{1,3-4,aa-8}
+\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
+justification}. Moreover, each line is either a \emph{hypothesis} or a
+\emph{derived formula}. Generally, 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.
+
+\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
+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$.
+In the output, lines are automatically numbered consecutively. Labels
+may not contain any punctuation characters or spaces.
+
+\DescribeMacro{\open}\DescribeMacro{\close}
+Subderivations are opened and closed with the commands \verb!\open! and
+\verb!\close!. Finally, the following commands are provided for
+annotating lines with justifications:
+
+\medskip
+\hfill
+\begin{tabular}{@{}ll@{}}
+ \verb!\r! & reiteration \\
+ \verb!\ii! & implication introduction \\
+ \verb!\ie! & implication elimination \\
+ \verb!\ai! & and introduction \\
+ \verb!\ae! & and elimination \\
+\end{tabular}
+\hfill
+\begin{tabular}{ll}
+ \verb!\oi! & or introduction \\
+ \verb!\oe! & or elimination \\
+ \verb!\ni! & not introduction \\
+ \verb!\ne! & not elimination \\
+ \verb!\be! & bottom elimination \\
+\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
+
+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!.
+
+\section{Details}
+
+\subsection{Guards}
+
+Some natural deduction derivations with quantifiers use \emph{guards}, as in
+the following example:
+
+\begin{LTXexample}
+\[
+\begin{nd}
+ \hypo {1} {\exists x\forall y.P(x,y)}
+ \open[v]
+ \open[u]
+ \hypo {2} {\forall y.P(u,y)}
+ \have {3} {P(u,v)} \Ae{2}
+ \have {4} {\exists x.P(x,v)} \Ei{3}
+ \close
+ \have {5} {\exists x.P(x,v)} \Ee{1,2-5}
+ \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
+subderivations.
+
+\DescribeMacro{\guard}
+For most purposes, the above way of specifying guards is sufficient.
+However, there is another method, which allows a more flexible
+placement of guards: before any line, you can give the command
+\verb!\guard{u}! to add a guard $u$ to the top-level subderivation at
+that line, or \verb!\guard[n]{u}! to add a guard to the $n$th
+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.
+
+% For backward compatibility, there is a third way of specifying guards
+% by giving an optional second argument to the \verb!\hypo! and
+% \verb!\have! commands. The use of this feature is discouraged.
+
+\subsection{Generic justifications}
+
+Non-standard justifications can be created with the \verb!\by!
+command. This command takes two arguments: a name and a reference
+list. For instance, the command \verb!\by{De Morgan}{lab3,lab4}! might
+produce the output ``\mbox{De Morgan, 3, 4}''. Note that the justification
+is typeset in text mode. A comma is automatically inserted between the
+name and the reference list, unless the reference list is empty.
+
+\subsection{Label and reference list details}
+
+Labels may not contain commas, periods, semicolons, hyphens,
+parenthesis, or spaces. In a reference list, spaces are ignored (even
+within a label!), whereas commas, periods, semicolons, parenthesis,
+and hyphens are copied to the output. All other characters are
+interpreted as part of a label. Attempting to reference a label which
+has not been previously defined by any \verb!\hypo! or \verb!\have!
+command produces an error message of the form:
+
+\begin{verbatim}
+ ! Package fitch Error: Undefined line reference: lab17.
+\end{verbatim}
+
+\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
+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.
+
+\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}.
+
+\subsection{Breaking it across pages}\label{subsec-break}
+
+\DescribeMacro{\ndresume}
+The \verb!nd! environment is derived from the {\LaTeX} \verb!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!
+environment is provided to continue a previously interrupted
+derivation. Here is an example:
+
+\begin{LTXexample}
+$
+\begin{nd}
+ \hypo {1} {P\vee Q}
+ \hypo {2} {\neg Q}
+ \open
+ \hypo {3} {P}
+ \have {4} {P} \r{3}
+ \close
+ \open
+ \hypo {aa} {Q}
+ \have {6} {\neg Q} \r{2}
+\end{nd}
+$
+
+Derivations can be interrupted and
+resumed at any point.
+
+$
+\begin{ndresume}
+ \have {7} {\bot} \ne{aa,6}
+ \have {8} {P} \be{7}
+ \close
+ \have {9} {P} \oe{1,3-4,aa-8}
+\end{ndresume}
+$
+\end{LTXexample}
+
+\subsection{Custom line numbers}
+
+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!
+commands have an optional first argument which is a symbolic constant.
+For instance, \verb!\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
+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
+number to $7$. The following example illustrates this behavior:
+
+\begin{LTXexample}
+\[
+\begin{nd}
+ \hypo {1} {P\vee Q}
+ \open
+ \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}
+\]
+\end{LTXexample}
+
+Note that in the justification for line $m+1$, parentheses had to be
+put around the label $4$. There is currently no way of doing this
+automatically.
+
+{\bf Exercise.} How does one typeset an empty line number?
+
+{\bf Solution.} Since \verb!\have[]! has a special meaning as explained
+above, we need to use \verb!\have[~]! instead.
+
+\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
+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{} \\
+ 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
+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{}}
+ \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
+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}
+
+\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:
+\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. 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:
+\begin{center}
+\verb!\nddim{4.5ex}{3.5ex}{1.5ex}{1em}{1.6em}{.5em}{2.5em}{.2mm}!.
+\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}
+
+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,
+ill-formed, or invalid derivations. Sometimes it is pedagogically necessary
+to do so.
+
+There are no arbitrary limits on the size or nesting depth of a derivation,
+except for the obvious requirement of fitting horizontally on the
+printed page.
+
+\section{Copyright and license}
+
+This document and the accompanying \verb!fitch.sty! macros
+are {\copyright} 2002--2023 by Peter Selinger and distributed under
+the terms of the \href{https://www.latex-project.org/lppl/}{LPPL}.
+
+\end{document}
diff --git a/Master/texmf-dist/doc/latex/fitch/fitchexample.png b/Master/texmf-dist/doc/latex/fitch/fitchexample.png
new file mode 100644
index 00000000000..d66390786e7
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/fitch/fitchexample.png
Binary files differ