forallxyyc.sty

%!TEX root = forallxyyc.tex
\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{forallxyyc}[2023/09/01 support for a logic textbook]

% The current book version
\def\forallxversion{Fall 2023}
\def\forallxshortversion{F23}

\RequirePackage{amssymb,amsmath,pifont,rotating}
\usepackage[cal=boondoxo]{mathalfa}
\usepackage[german,english]{babel}
\usepackage[utf8]{inputenc}
\usepackage{latexml}
\RequirePackage{hyperref,ifthen,graphicx,xcolor}
\RequirePackage{enumitem}

% References using cleveref

\RequirePackage[nameinlink]{cleveref}
\crefname{enumi}{sentence}{sentences}

% \ifHTMLtarget -- for conditional code depending on whether we're
% compiling to HTML or to PDF. To be used for anything that would also
% compile to PDF for testing and because BookML runs the file through
% LaTeX. Use \iflatexml to test for when we're *actually* running
% through LaTeXML (e.g., inserting raw HTML)
\newif\ifHTMLtarget
\HTMLtargetfalse

% The original forallx.sty was written in 2005
% Comments marked "TB" are additions by Tim Button in September 2012

%    ****************************************
%    *        TITLE AND VERSION DATA        *
%    ****************************************
% the title of the book

\newcommand*{\forallx}{\texttt{forall}\textit{x}}
\newcommand*{\forallxyyc}{\texttt{forall}\textit{x}\texttt{:Calgary}}

%    ****************************************
%    *            LOGICAL SYMBOLS           *
%    ****************************************
%
% There are, of course, many different symbols used for the truth-functional
% connectives. In order to make the book adaptable, the symbols are defined
% here in the style sheet and these commands are used throughout the book.
% To change conjunction from the ampersand to the carat, for instance,
% change the definition of \eand from ~\&~ to \wedge. To change negation from
% the hoe to the swung dash, change \enot from \neg to {\sim}. Other examples
% are given below.
%
\let\oldtherefore\therefore
\def\therefore{\ensuremath{\oldtherefore}}
\iflatexml
\def\texttherefore{∴}
\else
\let\texttherefore\therefore
\fi
% disjunction
\def\eor{\ensuremath{\vee}}
% conjunction: 
% {\,^{_{_{_{_{\mbox{\footnotesize\textbullet}}}}}}} gives the dot
\def\eand{\ensuremath{\wedge}}
% conditional: \supset gives the horseshoe
\def\eif{\ensuremath{\rightarrow}}
% biconditional: \equiv gives the triple bar
\def\eiff{\ensuremath{\leftrightarrow}}
% negation: {\sim} gives the swung dash 
\def\enot{\ensuremath{\neg}}
\def\ered{\ensuremath{\bot}}% TB: added to give an absurdity sign
\newcommand*{\ebox}{\ensuremath{\Box}}
\def\ediamond{\ensuremath{\Diamond}}
\iflatexml
\def\maththe{\ensuremath{\iota}}
\else
\def\maththe{\rotatebox[origin=c]{180}{$\iota$}} % TB: added to give definite description operator
\fi
\def\proves{\ensuremath{\vdash}}
\def\entails{\ensuremath{\vDash}}
\def\nproves{\ensuremath{\nvdash}}
\def\nentails{\ensuremath{\nvDash}}

% modal logic systems
\def\mlK{\ensuremath{\mathbf{K}}}
\def\mlT{\ensuremath{\mathbf{T}}}
\def\mlSfour{\ensuremath{\mathbf{S4}}}
\def\mlSfive{\ensuremath{\mathbf{S5}}}

% args -- format a list of arguments separated by commas without commas

\newcommand*{\args}[1]{%
  \let\@argsep\@argsepinit
  \@for\@arg:=#1\do{%
    \@argsep\@arg}%
}

\def\@argsepinit{\let\@argsep\argsep}

\newcommand{\argsep}{}

