forallxcam.sty

%!TEX root = forallxcam.tex
% The original forallx.sty was written in 2005 by PD Magnus
% This version is 2018
\ProvidesPackage{forallxcam}[support for forallx:Cambridge]
\usepackage{amsmath, hyperref, multicol,  graphicx, ifthen, rotating, color}

%    ****************************************
%    *            LOGICAL SYMBOLS           *
%    ****************************************
\def\eor{\ensuremath{\vee}} % logical or
\def\eand{\ensuremath{\wedge}} % logical and
\def\eif{\ensuremath{\rightarrow}} % logical conditional
\def\eiff{\ensuremath{\leftrightarrow}} % logical biconditional
\def\enot{\ensuremath{\neg}} % logical not 
\def\ered{\ensuremath{\bot}}% used for absurdity in proofs
\def\maththe{\rotatebox[origin=c]{180}{$\iota$}} % the definite description operator
\def\proves{\ensuremath{\vdash}}
\def\entails{\ensuremath{\vDash}}
\def\nproves{\ensuremath{\nvdash}}
\def\nentails{\ensuremath{\nvDash}}
\newcommand*{\blank}{\underline{\hspace*{2em}}}
\newcommand*{\gap}[1]{\blank$_{#1}$} 
\newcommand*{\openntuple}{\langle}
\newcommand*{\closentuple}{\rangle}
\newcommand*{\ntuple}[1]{\mbox{\ensuremath{\mathopen{\openntuple}}#1\ensuremath{\mathclose{\closentuple}}}} 
\newcommand*{\define}[1]{\textsc{\lowercase{#1}}}

%    ****************************************
%    *        TITLE AND VERSION DATA        *
%    ****************************************
\newcommand*{\forallx}{\texttt{forall}\script{x}}
\newcommand*{\forallxcam}{\texttt{forall}\script{x}\texttt{:Cambridge}}
	
%    ****************************************
%    *          LIST  ENVIRONMENTS          *
%    ****************************************
% The {earg} environment is used for arguments and example sentences.
% The {ekey} environment is used for symbolization keys.
\newcounter{eargnum}
\newcounter{OLDeargnum}
\newenvironment{earg}%
{\begin{list}{\arabic{eargnum}.}{\usecounter{eargnum}\itemsep=0pt \parsep=0pt}}%
	{\setcounter{OLDeargnum}{\arabic{eargnum}}\end{list}}

\newenvironment{ebullet}% TB: added to give a nice bulleted enivronment
{\begin{list}{\textbullet}{\itemsep=0pt \parsep=0pt}}%
	{\end{list}}

\newcommand{\ekeylabel}[1]{{\makebox[8ex][r]{\ensuremath{ #1}:}}}
\newenvironment{ekey}{\begin{list}{}{\renewcommand{\makelabel}{\ekeylabel} \itemsep=0pt \parsep=0pt}}{\end{list}}

% Used in conjunction with {earg}, this handles the numbering and
% references to example sentences:
\newcounter{Example}[chapter]
\newcommand*{\ex}[1]{\refstepcounter{Example}\arabic{Example}.\label{#1}}
\renewcommand{\labelitemi}{$\triangleright$}

% \factoidbox{...} produces an inset paragraph of text with a line around it
\newcommand{\factoidbox}[1]{\begin{quote}\framebox{\parbox{\linewidth}{#1}}\end{quote}}

%    ****************************************
%    *          PRACTICE PROBLEMS           *
%    ****************************************
\newcounter{ProbPart}
\renewcommand{\theProbPart}{\Alph{ProbPart}}
% This inserts a heading and resets the counter:
\newcommand*{\practiceproblems}{
	\setcounter{ProbPart}{0}\section*{Practice exercises}%
	\addcontentsline{toc}{section}{Practice exercises}
}
% This starts a new section which is automatically numbered:
\newcommand*{\problempart}{\par\noindent\refstepcounter{ProbPart}\textbf{\Alph{ProbPart}. }}

% This is used to enumerate things that have a given property.
% For example: \nextSeq\nextSeq\noSeq\lastSeq are valid.
% produces   : 1, 2, and 4 are valid.
\newcounter{countSeq}
\newcommand*{\nextSeq}{\stepcounter{countSeq}\arabic{countSeq}, }
\newcommand*{\noSeq}{\stepcounter{countSeq}}
\newcommand*{\lastSeq}{and \stepcounter{countSeq}\arabic{countSeq} }

%    ****************************************
%    *         TABLE OF CONTENTS, ETC.      *
%    ****************************************
\renewcommand{\thechapter}{\arabic{chapter}}
\renewcommand{\thesection}{\arabic{chapter}.\arabic{section}}
\setstocksize{297mm}{210mm} %Height and width of stock
\settrimmedsize{297mm}{210mm}{*} %Height and width of trimmed page
\settrims{0mm}{0mm} %Trims top and fore-edge
\settypeblocksize{227mm}{140mm}{*} %Height and width of typeblock
\setlrmargins{*}{*}{1} %Left and right margins are equal
\setulmargins{*}{*}{1} %Top and bottom margins are equal 
\setlength{\parindent}{1em}
\setlength{\parskip}{0em}
\checkandfixthelayout

%    ****************************************
%    *             TRUTH TABLES             *
%    ****************************************
% This facilitates the typesetting of truth tables 
% e.g. to have a two atom truth table with five bits, I use:
%\begin{tabular}{c c | d e e e f}
% d for left-most columns, e for middle ones, f for right-most ones. The ensuing spacing is ok.
\newcolumntype{d}{ c@{\extracolsep{0.1em}}}
\newcolumntype{e}{@{\extracolsep{0.1em}}c@{\extracolsep{0.1em}}}
\newcolumntype{f}{@{\extracolsep{0.1em}}c }
\newcommand*{\TTbf}[1]{\textbf{ #1}}


%    ****************************************
%    *                PROOFS                *
%    ****************************************
% based on fitch.sty by Peter Selinger, University of Ottawa
% v 0.4, (C) 2002 Peter Selinger
% revised 2003--5 by P.D. Magnus
% Selinger released this code under the GNU General Public License,
% version 2 or later. So this bit of the style is free to you under
% the GPL.
% ----------------------------------------------------------------------
% The comments in this file are intended for programmers who
% might want to hack this package. For information on how to use the
% package, the file fitchdoc.tex is a better place to look.
% ----------------------------------------------------------------------

% Global identifiers defined by this package start with '\nd*'. The
% only exceptions are \ndref, \nddim, and the "nd" and "ndresume"
% latex environments.

{\chardef\x=\catcode`\*
	\catcode`\*=11
	\global\let\nd*astcode\x}
\catcode`\*=11

% 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 C) 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

\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{}

%\def\nd*num#1{\global\advance\nd*ctr1\nd*numo{\the\nd*ctr}{#1}}
\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%
	\errmessage{Undefined natdeduction reference: #1}\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\c{\nd*aux{}}%
	\else\ifx#2,\nd*refa{#1}, \def\c{\nd*aux{}}%
	\else\ifx#2;\nd*refa{#1}; \def\c{\nd*aux{}}%
	\else\ifx#2.\nd*refa{#1}. \def\c{\nd*aux{}}%
	\else\ifx#2)\nd*refa{#1})\def\c{\nd*aux{}}%
	\else\ifx#2(\nd*refa{#1}(\def\c{\nd*aux{}}%
	\else\ifx#2\nd*end\nd*refa{#1}\def\c{}%
	\else\def\c{\nd*aux{#1#2}}%
	\fi\fi\fi\fi\fi\fi\fi\c}
\def\ndref#1{\nd*aux{}#1\nd*end}


% 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.

% define various dimensions (explained in fitchdoc.tex):
\newlength{\nd*dim} 
\newdimen\nd*depthdim
\newdimen\nd*hsep
% 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}

\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}}

% 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.

\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%
		{\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}}

% 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 following function 
% 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. 

\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}}

% 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*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.

\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}{r@{\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*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}}}
	% one must first \close the outermost layer of assumption
	% it's a bit of a hack
	
	% 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 the syntax used by the end user. It is implemented as a
	% wrapper around layer B, providing six additional conveniences: 
	% (1) no more need for explicit '\\', (2) all hypotheses 
	% are denoted \hypo, (3) a convenient syntax for writing justification
	% labels, (4) a latex environment, (5) guard as optional argument to
	% \have, \hypo, or \open, (6) optional relabeling arguments. The user
	% level commands are similar to those of layer B: they are called
	% \begin{nd}, \end{nd}, \open, \close, \hypo, \have. In addition there
	% is a \by command for writing justification labels, in the style of
	% \by{$\vee$E}{1,2-4,5-6}. For convenience, a number of abbreviations
	% is also provided, 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 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. Finally, \nd*init puts all the commands which are visible
	% inside an nd-environment in the current name space.
	
	\def\nd*clr{\gdef\nd*cmd{}}
	\def\nd*sto#1#2#3{\gdef\nd*typ{#1}\gdef\nd*byt{}%
		\gdef\nd*cmd{\nd*typ{#2}{#3}\nd*byt\\}}
	\def\nd*hyc#1#2{\def\nd*typ{\nd*haveb}\nd*cmd\nd*sto{\nd*hypob}{#1}{#2}}
	\def\nd*hac#1#2{\nd*cmd\nd*sto{\nd*haveb}{#1}{#2}}
	%\def\nd*htc#1#2{\nd*cmd\nd*sto{\nd*theob}{#1}{#2}}
	
	% usage: \optarg{default}{continuation}xxx - reads an optional argument, 
	% supplies default if necessary, then continues with continuation. 
	% Continuation expects optional argument between [...]. I.e., 
	% \optarg{d}{c}[xxx] => c[xxx], and \optarg{d}{c}x => c[d]x if x != '['. 
	% Behavior is undefined if x is {[...}. \optargg is similar except it 
	% takes two continuations: first one for optional argument present, second 
	% for not present. It takes no default value.
	
	\def\optarg#1#2#3{\ifx[#3\def\c{#2#3}\else\def\c{#2[#1]{#3}}\fi\c}
	\def\optargg#1#2#3{\ifx[#3\def\c{#1#3}\else\def\c{#2{#3}}\fi\c}
	
	\def\nd*hyx[#1][#2]#3[#4]#5{\ifx\relax#4\relax\else\nd*guardb{1}{#4}\fi\nd*hyc{#3}{#5}\nd*set{#1}{#2}}
	\def\nd*hax[#1][#2]#3[#4]#5{\ifx\relax#4\relax\else\nd*guardb{1}{#4}\fi\nd*hac{#3}{#5}\nd*set{#1}{#2}}
	%\def\nd*htx[#1][#2]#3[#4]#5{\ifx\relax#4\relax\else\nd*guardb{1}{#4}\fi\nd*htc{#3}{#5}\nd*set{#1}{#2}}
	
	% \nd*five{\a}: read five, partly optional arguments of the shape [][]{}[]{}, 
	% then call \a with these arguments.
	\def\nd*five#1{\optargg{\nd*four{#1}}{\nd*two{#1}}}
	\def\nd*four#1[#2]{\optarg{0}{\nd*three{#1}[#2]}}
	\def\nd*three#1[#2][#3]#4{\optarg{}{#1[#2][#3]{#4}}}
	\def\nd*two#1{\nd*three{#1}[\relax][]}
	
	\def\nd*have{\nd*five{\nd*hax}}
	\def\nd*theo{\nd*five{\nd*htx}} % To be like have
	\def\nd*hypo{\nd*five{\nd*hyx}}
	\def\nd*base{undefined}
	
	\def\nd*open{\optargg{\nd*openopt}{\nd*opennoopt}}
	\def\nd*openopt[#1]{\nd*cmd\nd*clr\nd*openb\nd*guard{#1}}
	\def\nd*opennoopt#1{\nd*cmd\nd*clr\nd*openb#1}
	\def\nd*close{\nd*cmd\nd*clr\nd*closeb}
	\def\nd*guard{\optarg{1}{\nd*guardc}}
	\def\nd*guardc[#1]#2{\nd*guardb{#1}{#2}}
	
	\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}
	
	% * * *
	% This block defines the natural deduction rules.
	% Rules designated by ordinary letters may be specified with \by{RULE}
	% * * *
	
	\def\nd*init{%
		\let\open\nd*open%
		\let\close\nd*close%
		\let\hypo\nd*hypo%
		\let\have\nd*have%
		%  \let\theo\nd*theo%
		\let\by\nd*by%
		\let\guard\nd*guard%
		\def\bi{\by{{\eiff}I}}%
		\def\be{\by{{\eiff}E}}%
		\def\ci{\by{{\eif}I}}%
		\def\ce{\by{{\eif}E}}%
		\def\Ai{\by{$\forall$I}}%
		\def\Ae{\by{$\forall$E}}%
		\def\Ei{\by{$\exists$I}}%
		\def\Ee{\by{$\exists$E}}%
		\def\ae{\by{{\eand}E}}%
		\def\ai{\by{{\eand}I}}%
		\def\oi{\by{{\eor}I}}%
		\def\oe{\by{{\eor}E}}%
		\def\ni{\by{{\enot}I}}%
%			\def\ne{\by{{\enot}E}}%
		\def\ri{\by{{\enot}E}}% TB: reductio introduction
		\def\re{\by{X}}% TB: reductio elimination
		\def\ii{\by{$=$I}}%
		\def\ie{\by{$=$E}}%
		\def\tnd{\by{TND}}% TB: tertium non datur
		\def\dne{\by{DNE}}% TB: double negation elimination (derived rule)
		\def\mt{\by{MT}}% TB: modus tollens (derived rule)
		\def\ds{\by{DS}}% TB: disjunctive syllogism (a derived rule in Cambridge version)
		\def\dem{\by{DeM}}% TB: De Morgan rule (derived rule)
		\def\cq{\by{CQ}}% TB: conversion of quantifiers (derived rule)
	}
	\newenvironment{nd}{\begingroup\nd*init\nd*beginb\nd*clr}{\nd*cmd\nd*endb\endgroup}
	\newenvironment{ndresume}{\begingroup\nd*init\nd*resumeb\nd*clr}%
	{\nd*cmd\nd*endb\endgroup}
	
	% Example of a derivation using layer C 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 C syntax, using guards and relabelings:
	
	% \begin{nd}
	%   \hypo          {1} {P\vee Q}
	%   \open
	%   \hypo          {2}[u] {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}
	
	\catcode`\*=\nd*astcode
	
	% a command for indicating the goal in a proof or subproof
	\newcommand*{\want}[1]{\by{want \ensuremath{#1}}{}}
	% an environment that separates the proof from surrounding paragraphs
	\newenvironment{proof}
	{\begin{list}{}{}\item$\begin{nd}}
		{\end{nd}$\end{list}}
	
	% I keep mixing up the \ce and \ae commands, so I define a less ambiguous
	% alternate set of commands
	
	\newcommand*{\notI}{\ni}
	\newcommand*{\notE}{\ne}
	\newcommand*{\iffI}{\bi}
	\newcommand*{\iffE}{\be}
	\newcommand*{\ifI}{\ci}
	\newcommand*{\ifE}{\ce}
	\newcommand*{\andI}{\ai}
	\newcommand*{\andE}{\ae}
	\newcommand*{\orI}{\oi}
	\newcommand*{\orE}{\oe}
	\newcommand*{\forallI}{\Ai}
	\newcommand*{\forallE}{\Ae}
	\newcommand*{\existsI}{\Ei}
	\newcommand*{\existsE}{\Ee}
	
	%    ****************************************
	%    *            STYLE OF THE BOOK           *
	%    ****************************************
	% From the point of view of LaTeX, the book consists of 9 parts, containing roughly 5 chapters each. From the point of view of the user, the book consists of 9 chapters, containing roughly 5 sections each. This means a fair bit of internal redefinition of LaTeX code.
	
	\makeatletter
	\renewcommand{\@chapapp}{ } % to prevent "chapter" appearing all over the place
	\makeatother
	\renewcommand\cftchapterfont{\normalfont} % to make the sections (which LaTeX regards as chapters) small in the ToC
	\renewcommand\cftchapterpagefont{\normalfont} % to make the sections (which LaTeX regards as chapters) small in the ToC
	\renewcommand\cftbeforechapterskip{0pt} % to leave no gap between sections (which LaTeX regards as chapters) in the TOC
	\renewcommand{\partname}{} % to make the chapters (which LaTeX regards as parts) labelled "chapter"
	\setlength{\headwidth}{\textwidth} 
	
	\makepagestyle{forallxpage} %TB: design new page style
	\makeheadrule {forallxpage}{\textwidth}{\normalrulethickness} % put rule beneath page header
	\makeevenhead {forallxpage}{\small \thepage}{}{\small\leftmark}  % page header consists of section name and page
	\makeoddhead {forallxpage}{\small\rightmark}{}{\small \thepage} 
	\makeatletter
	\makepsmarks{forallxpage}{
		\nouppercaseheads
		\createmark {chapter} {both} {shownumber}{}{.\ }
	}
	\makeatother
	
	\setcounter{tocdepth}{0} % only chapters and sections to appear
	\renewcommand{\thepart}{\arabic{part}}  % chapters (which LaTeX regards as parts) to be numbered
	\renewcommand{\thechapter}{\arabic{chapter}} % sections (which LaTeX regards as chapters) to be numbered
	\renewcommand{\thesection}{\arabic{chapter}.\arabic{section}} % subsections (which LaTeX regards as sections) to be n.m
	
	\makechapterstyle{forallx}{% defines a nice style for section headings (which LaTeX regards as chapter headings)
		\renewcommand{\chapnamefont}{\normalfont\Huge\bfseries} 
		\renewcommand{\chapnumfont}{\normalfont\Huge\bfseries}
		\renewcommand{\chaptitlefont}{\normalfont\Huge\bfseries} 
		\renewcommand{\afterchapternum}{}
		\renewcommand{\printchaptername}{} 
		\setlength{\midchapskip}{0mm} 
		\renewcommand{\chapternamenum}{} 
		\renewcommand{\printchapternum}{%
			\noindent\marginpar{\chapnumfont\thechapter}}
		\renewcommand{\printchaptertitle}[1]{\chaptitlefont ##1}
	}
	\chapterstyle{forallx}
	
	\setlength{\columnsep}{2em} % Sets 2em space between columns when calling multicol 
	
	\definecolor{darkred}{rgb}{0.5,0,0} % TB: used to color links in red
	\definecolor{darkblue}{rgb}{0,0,0.5} % TB: used to color answers in blue
	\newcommand\myanswer[1]{\textcolor{blue}{#1}} % TB: puts model answers in blue
	\hypersetup{pdfinfo={Title={forallx: Cambridge}, Author={P.D. Magnus, Tim Button}, Subject={An open access introductory textbook in formal logic}, Keywords={truth-functional logic, propositional logic, predicate logic, sentential logic, first-order logic, quantified-logic, natural deduction, fitch}}, %
		colorlinks={true}, %
		linkcolor={darkred},
		pdfdisplaydoctitle={true}}
	
	%    ****************************************
	%    *            DIAGRAMS IN TIKZ           *
	%    ****************************************
	% I use diagrams in a few places, always using Tikz.
	% All these drawings are done using tikz
	\usepackage{tikz}
	\usetikzlibrary{arrows,positioning,shapes} 
	
	\tikzset{phantom_shape/.style={thick, fill=black!0, minimum width=30pt, minimum height=30pt}, % TB: renders the shape invisible
		grey_shape/.style={thick, fill=black!20, draw, minimum width=30pt, minimum height=30pt}, % TB: renders a light grey shape with a black outline
		white_shape/.style={thick, fill=black!0, draw, minimum width=30pt, minimum height=30pt} % TB: renders a white shape with a black outline
	}