\documentclass{article}
\usepackage{setspace}
\usepackage{amssymb}
\usepackage[margin=1.45in]{geometry}
\usepackage{microtype}
\usepackage{fancyvrb}
\usepackage{bussproofs}
\usepackage[oxford]{logictools}
\usepackage[svgnames]{xcolor}
\usepackage{tabularx}
\usepackage{nicematrix,tikz}
\usetikzlibrary{patterns.meta, patterns, decorations.markings,fadings}
\tikzset{->-/.style={decoration={
  markings,
  mark=at position #1 with {\arrow[line width=1.25pt]{>}}},postaction={decorate}}}
%-----------------------------------------------------
\title{The logictools Package}
\author{Miles Min Yin Cheang}
%-----------------------------------------------------

%\usepackage[bitstream-charter,expert]{mathdesign}
\usepackage{XCharter}
\SetMathAlphabet{\mathcal}{normal}{OMS}{cmsy}{m}{n}

\usepackage{hyperref}
\hypersetup{
    colorlinks,
    citecolor=black,
    filecolor=black,
    linkcolor=black,
    urlcolor=black
}

% Super easy proof annotations in the style that Volker likes, with good(ish) kerning.
\newcommand{\andlabel}[1]{
\RightLabel{\scriptsize($\land$\hspace{1px}#1)}
}

\newcommand{\orlabel}[1]{
\RightLabel{\scriptsize($\lor\hspace{1px}\text{#1}$)}
}

\newcommand{\implieslabel}[1]{
\RightLabel{\scriptsize($\rightarrow$\hspace{0.5px}#1)}
}

\newcommand{\ifflabel}[1]{
\RightLabel{\scriptsize($\leftrightarrow$\hspace{0.5px}#1)}
}

\newcommand{\neglabel}[1]{
\RightLabel{\scriptsize($\neg$\hspace{0.5px}#1)}
}

\newcommand{\foralllabel}[1]{
\RightLabel{\scriptsize($\forall$\hspace{1px}#1)}
}

\newcommand{\existslabel}[1]{
\RightLabel{\scriptsize($\exists$\hspace{0.5px}#1)}
}

\makeatletter
\def\shorteq{\@ltoolsshorteq}
\makeatother

\fboxsep=0pt \fboxrule=1sp

\begin{document}

\maketitle
\setstretch{1.4}
\tableofcontents
\newpage

\section{Purpose of this package}
The star of the show here is the formallogic environment. Prior to the development of this environment, spending way too much time fiddling around with spacing commands was a familiar experience for every logician. Most of the spacing you need in a logical statement is context sensitive, so only so much can be done through basic macros. Furthermore, using too many macros destroys the readability of the code, and slows down writing to a crawl.

In an effort to change this, I wrote an environment that both \emph{speeds up} writing formal logic (by offering shorter syntax) and improves the output considerably. The details of how this works will be presented in the upcoming sections. The default settings were made with \LaTeX's default math font in mind, with the intention that the user come up with a preset that matches their preferences. The options can be changed on the fly, so more than one preset can be used in different parts of the document.

Other than this, the option `oxford' will load a few neat macros that might be of particular interest to those studying logic at the University of Oxford; they provide shortcuts to notations that are commonly used in the first-year courses. It is likely that this section of the package will be updated with more content as I go through my degree.
\newpage
\section{The formallogic environment}
\subsection{Introduction}

This interface, accessed through the environment named \verb|formallogic|, or the command \verb|\fmllgc{<content>}|, helps to type formal logic in \LaTeX. Here are some of its uses:
\logictoolsoptions{partype=single,italiccorrection=1mu, quantskip=5mu,lastquantskip=5mu}
\begin{center}
\begin{tabular}{c|c}
   Code:  & Output: \\ \hline
   \verb!|forall, x ; exists, y| (Ryx)!  & \fmllgc{|forall,x;exists,y| (Ryx)} \\
   \verb!|f,x;e,y|(Ryx)!  & \fmllgc{|forall,x;exists,y| (Ryx)} \\
    \verb|((P \land Q) \liff R)|& \logictoolsoptions{partype=double,italiccorrection=1mu, quantskip=5mu,lastquantskip=5mu,parinnerpad=5mu,parvoffset=0.17ex} \fmllgc{((P \land Q) \liff R))}\\
    \verb|((P \land Q) \liff R)|& \logictoolsoptions{partype=single,italiccorrection=1mu, quantskip=5mu,lastquantskip=5mu,parinnerpad=1mu,parstackkern=-3mu, parvoffset=0.17ex} \fmllgc{((P \land Q) \liff R))}\\
    \verb|((P \land Q) \liff R)|& \logictoolsoptions{partype=single,italiccorrection=1mu, quantskip=5mu,lastquantskip=5mu,parinnerpad=2.5mu,parstackkern=5mu, parvoffset=0.17ex} \fmllgc{((P \land Q) \liff R))}
\end{tabular} 
\end{center}


You will be shown how to accomplish every one of these in the following documentation. Note that there are various user-defined parameters controlling the typesetting (e.g. spacing, kerning, parenthesis style); this is how the same code can produce wildly different outputs. Furthermore, the user can control certain parts of the syntax (e.g. the names of quantifiers).
\subsection{Quantifier stacks}
Quantifier stacks are a concept introduced for typesetting logical quantifiers:

\begin{center}
    \fmllgc{|forall , x ;exists , y ;forall, x_1 ;exists, z\in \mathbb{R}|}

    \verb!| forall, x ; exists, y ; forall, x_1 ; exists, z\in\mathbb{R} |!
\end{center}

Quantifier stacks are used by the formallogic environment. They are delimited by `\texttt{|}'. A quantifier stack is made up of quantifiers, written in the form \verb|<label>,<argument>|. The label consists of some text that indicates which quantifier will be used, while the argument can be any math mode code. These quantifiers are separated by `;'. The formallogic environment processes these stacks, turning them into a fully typeset sequence of quantifiers. 

Spacing on either side of the label and argument is trimmed, but spacing inside the label is not. This means `for all' is a distinct label from `forall'.
\newpage
\subsubsection{Declaring quantifiers}

A declared quantifier has the following form:
\begin{center}
\input{tikz/quantdiagram}
\end{center}

\noindent \textbf{Syntax for quantifier declaration:}
\begin{center}\verb|\DeclareQuantifier{<label>}{<command>}[<left pad>][<right pad>]|\end{center}

\vskip-1.5ex This command will globally declare (or redeclare) a quantifier with the associated properties. The label consists of some text that refers to this quantifier; the command should be a LaTeX command providing the quantifier symbol; left and right padding are optional padding values on either side of the command. For instance: \verb|\DeclareQuantifier{ex!}{\exists !}[5mu][1.5mu]| provides a quantifier that can be used like: \verb'|ex!,x;forall,y|' $\to$ \DeclareQuantifier{ex!}{\exists !}[5mu][1.5mu]\fmllgc{|ex!,x;forall,y|}.

\begin{center}\verb|\LDeclareQuantifier{<label>}{<command>}[<left pad>][<right pad>]|\end{center} 

\vskip-1.5ex This command does the same thing, but locally. With this, one can quickly redefine a quantifier in the middle of the environment, and not worry about the changes carrying over to other instances of the environment.
\subsection{Other syntax}
\begin{itemize}
    \item Parentheses written consecutively (without spaces) will become parenthesis stacks, and use \texttt{parstackkern} instead of \texttt{parinnerpad} as spacing.
    \item \texttt{[<arg 1>/<arg 2>]} $\to\,[\nicefrac{\texttt{<1>}}{\texttt{<2>}}]$, allowing one to write easy variable substitutions inline\footnote{Note that this means `\texttt{[}' is by default active in the syntax, and so requires escaping if one wishes to use it without following it with `\texttt{/}' and then `\texttt{]}'.}.
    \item \texttt{.=} $\to\,\doteq$, providing quick access to \verb|\doteq|.
\end{itemize}

One can use \texttt{"<content>"} within the environment to escape \texttt{<content>}, preventing it from being parsed by the environment; this is useful when one wishes to use a character that is active in the syntax of the environment. The delimiter used here is the double quote, \texttt{"} (U+0022). 

For example, this can be used to write a function with single parentheses in a double parenthesis environment, or a list using commas inside of a quantifier stack\footnote{Actually, `\texttt{,}' and `\texttt{;}' only need escaping when inside of a quantifier stack, delimited by `\texttt{|}'.}:
\begin{Verbatim}[numbers=left,xleftmargin=5mm]
\logictoolsoptions{partype=double, parinnerpad=3.5mu}
\begin{formallogic}
|forall,"x_1,x_2,x_3,\ldots";exists,y|(f"(y)"=x_1+x_2+x_3+\ldots\land Py)
\end{formallogic}
\end{Verbatim}
Produces: \hspace{4.25em}
\logictoolsoptions{partype=double, parinnerpad=3.5mu}
 \begin{formallogic}
    |forall,"x_1,x_2,x_3,\ldots"; exists,y|
    ( f"(y)" = x_1+x_2+x_3+\ldots \land Py)
    \end{formallogic} \hfill

\vspace{1.5ex}

The only syntax that is not escaped like this is \texttt{.=} $\to \,\doteq$, since checks for escaping slightly lower performance, and this can already be escaped with a space between the two characters.

\subsection{Typesetting features}
\subsubsection{Customisation}
The formallogic environment offers many customisation options through user-adjustable keys. They may be changed with the command \verb|\logictoolsoptions{<key>=<value>, ... }| (in either the document or the preamble). A list of key-value pairs may also be given in an optional argument to the formallogic environment. The following keys are available:
\newcolumntype{Y}{>{\hsize=.5\hsize\linewidth=\hsize}X}
\setlength{\tabcolsep}{6pt} % Default value: 6pt
\renewcommand{\arraystretch}{1.5} % Default value: 1
\begin{center}
\begin{tabularx}{\textwidth}{r|>{\hsize=1.65\hsize\linewidth=\hsize}X
|>{\hsize=0.35\hsize\linewidth=\hsize}X|l|}
   Key  & Description & Accepts & Default \\ \hline
   \texttt{partype} & \raggedright Determines the type of parenthesis used, single `$($ ... $)$' or double `$\llparenthesis$ ... $\rrparenthesis$'. & \texttt{single,} \texttt{double} & \texttt{single} \\
   \texttt{parinnerpad} & \raggedright Extra space inserted between parentheses and their content. & mu & \texttt{0.9mu} \\
   \texttt{parstackkern} & \raggedright Kern applied to stacked parentheses. & mu & \texttt{-0.9mu} \\
   \texttt{italiccorrection} & \raggedright Extra kern between closing parentheses and their content, to offset italic math font. & mu & \texttt{1.12mu} \\
   \texttt{parvoffset} & \raggedright Amount to raise parentheses by; helps center them on text in some fonts. & ex & \texttt{0.2ex} \\
   \texttt{quantskip} & \raggedright Default skip inserted between quantifiers. & mu & \texttt{4.32mu} \\
   \texttt{lastquantskip} & \raggedright Default skip inserted after last quantifier. & mu & \texttt{4.32mu} \\
   \texttt{scriptspace} & \raggedright Determines space after sub/superscript, same as the \LaTeX\ primitive. & em & \texttt{-0.025em} \\
\end{tabularx} 
\end{center}

\newpage
\section{The `oxford' package option}\fboxsep=3pt
This package option adds a few macros for common notations at University of Oxford.

\subsection{Good looking `proof from $\varphi$ to $\psi$'}
`A proof $\pi$ from $\varphi$ to $\psi$' (perhaps with some discharged assumptions) might be notated like this:

\begin{center}
\begin{minipage}[t]{0.65\linewidth}
\catcode`?=\active
\def?{\footnotemark}
\begin{Verbatim}[numbers=left,xleftmargin=5mm]
\begin{prooftree}
    \alwaysNoLine
    \AxiomC{\fbox{$\pi$}}
    \UnaryInfC{$\vdots$}
    \UnaryInfC{$\psi$}
    \AxiomC{\fbox{$\pi$}$^{[\varphi]}$}
    \UnaryInfC{$\vdots$}
    \UnaryInfC{$\phi$}
    \alwaysSingleLine
    \andlabel{Intro}?
    \BinaryInfC{$\psi \land \phi$}
\end{prooftree}
\end{Verbatim}
\end{minipage}
\begin{minipage}[t]{0.25\linewidth}
\begin{prooftree}
    \alwaysNoLine
    \AxiomC{\fbox{$\pi$}}
    \UnaryInfC{$\vdots$}
    \UnaryInfC{$\psi$}
    \AxiomC{\fbox{$\pi$}$^{[\varphi]}$}
    \UnaryInfC{$\vdots$}
    \UnaryInfC{$\phi$}
    \alwaysSingleLine
    \andlabel{Intro}
    \BinaryInfC{$\psi \land \phi$}
\end{prooftree}
\end{minipage}
\end{center}
\vspace{1ex}
\VerbatimFootnotes
\footnotetext{The macro \verb|\andlabel{#1}| gives \verb|\RightLabel{\scriptsize($\land$\hspace{1px}#1)}|. }
The output is not ideal; introducing discharged assumptions puts the box off center in an annoying way, and the \verb|\vdots| are not aligned correctly. The following command achieves better output with nicer syntax:
\begin{center} \verb|\prooffrom{<1>}|$\underbracket[1pt][1pt]{\mskip20mu}_{\mathclap{\texttt{<2>}}}$\verb|{<3>}| \end{center}
\noindent \texttt{<2>} \hspace{0.2em}=\begin{minipage}[t]{0.9\linewidth}
    \begin{center}\adjustbox{fbox}{Either `\textasciicircum' (for superscript), `\verb|_|' (for subscript), or nothing (for centered script).}

\vspace{0.5ex}
    
    +

\vspace{1ex}
    
    \adjustbox{fbox,minipage=0.9\linewidth}{Some \texttt{content} delimited by \texttt{[${}\cdots{}$]} (for square-bracketed content) or \texttt{<${}\cdots{}$>}\\ \mbox{} \hfill (for non-square-bracketed content). \hfill \mbox{}}\end{center}
\end{minipage}

\vspace{2ex}

\noindent So \verb|\prooffrom{$\pi$}{$\psi$}|, \verb|\prooffrom{$\pi_1$}^[$\varphi$]{$\phi$}| become: 
\begin{prooftree}
    \prooffrom{$\pi$}{$\psi$}
    \prooffrom{$\pi_1$}^[$\varphi$]{$\phi$}
    \andlabel{Intro}
    \LeftLabel{\hphantom{\scriptsize($\lor\hspace{1px}\text{Intro}$)}}
    \BinaryInfC{$\psi \land \phi$}
\end{prooftree}

\subsection{Bits and Bobs}

\begin{center} \verb|\difmost{<variable>}|{\color{DarkBlue}\llap{\text{[Math mode only.]\hspace{14em}}}} \end{center}

\noindent Gives the variable assignment notation: $\alpha \difmost{v} \beta$, meaning `$\beta$ differs from $\alpha$ in at most $v$'.
\\
\hrule

\begin{center}\verb|\lcma|\end{center}

\noindent Gives $\lcma$, the `logical comma' that Professor Beau Mount uses in the PTLP lecture notes.
\\
\hrule
\begin{center}\verb|\semval{<sent.>}{<structure>}[<var.assign.>]|\end{center}

\noindent Gives \semval{\texttt{<sent.>}}{A}[a], the semantic value of some sentence over model $\mathcal{A}$ with variable assignment $\alpha$. The input \texttt{<structure>} is converted to \verb|\mathcal{...}|. If the input \texttt{<var.assign.>} is a single latin letter (e.g. `a', `b', `d' `g'), it is converted into an appropriate greek one\footnote{This respects capitalisation, so one gets $\gamma$ from `g', and $\Gamma$ from `G'.}.
\\
\hrule
\begin{center}\verb|\lsym{<language>}[<signature>]|\footnote{This command loads even without the package option `oxford'. Why? Because I couldn't get it to work otherwise.}\end{center}

\noindent Gives \lsym{$\circ$}, where $\circ$ can be 1,2,= or something else. Also optionally allows the addition of a superscript, for a signature. The `=' uses \verb|\@ltoolsshorteq|, `$\shorteq$', which is prettier in most fonts.
\\
\hrule

%parstackkern        .muskip_set:N = \l__formal_parstackkern_muskip,
%  parinnerpad         .muskip_set:N = \l__formal_parinnerpad_muskip,
%  italiccorrection    .muskip_set:N = \l__formal_italiccorrection_muskip,
%  parvoffset          .dim_set:N = \l__formal_parvoffset_dim,
%  quantskip           .muskip_set:N = \l__formal_quantskip_muskip,
%  lastquantskip       .muskip_set:N = \l__formal_lastquantskip_muskip,
%  scriptspace         .dim_set:N = \l__formal_scriptspace_dim,
\end{document}