\newcommand{\atom}[2]{\ensuremath{\lxFcn{#1}(#2)}}

%    ****************************************
%    *       SYMBOLS AND SCRIPTY BITS       *
%    ****************************************
% equivalent to commenting something out, but usable on multiple lines
\providecommand{\nix}[1]{}

\newcommand*{\script}[1]{\ensuremath{\mathcal{#1}}}
\newcommand*{\metav}[1]{\ensuremath{\mathcal{#1}}}

% create a blank that SRs read out as "blank"
\iflatexml
\newcommand*{\blank}{\underline{blank~}\bmlPlusClass{fxblank}}
\else
\newcommand*{\blank}{\underline{\hspace*{2.5em}}}
\fi
\newcommand*{\gap}[1]{\blank$_{#1}$} % TB: used for keys, to avoid use/mention confusion

% make SRs read out "iff" as "if-f" by putting in invisible U+2060
% https://en.wikipedia.org/wiki/Word_joiner
\iflatexml
\newcommand*{\ifeff}{if⁠f}
\else
\newcommand*{\ifeff}{iff}
\fi

% These are included for discussing formal semantics in predicate logic.
\newcommand*{\model}[1]{\ensuremath{\mathbb{#1}}}
\newcommand*{\extension}[1]{\ensuremath{\mbox{extension}(#1)}}
\newcommand*{\referent}[1]{\ensuremath{\mbox{referent}(#1)}}
  % I personally dislike the default LaTeX angle brackets. I think that
  % they are too narrow. If you want to use them, though, you can
  % replace < and > in the commands below with \langle and \rangle
\newcommand*{\openntuple}{\langle}
\newcommand*{\closentuple}{\rangle}
\newcommand*{\ntuple}[1]{\ensuremath{\mathopen{\openntuple}}#1\ensuremath{\mathclose{\closentuple}}} 
% definitions
\newcommand*{\define}[1]{\textsc{\lowercase{\color{dkleadbeater}#1}}}

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

\newlist{factoiditems}{itemize}{1}

\iflatexml
\setlist[itemize]{label=‣,noitemsep}
\setlist[factoiditems]{label=‣}
\else
\setlist[itemize]{label=$\triangleright$,noitemsep}
\setlist[factoiditems]{label=$\triangleright$,labelindent=0pt,leftmargin=*}
\fi

% earg -- an unordered list for arguments, no labels
%\newenvironment{earg}{\begin{itemize}[noitemsep,label={},align=right]}{\end{itemize}}
\newlist{earg}{itemize}{1}
\setlist[earg]{noitemsep,label={},align=right}

% ebullet - a bulleted list
\newenvironment{ebullet}% TB: added to give a nice bulleted enivronment
{\begin{itemize}[noitemsep,label=\textbullet]}{\end{itemize}}

% ekey - for symbolization keys. TODO: turn this into a description
% list for better A11Y
% \newcommand{\ekeylabel}[1]{{\makebox[8ex][r]{\ensuremath{ #1}:}}}
% \newenvironment{ekey}{\begin{list}{}{\renewcommand{\makelabel}{\ekeylabel}
% \itemsep=0pt \parsep=0pt}}{\end{list}}
\newlist{ekeylist}{description}{1}
\setlist[ekeylist]{noitemsep,labelwidth=4em,align=right,font=\normalfont}
\def\ekeylabel#1{\hfil\normalfont\ensuremath{#1}:}
\newenvironment{ekey}{\begin{ekeylist}\renewcommand{\makelabel}{\ekeylabel}}{\end{ekeylist}}

% compactlist -- a numbered list with tight spacing
\newlist{compactlist}{enumerate}{1}
\setlist[compactlist]{noitemsep,label=\arabic*.}
% numberlist -- a numbered list with standard spacing
\newlist{numberlist}{enumerate}{1}
\setlist[numberlist]{label=\arabic*.}

% enumerate -- used for numbered examples; counter resets every
% chapter
\setlist[enumerate]{resume,noitemsep,labelwidth=4em}
\@addtoreset{enumi}{chapter}

%    ****************************************
%    *             TRUTH TABLES             *
%    ****************************************

% This facilitates the typesetting of truth tables by
% effectively eliminating the intercolumn space.
% This allows truth tables with the Ts and Fs immediately
% below arbitrary connectives.
% An example follows:
%\begin{center}
%\begin{tabular}{c|c|@{\TTon}*{5}{c}@{\TToff}}
%$A$&$B$&$(A$&\eand&$B)$&\eif&A\\
%\hline
% T & T &    &  T  &    &  T & \\
% T & F &    &  F  &    &  T & \\
% F & T &    &  F  &    &  T & \\
% F & F &    &  T  &    &  T &
%\end{tabular}
%\end{center}
%\newcommand*{\TTon}{\hspace{1.5em}\extracolsep{-1em}}
%\newcommand*{\TToff}{\extracolsep{-1em}\hspace{.3em}}

\RequirePackage{multicol,array}

% Moving to Memoir breaks Magnus's elegant macro
% In the preceding column definition, I would offer instead:
%\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                *
%    ****************************************

\usepackage[arrayenv=tabular]{fitch}

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

\newcommand*{\PR}{\by{PR}{}}
\newcommand*{\AS}{\by{AS}{}}

% a command for indicating the goal in a proof or subproof
\newcommand*{\want}[1]{\by{want \ensuremath{#1}}{}}

\def\ndrules{
  \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}}% RZ: this is now \enot E
  \def\re{\by{X}}% RZ: this is now X (explosion)
  \def\ii{\by{$=$I}}%
  \def\ie{\by{$=$E}}%
  \def\tnd{\by{LEM}}% RZ: Law of excluded middle
  \def\ip{\by{IP}}% RZ: indirect proof
  \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)
  \def\boxi{\by{{\ebox}I}}%
  \def\boxe{\by{{\ebox}E}}%
  \def\mc{\by{MC}}%
  \def\diadf{\by{Def{\ediamond}}}%
  \def\rt{\by{R$\mathbf{T}$}}%
  \def\rfour{\by{R$\mathbf{4}$}}%
  \def\rfive{\by{R$\mathbf{5}$}}%
  \def\ellipsesline{\have[ ]{}{\vdots}}%
}
\def\by#1#2{#1} % allow \by outside proofs

\setkeys{fitch}{
  height=4.5ex,
  topheight=3.5ex,
  depth=1.5ex,
  labelsep=.7em,
  indent=1em,
  hsep=.5em,
  justsep=1.5em,
  linethickness=.2mm,
  arrayenv=tabular
}

%    ****************************************
%    *            DIAGRAMS IN TIKZ           *
%    ****************************************
% TB: I use diagrams in a few places, always using Tikz.
%   A. To illustrate an argument for the truth table of the material conditional
%   B. To draw graphs illustrating small finite interpretations. 
% All these drawings are done using tikz
\usepackage{tikz}
\usetikzlibrary{arrows,positioning,shapes} 

\tikzset{phantom_shape/.style={thick, fill=none, 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=none, draw, minimum width=30pt, minimum height=30pt} % TB: renders a white shape with a black outline
		}

%    ****************************************
%    *          PRACTICE PROBLEMS           *
%    ****************************************
\newcounter{ProbPart}
\renewcommand{\theProbPart}{\Alph{ProbPart}}
\renewcommand{\theHProbPart}{\thechapter.\theProbPart}
% This inserts a heading and resets the counter:
\newcommand*{\practiceproblems}{
	\setcounter{ProbPart}{0}\section*{Practice exercises}%
  \sectionmark{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 bullet is used to indicate that solutions appear at the end of
% the book.
\newcommand*{\solutions}{} %TB: removed, since I am not including the solutions in the book
% When solutions are only given for selected problems, the
% star is placed left of the problem number.
\newcommand*{\leftsolutions}{\hspace{-2.2em}\makebox[2em][l]{\solutions}}

% This is used at the beginning of a section in the solutions
% appendix.
\newcommand*{\solutionsection}[2]{%
	\textbf{\textsc{Chapter {\ref{#1}} Part {\ref{#2}}}}%
	\markright{solutions for ch.~\ref{#1}}%
	\setcounter{countSeq}{0}
}

% 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{\thepart}{\Roman{part}}
\renewcommand{\thesection}{\thechapter.\arabic{section}}

\setcounter{tocdepth}{0} %TB: only chapters and sections to appear

\setlength{\columnsep}{2em} % Sets 2em space between columns when calling multicol 

\newcommand\myanswer[1]{\textcolor{dkleadbeater}{#1}} % TB: puts model answers in blue

% aria-label environment to provide accessible descriptions for inline
% SVG diagrams
\iflatexml
  \newenvironment{arialabel}[1]{\<span class="test">\<div aria-hidden="true" class="ltx\_centering">}{\</div>\</span>}
\else
  \newenvironment{arialabel}[1]{}{}
\fi

\IfFileExists{forallxyyc-local.sty}{\usepackage{forallxyyc-local}}{}