%% logictools.sty
%% Copyright 2025 Miles Min Yin Cheang
%
% 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
% http://www.latex-project.org/lppl.txt
% and version 1.3 or later is part of all distributions of LaTeX
% version 2005/12/01 or later.
%
% This work has the LPPL maintenance status “maintained”.
%
% The Current Maintainer of this work is Miles Min Yin Cheang
%
% This work consists of the file logictools.sty
\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{logictools}[2025/05/20, v0.1.1. logictools]
\RequirePackage[only,llparenthesis,rrparenthesis]{stmaryrd}
\RequirePackage{amsmath}
\RequirePackage{xfrac}
\RequirePackage{bussproofs}
\RequirePackage{adjustbox}
\RequirePackage{trimspaces}
\DeclareOption{oxford}{\let\formal@oxford\@empty}
\DeclareOption*{\PackageWarning{logictools}{Unknown ‘\CurrentOption’}}
\ProcessOptions\relax
% Loaded when package option oxford used:
\@ifundefined{formal@oxford}{}{%
\RequirePackage{bussproofs}
% Provides semantic value function
% Gives automatic mathcal letters for the structure
% Optionally gives a variable assignment, where if a single Latin letter is input then it will return the associated Greek symbol.
\NewDocumentCommand{\semval}{m m o}
{%
\IfNoValueTF{#3}
{\ensuremath{|#1|_{\mathcal{#2}}}}
{\ensuremath{|#1|_{\mathcal{#2}}^{\latinletterstogreek{#3}}}}%
}%
% Provides "y differs from x in at most v" sign
\newcommand{\difmost}[1]{%
\overset{#1}{\sim}%
}
% Provides logical comma symbol
\newcommand{\lcma}{%
\adjustbox{trim={.45\width} 0pt 0pt 0pt ,clip}{$\circ$}%
}
% Provides an easy way to notate an unspecified proof from a set of premisses
% Optionally, can include discharged assumptions
\NewDocumentCommand{\prooffrom}{m t^ t_ o d<> m}
{%
\def\@prffrmalign{m}%
\IfBooleanT{#2}%
{%
\IfBooleanT{#3}{\PackageWarning{logictools}{You shouldn't use both ^ and _ in one prooffrom. You got lucky, if you had done this the other way around (_^) everything would break.}}%
\def\@prffrmalign{t}%
}%
\IfBooleanT{#3}{\def\@prffrmalign{b}}%
\IfNoValueTF{#4}%
{\IfNoValueTF{#5}%
{\alwaysNoLine%
\AxiomC{\fbox{#1}}%
\UnaryInfC{\raisebox{0.675ex}[3.25ex]{\smash{$\vdots$}}}%
\UnaryInfC{#6}%
\alwaysSingleLine}
{\alwaysNoLine%
\AxiomC{\adjustbox{fbox,valign=\@prffrmalign}{#1}\adjustbox{valign=\@prffrmalign, rlap}{\hspace{0.1em}\scriptsize#5}}%
\UnaryInfC{\raisebox{0.675ex}[3.25ex]{\smash{$\vdots$}}}%
\UnaryInfC{#6}%
\alwaysSingleLine}%
}%
{\IfNoValueF{#5}{\PackageWarning{logictools}{You shouldn't use both [...] and <...> in one prooffrom. You got lucky, if you had done this the other way around (<...>[...]) you would have gotten strange results.}}%
\alwaysNoLine%
\AxiomC{\adjustbox{fbox,valign=\@prffrmalign}{#1}\adjustbox{valign=\@prffrmalign, rlap}{\hspace{0.1em}\scriptsize$\left[\text{#4}\right]$}}%
\UnaryInfC{\raisebox{0.675ex}[3.25ex]{\smash{$\vdots$}}}%
\UnaryInfC{#6}%
\alwaysSingleLine}%
}%
}
%---------------------------------------------------------------------
% Thanks to everyone at TeX-exchange for teaching me how to use expl3!
\ExplSyntaxOn
\exp_args:Nc \mathchardef { __formal_original_): }=\char_value_mathcode:n {`)}
\exp_args:Nc \mathchardef { __formal_original_(: }=\char_value_mathcode:n {`(}
\exp_args:Nc \mathchardef { __formal_original_|: }=\char_value_mathcode:n {`|}
\exp_args:Nc \mathchardef { __formal_original_;: }=\char_value_mathcode:n {`;}
\exp_args:Nc \mathchardef { __formal_original_.: }=\char_value_mathcode:n {`.}
\exp_args:Nc \mathchardef { __formal_original_[: }=\char_value_mathcode:n {`[}
% Error messages:
\msg_new:nnnn { logictools } { quantnoglobaldeferror }{}{} % msg if global def for a quantifier went missing
\msg_new:nnnn { logictools } { quantneverdeferror }{}{} % msg if quant is never defined at all
\tl_new:N \l__formal_rparchar_tl % the right parenthesis used in formallogic
\tl_new:N \l__formal_lparchar_tl % the left parenthesis used in formallogic
\keys_define:nn {formal/options}
{
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,
parstackkern .default:n = -0.9mu,
parinnerpad .default:n = 0.9mu,
italiccorrection .default:n = 1.12mu,
parvoffset .default:n = 0.2ex,
quantskip .default:n = 4.32mu,
lastquantskip .default:n = 4.32mu,
scriptspace .default:n = -0.025em,
partype .choice:,
partype / double .code:n =
\tl_set:Nn \l__formal_rparchar_tl {\rrparenthesis}
\tl_set:Nn \l__formal_lparchar_tl {\llparenthesis},
partype / single .code:n =
\tl_set:Nn \l__formal_rparchar_tl {\use:c{__formal_original_):}}
\tl_set:Nn \l__formal_lparchar_tl {\use:c{__formal_original_(:}},
partype / unknown .code:n =
\msg_error:nneee { formal/options } { unknown_bracket_type }
{ partype } % Name of choice key
{ double , single } % Valid choices
{ \exp_not:n {#1} }, % Invalid choice given
partype .default:n = single,
}
% Initialise all the keys
\keys_set:nn {formal/options}
{
parstackkern,
parinnerpad,
italiccorrection,
parvoffset,
quantskip,
lastquantskip,
partype,
scriptspace,
}
\bool_new:N \l__formal_rparpadreq_bool % this boolean will be true when we need padding on an rpar
\bool_set_true:N \l__formal_rparpadreq_bool
\bool_new:N \l__formal_escaped_bool % this boolean will be true if content is surrounded by ""
\bool_set_false:N \l__formal_escaped_bool
\box_new:N \l__formal_lpar_box % the box for parentheses
\box_new:N \l__formal_rpar_box
\cs_new_protected:Nn \__formal_llpar_char:
{
\bool_if:NTF \l__formal_escaped_bool
{\use:c {__formal_original_(:}}
{
\box_use:N \l__formal_lpar_box \peek_charcode:NF ( {\mskip \l__formal_parinnerpad_muskip}
}
}
\cs_new_protected:Nn \__formal_rrpar_char:
{
\bool_if:NTF \l__formal_escaped_bool
{\use:c {__formal_original_):}}
{
\bool_if:NTF \l__formal_rparpadreq_bool
{\mskip \l__formal_parinnerpad_muskip \mkern \l__formal_italiccorrection_muskip}
{}
\box_use:N \l__formal_rpar_box
\peek_charcode:NTF ) {\bool_set_false:N \l__formal_rparpadreq_bool} {\bool_set_true:N \l__formal_rparpadreq_bool}
}
}
\cs_new_protected:Nn \__formal_escapetoggle:
{
\bool_set_inverse:N \l__formal_escaped_bool
}
\cs_new_protected:Nn \__formal_quantstackenter:
{
\bool_if:NTF \l__formal_escaped_bool
{\use:c {__formal_original_|:}}
{
\begingroup
\char_set_active_eq:nN { `| } \__formal_quantstackesc:
\char_set_active_eq:nN { `; } \__formal_quantdivider:
\char_set_mathcode:nn { `; } { "8000 }
\__formal_headquant:w
}
}
\cs_new_protected:Npn \__formal_headquant:w #1,
{
\tl_trim_spaces_apply:nN {#1} \__formal_headbox:n
}
\cs_new_protected:Npn \__formal_headbox:n #1
{
\box_if_exist:cTF {l__formal_#1head_box}
{
\box_if_empty:cTF {l__formal_#1head_box}
{
\box_if_exist:cTF {g__formal_#1head_box}
{\box_use:c{g__formal_#1head_box}}
{
\msg_set:nnnn { logictools } { quantnoglobaldeferror }{Quantifier~’#1’~not~defined~\msg_line_context:.}{You~are~attempting~to~use~a~locally~declared~quantifier~outside~of~its~group.~Either~define~it~globally~with~DeclareQuantifier,~or~define~it~locally~here~too.\\ \msg_see_documentation_text:n {logictools}}
\msg_error:nn {logictools} {quantnoglobaldeferror}
}
}
{
\box_use:c{l__formal_#1head_box}
}
}
{
\msg_set:nnnn { logictools } { quantneverdeferror }
{Quantifier~’#1’~used~but~never~defined.}{You~must~declare~quantifiers~with~the~command(s)~(L)DeclareQuantifier~before~using~them.\\ \msg_see_documentation_text:n {logictools}}
\msg_error:nn {logictools} {quantneverdeferror}
}
}
\cs_new_protected:Npn \__formal_quantdivider:
{
\bool_if:NTF \l__formal_escaped_bool
{\use:c {__formal_original_;:}}
{\__formal_bodyquant:w}
}
\cs_new_protected:Npn \__formal_bodyquant:w #1,
{
\mskip \use:c{l__formal_quantskip_muskip} \tl_trim_spaces_apply:nN {#1} \__formal_bodybox:n
}
\cs_new_protected:Npn \__formal_bodybox:n #1
{
\box_if_exist:cTF {l__formal_#1body_box}
{
\box_if_empty:cTF {l__formal_#1body_box}
{
\box_if_exist:cTF {g__formal_#1body_box}
{\box_use:c{g__formal_#1body_box}}
{
\msg_set:nnnn { logictools } { quantnoglobaldeferror }{Quantifier~’#1’~not~defined~\msg_line_context:.}{You~are~attempting~to~use~a~locally~declared~quantifier~outside~of~its~group.~Either~define~it~globally~with~DeclareQuantifier,~or~define~it~locally~here~too.\\ \msg_see_documentation_text:n {logictools}}
\msg_error:nn {logictools} {quantnoglobaldeferror}
}
}
{
\box_use:c{l__formal_#1body_box}
}
}
{
\msg_set:nnnn { logictools } { quantneverdeferror }
{Quantifier~’#1’~used~but~never~defined.}{You~must~declare~quantifiers~with~the~command(s)~(L)DeclareQuantifier~before~using~them.\\ \msg_see_documentation_text:n {logictools}}
\msg_error:nn {logictools} {quantneverdeferror}
}
}
\cs_new_protected:Nn \__formal_quantstackesc:
{
\endgroup \mskip \use:c{l__formal_lastquantskip_muskip}
}
\cs_new_protected:Nn \__formal_dot:
{
\bool_if:NTF \l__formal_escaped_bool
{\use:c {__formal_original_.:}}
{\peek_charcode_remove:NTF =
{\doteq}
{\use:c {__formal_original_.:}}}
}
\cs_new_protected:Nn \__formal_lbrack:
{
\bool_if:NTF \l__formal_escaped_bool
{\use:c {__formal_original_[:}}
{\__formal_varsub:w}
}
\cs_new_protected:Npn \__formal_varsub:w #1/#2]
{
\left["\sfrac{"#1"}{"#2"}"\right]
}
\NewDocumentEnvironment{formallogic}{O{}}
{
\setlength{\parindent}{0pt}
\cs_set:Npn \par {$\newline$}
\keys_set:nn {formal/options} % Load any settings given in the optional argument.
{
#1,
}
\setlength\scriptspace{\l__formal_scriptspace_dim}
\hbox_set:Nn \l__formal_lpar_box
{
\raisebox{\l__formal_parvoffset_dim}{$\l__formal_lparchar_tl \mkern \l__formal_parstackkern_muskip$}
}
\hbox_set:Nn \l__formal_rpar_box
{
\raisebox{\l__formal_parvoffset_dim}{$\mkern \l__formal_parstackkern_muskip \l__formal_rparchar_tl$}
}
\char_set_active_eq:nN { `( } \__formal_llpar_char:
\char_set_mathcode:nn { `( } { "8000 }
\char_set_active_eq:nN { `) } \__formal_rrpar_char:
\char_set_mathcode:nn { `) } { "8000 }
\char_set_active_eq:nN { `" } \__formal_escapetoggle:
\char_set_mathcode:nn { `" } { "8000 }
\char_set_active_eq:nN { `| } \__formal_quantstackenter:
\char_set_mathcode:nn { `| } { "8000 }
\char_set_active_eq:nN { `. } \__formal_dot:
\char_set_mathcode:nn { `. } { "8000 }
\char_set_active_eq:nN { `[ } \__formal_lbrack:
\char_set_mathcode:nn { `[ } { "8000 }
\(
\peek_charcode:NTF ) {\bool_set_false:N \l__formal_rparpadreq_bool} {\bool_set_true:N \l__formal_rparpadreq_bool}
}
{\)}
% make quants
\NewDocumentCommand{\DeclareQuantifier}{m m O{0mu} O{0mu}}
{
\box_if_exist:cF {g__formal_#1head_box}
{
\box_new:c {g__formal_#1head_box}
\box_new:c {g__formal_#1body_box}
}
\box_if_exist:cF {l__formal_#1head_box}
{
\box_new:c {l__formal_#1head_box}
\box_new:c {l__formal_#1body_box}
}
\hbox_gset:cn {g__formal_#1head_box}
{
$#2 \mkern#4$
}
\hbox_gset:cn {g__formal_#1body_box}
{
$\mskip#3 #2 \mkern#4$
}
}
\NewDocumentCommand{\LDeclareQuantifier}{m m O{0mu} O{0mu}}
{
\box_if_exist:cF {l__formal_#1head_box}
{
\box_new:c {l__formal_#1head_box}
\box_new:c {l__formal_#1body_box}
}
\hbox_set:cn {l__formal_#1head_box}
{
$#2 \mkern#4$
}
\hbox_set:cn {l__formal_#1body_box}
{
$\mskip#3 #2 \mkern#4$
}
}
% Use this command to declare settings that will stay for the rest of the document!
\NewDocumentCommand \logictoolsoptions { m }
{
\keys_set:nn {formal/options}
{
#1
}
}
% Command that puts things inside the formallogic environment, can be used inline.
\NewDocumentCommand \fmllgc {o m}
{
\text{\begin{formallogic}[#1]#2
\end{formallogic}}
}
%--------------------------------------------------
% A command for turning latin characters into greek ones
\NewDocumentCommand{\latinletterstogreek}{m}
{
\str_case_e:nnF { #1 }
{
{a}{\alpha}
{b}{\beta}
{c}{\varsigma}
{d}{\delta}
{e}{\varepsilon}
{f}{\varphi}
{g}{\gamma}
{h}{\eta}
{i}{\iota}
{j}{\vartheta}
{k}{\kappa}
{l}{\lambda}
{m}{\mu}
{n}{\nu}
{o}{o}
{p}{\pi}
{q}{\chi}
{r}{\rho}
{s}{\sigma}
{t}{\tau}
{u}{\upsilon}
{v}{\nu}
{w}{\omega}
{x}{\xi}
{y}{\psi}
{z}{\zeta}
{A}{\mathrm{A}}
{B}{\mathrm{B}}
{C}{\Sigma}
{D}{\Delta}
{E}{\mathrm{E}}
{F}{\Phi}
{G}{\Gamma}
{H}{\mathrm{H}}
{I}{\mathrm{I}}
{J}{\Theta}
{K}{\mathrm{K}}
{L}{\Lambda}
{M}{\mathrm{M}}
{N}{\mathrm{N}}
{O}{\mathrm{O}}
{P}{\Pi}
{Q}{\mathrm{X}}
{R}{\mathrm{P}}
{S}{\Sigma}
{T}{\mathrm{T}}
{U}{\Upsilon}
{V}{\mathrm{V}}
{W}{\Omega}
{X}{\Xi}
{Y}{\Psi}
{Z}{\mathrm{Z}}
}
{#1}
}
\ExplSyntaxOff
%-----------------------------------------------------------------------------
% Shorter equals sign
\newcommand{\@ltoolsshorteq}{%
\settowidth{\@tempdima}{$x$}% Width of x in mathfont
\resizebox{\@tempdima}{\height}{=}%
}
\ExplSyntaxOn
% Provides the symbols for l-one, l-two, l-equals and nice looking superscript
\NewDocumentCommand{\lsym}{m o}%
{
\IfNoValueTF{#2}
{% No superscript:
\str_case:nnF {#1}
{
{1}{\text{$\mathcal{L}\sb{1}$}}
{2}{\text{$\mathcal{L}\sb{2}$}}
{=}{\text{$\mathcal{L}\sb{\text{\hspace{0.01em}\@ltoolsshorteq}}$}}
}
{\text{$\mathcal{L}\sb{\text{#1}}$}}
}
{% Superscript:
\str_case:nnF {#1}
{
{1}{\text{$\mathcal{L}\sb{1}^{\text{#2}}$}}
{2}{\text{$\mathcal{L}\sb{2}^{\text{#2}}$}}
{=}{\text{$\mathcal{L}\sb{\text{\hspace{0.01em}\@ltoolsshorteq}}^{\text{#2}}$}}
}
{\text{$\mathcal{L}\sb{\text{#1}}^{\text{#2}}$}}
}
}
\ExplSyntaxOff
\DeclareQuantifier{exists}{\exists}
\DeclareQuantifier{forall}{\forall}
% Fix for amsmath messing with math-active codes.
\edef\originalbmathcode{%
\noexpand\mathchardef\noexpand\@tempa\the\mathcode`\(\relax}
\def\resetMathstrut@{%
\setbox\z@\hbox{%
\originalbmathcode
\def\@tempb##1"##2##3{\the\textfont"##3\char"}%
\expandafter\@tempb\meaning\@tempa \relax
}%
\ht\Mathstrutbox@\ht\z@ \dp\Mathstrutbox@\dp\z@
}