open-logic-config.sty

% % The Default OLP Configuration File `open-logic-config.sty`
% % Open Logic Project
%
% Description
% ===========
%
% This file contains all commands and environments that are meant to
% be configured, changed, or adapted by a user generating their own
% text based on OLP text.  **Do not edit this file to customize your
% OLP-derived text!** A file `myversion.tex` adapted from
% `open-logic-complete.tex` (or from any of the contributed example
% master files) will include `myversion-config.sty` if it exists. It
% will do so after it loads this file, so your `myversion-config.sty`
% will redefine the defaults.  This means you won't have to include
% everything, e.g., you can just change some tags and nothing else. You
% may copy and paste definitions you want to change into that file, or
% copy thi file, rename it `myversion-config.sty` and delete anything
% you'd like to leave as the default.

\NeedsTeXFormat{LaTeX2e}

% Symbols
% =======

% Formula metavariabes 
% --------------------
%
% Use the exclamation point symbol `!` immediately in front of an
% uppercase letter in math mode for formula metavariables.  By
% default, `!A`, `!B`, ... are typeset as $\varphi$, $\psi$, $\chi$,
% ... if you use the command `\olgreekformulas`. If this is not desired,
% and you'd like $A$, $B$, $C$, ... instead, use `\ollatinformulas`.
% If you issue `\olalphagreekformulas`, you'll get $\alpha$, $\beta$,
% $\gamma$, \dots.

\olgreekformulas

% We prefer `\varphi` to `\phi` and `\varepsilon` to `\epsilon`. If
% you don't, you can say
% ```
% \let\phi\oldphi
% \let\epsilon\oldepsilon
% ```

\let\oldphi\phi
\let\phi\varphi

\let\oldepsilon\epsilon
\let\epsilon\varepsilon

% Logical symbols
% ---------------

% The following commands are used in the OLP texts for logical
% symbols. Their definitions can be customized to produce different
% output.

% ### Truth Values
%
% - `\True` defaults to $\mathbb{T}$ and `\False` to $\mathbb{F}$.

\DeclareDocumentMacro \True {\ensuremath{\mathbb{T}}}
\DeclareDocumentMacro \False {\ensuremath{\mathbb{F}}}

% For many-valued logic we have `\Indet` ($\mathbb{I}$) and `Undef' ($\mathbb{U}$).

\DeclareDocumentMacro \Indet {\ensuremath{\mathbb{I}}}
\DeclareDocumentMacro \Undef {\ensuremath{\mathbb{U}}}

% ### Propositional Constants and Connectives
%
% - Falsity is `\lfalse` and defaults to $\bot$.

\DeclareDocumentMacro \lfalse {\bot}

% - Truth is `\ltrue` and defaults to $\top$.

\DeclareDocumentMacro \ltrue {\top}

% - Negation is `\lnot` and defaults to $\lnot$.  To use a different
% symbol (e.g., tilde), include the following code:
% ```
% \DeclareDocumentMacro \lnot {\mathord{\sim}}
% ```

% - Conjunction is `\land` and deaults to $\land$. To use ampersand,
% include the following code:
% ```
% \DeclareDocumentMacro \land {\mathbin{\&}}
% ```

% - Disjunction is `\lor` and defaults to $\lor$.

% - Conditional is `\lif` and defaults to $\rightarrow$.  To use a
% different symbol, replace `\rightarrow` in the definition, e.g., by
% `\supset`

\DeclareDocumentMacro \lif {\mathbin{\rightarrow}}

% - The biconditional is `\liff` and defaults to $\leftrightarrow$.  To
% use the triple bar $\equiv$ replace with `\equiv`.

\DeclareDocumentMacro \liff {\mathbin{\leftrightarrow}}

% - NAND (Sheffer stroke) and NOR (Peirce arrow) operators

\DeclareDocumentMacro \lnand {\mathbin{\uparrow}}
\DeclareDocumentMacro \lnor {\mathbin{\downarrow}}

% - The conditional `\cif` and defaults to `\boxright` which produces
%   Lewis's box-arrow symbol.

\DeclareDocumentMacro \cif {\boxright}

% - The strict conditional `\strictif` defaults to `\fishhookright`

\DeclareDocumentMacro \strictif {\fishhookright}

% Quantifiers 
% ----------- 

% The quantifier symbols are provided as commands `\lexists` and
% `\lforall` which take two optional arguments. If no arguments are
% provided, it they just typeset the quantifier symbol. With one
% optional argument they produce the quantifier together with a
% variable, and this may include parenthesesaround the quantifier and
% variable. The second optional argument producesthe
% quantifier/variable combination plus the formula in the scope of the
% formula with appropriate spacing.  For instance,
% `\lexists[x][!A(x)]` will, by default, produce $\exists
% x\,\varphi(x)$.

% - The existential quantifier is `\lexists`.  Replace `\exists` with
% `\boldsymbol{\exists}` for boldface, or redefine appropriately if
% you want parentheses around $\exists x$.

\DeclareDocumentCommand \lexists { t{!} o o } {
    \exists 
    \IfBooleanTF {#1} 
        \mathexclaim    % unique
        \relax % not unique
    \IfNoValueTF {#2} 
        \relax     % no arguments
        { #2 } % one argument: variable
    \IfNoValueTF {#3} 
        \relax
        { \, #3 }      % two arguments: space and matrix
}

% - The universal quantifier is `\lforall`.

\DeclareDocumentCommand \lforall { o o } {
    \IfNoValueTF {#1} 
        { \forall }    % no arguments
        { \forall #1 } % one argument: variable
    \IfNoValueTF {#2} 
        \relax
        { \, #2 }      % two arguments: space and matrix
}

% - The identity relation is also provided as `\eq`. By itself, it
% produces the identity reation symbol (default: $=$) by itself. With
% two optional arguments, it typesets the corresponding atomic
% formula, e.g., `\eq[x][y]` produces $x = y$.  `\eq/` produces the
% negated symbol (formula).

\DeclareDocumentCommand \eq { t{/} o o } {
  \IfNoValueTF {#3}
    % no optional arguments: just typeset symbol
    { \IfBooleanTF{#1}{ \neq }{ = } }
    % optional arguments: typeset atomic formula
    { \IfBooleanTF{#1}{ #2 \neq #3}{#2 = #3} }
}

% Proofs and Derivations
% ----------------------

% - The sequent symbol `\Sequent` produces $\Rightarrow$ by
% default. Change the definition for $\vdash$, or another symbol.

\DeclareDocumentMacro \Sequent {\Rightarrow}

\DeclareDocumentMacro \nSequent {\mid}

% - The sequent symbol in proofs displays as the above sequent symbol.
%   (We use the `bussproofs` package to typeset proofs.)

\DeclareDocumentMacro \fCenter {\ensuremath{\,\Sequent\,}}

% - Rule names: `\LeftR{Op}` typesets the name of a left rule for
% operator `Op`, e.g., `\LeftR{\land}` produces `$\land$L`.
% `\RightR{Op}` does the same for right rules.

\DeclareDocumentCommand \LeftR { m } {\ensuremath{{#1}\mathrm{L}}}

\DeclareDocumentCommand \RightR { m } {\ensuremath{{#1}\mathrm{R}}}

\DeclareDocumentCommand \iR { m m o} {\ensuremath{{#1\IfNoValueTF{#3}{}{_{#3}}}{#2}}}

% - `\Weakening`: produces name or abbreviation for weakening rule,
% e.g., ``W''.

\DeclareDocumentMacro \Weakening {\ensuremath{\mathrm{W}}}

% - `\Contraction`: produces name or abbreviation for contraction rule,
% e.g., ``C''.

\DeclareDocumentMacro \Contraction {\ensuremath{\mathrm{C}}}

% - `\Exchange`: produces name or abbreviation for exchange rule,
% e.g., ``X''.

\DeclareDocumentMacro \Exchange {\ensuremath{\mathrm{X}}}

% - `\Cut`: produces name or abbreviation for cut rule,
% e.g., ``Cut''.

\DeclareDocumentMacro \Cut {\ensuremath{\mathrm{Cut}}}

% - Rule names: `\Intro{Op}` typesets the name of an intro rule for
% operator `Op`, e.g., `\Intro{\land}` produces `$\land$Intro`.
% `\Elim{Op}` does the same for elimination rules.

\DeclareDocumentCommand \Intro { m o } {\ensuremath{{#1}\mathrm{Intro}\IfNoValueTF{#2}{}{_{#2}}}}

\DeclareDocumentCommand \Elim { m o } {\ensuremath{{#1}\mathrm{Elim}\IfNoValueTF{#2}{}{_{#2}}}}

% - `\FalseInt`, `\FalseCl`: produces name or abbreviation for
% intuitionistic and classical absurdity rule, e.g., ``$\bot_I$,''
% ``$\bot_C$''.

\DeclareDocumentMacro \FalseInt {\ensuremath{\lfalse_I}}
\DeclareDocumentMacro \FalseCl {\ensuremath{\lfalse_C}}

% - `\Discharge{!A}{n}`: typesets a discharged assumption with label
% $n$, e.g., $[\phi]^n$.

\DeclareDocumentCommand \Discharge { m m }{[#1]^{#2}}

% - `\DischargeRule{Rule}{n}`: used in a `prooftree` environment to
% provide the labels for an inference that discharges an assumption.

\DeclareDocumentCommand \DischargeRule { m m }{
  \RightLabel{#1}
  \LeftLabel{\scriptsize $#2$}
}

% Proof Terms
% ---------------------
%
% Proof terms used in intuitionistic logic

\DeclareDocumentCommand \typeof { m m } {#1^{#2}}

\DeclareDocumentCommand \andi { m m } {\tuple{#1, #2}}
\DeclareDocumentCommand \ande { m m } {\fn{p}_{#1}(#2)}
\DeclareDocumentCommand \ori { m m m } {\fn{in}_{#1}^{#2}(#3)}
\DeclareDocumentCommand \ore { m m m m m } {\fn{case}(#1, #2.#3, #4.#5)}
\DeclareDocumentCommand \falsee { m m } {\fn{contr}_{#1}(#2)}

% Axiomatic Derivations
% ---------------------

% - `\MP`: produces abbreviation for Modus Ponens.

\DeclareDocumentMacro \MP {\textsc{mp}}

% - `\QR`: produces abbreviation for Quantifier Rule.

\DeclareDocumentMacro \QR {\textsc{qr}}

% - `\Hyp`: produces abbreviation for Hypothesis.

\DeclareDocumentMacro \Hyp {\textsc{Hyp}}

% - `\sFmla`: Signed (prefixed) formulas in running text

\DeclareDocumentCommand \sFmla { m m o }{
  \ensuremath{%
    \IfNoValueTF{#3}{}{#3\,}%
    \hbox to.8em{\ensuremath{#1}\hfil} #2}}

% - `\pFmla`: signed prefixed formulas for tableaux

\DeclareDocumentCommand \pFmla { m m m }{
  \ensuremath{%
    \hskip 3em{\llap{$#3$}\,}%
    \hbox to1.3em{\ensuremath{#1}\hfil} #2}}

% Tableaux
% --------

% - Tableau rule names: `\TRule{Sign}{Op}[line]` typesets the name of a the
% `Sign` rule for operator `Op`. The optional argument contains the
% line number to which the rule is applied.

\DeclareDocumentCommand \TRule { m m o }{%
  \ensuremath{{#2}{#1}\IfNoValueTF{#3}{}{\, #3}}}

% - `\TAss`: justification label for ``assumption''

\DeclareDocumentMacro \TAss {Assumption}


% Metalogical Relations
% ---------------------
%
% Metalogical relationships, such as truth in a structure, validity,
% consequence, and provability, are also provided as commands. Uniform
% use of these commandsinstead of hard-coded typesetting according to
% specific conventions guarantees that by changing the definitions
% below you can uniformly change notation in the text.


% ### Substitution

% - `\subst{t}{x}`: typeset the substitution notation

\DeclareDocumentCommand \subst { m m } {#1/#2}

% - `\SSubst{A}{s}`: typeset simultaneous substitution (expects $s$ to
% be a list of `\subst{t}{x}` expressions, say)

\DeclareDocumentCommand \SSubst { m m } {
  #1[#2]}

% - `\Subst{!A}{t}{x}`: The operation of substituting a term for a
% (free) variable in another term or in a formula.  The default is
% $\varphi[x/t]$, other common notations are $\varphi^t_x$,
% $\varphi\{t \rightarrow x\}$, or $S^t_x \varphi$.

\DeclareDocumentCommand \Subst { m m m } {
  #1[\subst{#2}{#3}]}

% ### pre-Substitution

\DeclareDocumentCommand \pSubst { m m m } {
  #1[#2/#3]^{-}
}

% ### The satisfaction/truth relation 

% - `\Sat[/]{M}{!A}[s]`, the relation of being satisfied in a
% structure (relative to an assignment), is provided as the command
% `\Sat` with two mandatory arguents (the structure and the formula)
% and one optional argument (the assignment).  Use `\Sat/` to create
% the negated relation.  By default, `\Sat{M}{!A}[s]` is typeset as
% $\mathfrak{M}, s \models \varphi$.

\DeclareDocumentCommand \Sat { t{/} m m o } {
  \IfBooleanTF{#1}{
    % negated
    \IfNoValueTF {#4} 
        { \Struct{#2} \nvDash #3 }
        { \Struct{#2}, #4 \nvDash #3}}{
    % not negated
    \IfNoValueTF {#4} 
        { \Struct{#2} \vDash #3 }
        { \Struct{#2}, #4 \vDash #3 }}
}

% ### The derivability relation

% - `\Proves[L]` is used to create the symbol for the derivability
% relation, `\Proves/` for the negation. By default this creates
% $\vdash$; e.g., `\Gamma \Proves !A` yields $\Gamma \vdash
% \varphi$. An optional argument may be used for the calculus or logic
% relative to which the provability relation is defined; by default it
% creates a subscript on the turnstile.

\DeclareDocumentCommand \Proves { t{/} o } {
  \IfBooleanTF {#1}{
    \IfNoValueTF {#2} 
        { \nvdash }
        { \nvdash_{#2} }}{
    \IfNoValueTF {#2} 
        { \vdash }
        { \vdash_{#2} }}
}

% - `\Thms{X}`: theorems a set of formulas

\DeclareDocumentCommand \Thms { m } {\mathrm{Thm}(#1)}

% - `\PAx`: the set of propositional axioms

\DeclareDocumentMacro \PAx { \mathrm{Ax}_0 }

% ### The semantic consequence relation relation

% - `\Entails` is the semantic counterpart of `\Proves` and defaults to
% $\vDash$. It also takes an optional `/` for $\nvDash$ and an
% optional argument for a subscript.

\DeclareDocumentCommand \Entails { t{/} o } {
  \IfBooleanTF {#1}{
    \IfNoValueTF {#2} 
        { \nvDash }
        { \nvDash_{#2} }}{
    \IfNoValueTF {#2} 
        { \vDash }
        { \vDash_{#2} }}
}


% ### Model-theoretic notions and symbols

% - `\Domain{M}` - domain of a structure, e.g., `\Domain{M}` gives
% $\left|\mathfrak M\right|$.

\DeclareDocumentCommand \Domain { m }{\left| \Struct{#1} \right|}

% - `\Assign{R}{M}` - Assignment (value of) of a constant/predicate symbol
% in a structure; e.g., `\Assign{R}{M}` produces $R^\mathfrak{M}$.

\DeclareDocumentCommand \Assign { m m }{\mathord{#1^{\Struct{#2}}}}

% - `\varAssign{s'}{s}{x}[o]` - Assignment variant. Takes three mandatory
% argument (s' differs from s at most at x) and one optional one (s' assigns
% o to x. Default: `\varAssign{s'}{s}{x}` produces `s' \sim_{x} s`
% and `\varAssign{s'}{s}{x}[o] produces `s' = s[o/x]`.

\DeclareDocumentCommand \varAssign { m m m o } {
    \IfNoValueTF {#4}
        % optional argument not present
        { #1 \sim_{#3} #2 }
        % optional argument present
        { #1 = #2[^{#4}/{#3}] }
}

% - `\Value{t}{M}[s]` - Value of a term in a structure. Takes two mandatory
% arguments (term and structure) and one optional argument (variable
% assignment). By default, `\Value{t}{M}[s]` produces 
% $\mathrm{Val}^\mathfrak{M}_s(t)$.

\DeclareDocumentCommand \Value { m m o} {
    \IfNoValueTF {#3}
        % optional argument not present
        { \mathrm{Val}^{\Struct{#2}}(#1) }
        % optional argument present
        { \mathrm{Val}^{\Struct{#2}}_{#3}(#1) }
}

% - `\pAssign{v}` - Typeset a truth-value assignment

\DeclareDocumentCommand \pAssign { m } {\applytofirst{\mathfrak}{#1}}

% - `\pValue{v}(A)[L]` - Truth value of a formula under a truth-value assignment.

\DeclareDocumentCommand \pValue { m d() o}{
  \overline{\pAssign{#1}}%
  \IfNoValueTF{#3}{}{_{#3}}%
  \IfNoValueTF {#2}{}{(#2)}
}

% - `\pSat[/]{v}{!A}[L]`, the relation of being satisfied by a
% truth-value assignment in a logic L.

\DeclareDocumentCommand \pSat { t{/} m m o } {
  \pAssign{#2} 
      \IfBooleanTF{#1}{\nvDash}{\vDash}%
      \IfNoValueTF{#4}{}{_{#4}}
  #3
}

% - `\tf{\star}[L]`: truth function for $\star$ in $\mathbf{L}$

\DeclareDocumentCommand \tf { m o } {
      \widetilde{#1}%
      \IfNoValueTF{#2}{}{_{#2}}
}


% - `\substruct`: symbol for the substructure relation

\DeclareDocumentMacro \substruct {\subseteq}

% - `\Theory{M}`: theory of a structure

\DeclareDocumentCommand \Theory { m } {\mathrm{Th}(\Struct{#1})}

% - `\Mod[L](L'){T}`: class of models of a theory/sentence $T$ in a
% language $\mathcal{L}$ and logic $L'$.

\DeclareDocumentCommand \Mod { o d() m } {
  \IfNoValueTF {#2} {
  % optional logic argument not present
    \IfNoValueTF {#1}{
      \mathrm{Mod}(#3) }{
      \mathrm{Mod}^{\Lang{#1}}(#3) }}{
  % optional logic argument present
    \IfNoValueTF {#1}{
      \mathrm{Mod}_{#2}(#3)}{
      \mathrm{Mod}_{#2}^{\Lang{#1}}(#3)}}
}


% - `\elemequiv`: elementary equivalence (infix relation)

\DeclareDocumentCommand \elemequiv { t{/} o } {
  \IfBooleanTF {#1}{
    \IfNoValueTF {#2} 
        { \not\equiv }
        { \not\equiv_{#2} }}{
    \IfNoValueTF {#2} 
        { \equiv }
        { \equiv_{#2} }}
}

% - `\eqc`: the equivalence class the element (first argument) belongs
% to; second argument is used to mark the equivalence relation if
% there's more than one

\DeclareDocumentCommand \eqc { m o } {
  \IfNoValueTF {#2}
  {[#1]}
  {[#1]_{#2}}
}

% - `\rep`: the representative of an equivalence class, the second
% argument is used to mark the equivalence relation if there's more
% than one

\DeclareDocumentCommand \rep { m o } {
  \IfNoValueTF {#2}
  {\underline{#1}}
  {{\underline{#1}}_{#2}}
}

% - `\iso[/][p]`: relation of being (partially) isomorphic

\DeclareDocumentCommand \iso { t{/} o } {
  \IfBooleanTF {#1}{
    \IfNoValueTF {#2} 
        { \not\simeq }
        { \not\simeq_{#2} }}{
    \IfNoValueTF {#2} 
        { \simeq }
        { \simeq_{#2} }}
}



% - `\ident`: syntactic identity between expressions (infix relation),

\DeclareDocumentMacro \ident {\equiv}

% - `\QuantRank{!A}`: quantifier rank of a formula

\DeclareDocumentCommand \QuantRank { m } {\mathrm{qr}(#1)}

% - `\Expan{M}{R}`: expansion of a structure by a relation (etc.)

\DeclareDocumentCommand \Expan { m m } {(\Struct{#1}, #2)}

% - `\nssucc`, `\nsplus`, `\nstimes`, `\nsless`: non-standard
% arithmetical operations

\DeclareDocumentMacro \nszero {\mathbf{z}}
\DeclareDocumentMacro \nssucc {*}
\DeclareDocumentMacro \nsplus {\oplus}
\DeclareDocumentMacro \nstimes {\otimes}
\RequirePackage{stmaryrd}
\DeclareDocumentMacro \nsless {\varolessthan}


% Recursion-theoretic Notions and Symbols
% ---------------------------------------

% - `\Proj{n}{i}`: projection functions

\DeclareDocumentCommand \Proj { m m } {P^{#1}_{#2}}

% - `\Zero`: the constant zero function

\DeclareDocumentMacro \Zero {\fn{zero}}

% - `\Succ`: the successor function

\DeclareDocumentMacro \Succ {\fn{succ}}

% - `\Add`: the addition function

\DeclareDocumentMacro \Add {\fn{add}}

% - `\Mult`: the multiplication function

\DeclareDocumentMacro \Mult {\fn{mult}}

% - `\Exp`: the exponentiation function

\DeclareDocumentMacro \Exp {\fn{exp}}

% - `\Pred`: the successor function

\DeclareDocumentMacro \Pred {\fn{pred}}

% - `\tsub`: truncated subtraction function

\DeclareDocumentMacro \tsub {\mathbin{\dot-}}

% - `\Char{R}`: characteristic function

\DeclareDocumentCommand \Char { m } {\chi_{#1}}

% - `\defis`: definitional identity

\DeclareDocumentMacro \defis {=} %{\mathrel{=_\mathrm{df}}}

% - `\defiff`: definitional equivalence

\DeclareDocumentMacro \defiff {\Leftrightarrow}

% - `\concat`: concatenation of sequences

\DeclareDocumentMacro \concat {\frown}

% - `\umin{x}{!A}`: unbounded minimization

\DeclareDocumentCommand \umin { m m } {\mu #1 \; #2}

% - `\bmin{x < y}{!A}`: bounded minimization

\DeclareDocumentCommand \bmin { m m } {(\fn{min} \; #1)\, #2}

% - `\bexists{x < y}{!A}`: bounded existential quantification

\DeclareDocumentCommand \bexists { m m } {(\exists #1)\; #2}

% - `\bforall{x < y}{!A}`: bounded univeral quantification

\DeclareDocumentCommand \bforall { m m } {(\forall #1)\; #2}

% - `\cfind{e}[n]`: partial computable function with index $e$

\DeclareDocumentCommand \cfind { m o } {%
    \IfNoValueTF {#2}
        % optional argument not present
        { \varphi_{#1} }
        % optional argument present
        { \varphi_{#1}^{#2} }
}

% - `\fdefined`, `\fundefined`: postfix for defined, undefined
%   functions; LaTeX code for this is under ``Special sets and
%   mathematical symbols''

% Lambda calculus
% ---------------

% - `\redone`: one-step reduction

\DeclareDocumentCommand \redone { o } {
  \IfNoValueTF {#1}
  {\xrightarrow{}}
  {\xrightarrow{#1}}
}

\DeclareDocumentMacro \aconvone {\redone[\alpha]}

\DeclareDocumentMacro \bredone {\redone[\beta]}

\DeclareDocumentMacro \eredone {\redone[\eta]}

\DeclareDocumentMacro \beredone {\redone[\beta\eta]}

\DeclareDocumentMacro \xredone {\redone[X]}

% - `\red`: reduction

\DeclareDocumentCommand \xrightarrowdbl { o m } {
  \IfNoValueTF {#1}
  {\xrightarrow{#2} \mathrel{\mkern-14mu}\rightarrow}
  {\xrightarrow[#1]{#2} \mathrel{\mkern-14mu}\rightarrow}
}

\DeclareDocumentCommand \red { o } {
  \IfNoValueTF {#1}
  {\xrightarrowdbl{}}
  {\xrightarrowdbl{#1}}
}

\DeclareDocumentMacro \aconv {\red [\alpha]}

\DeclareDocumentMacro \bred {\red [\beta]}

\DeclareDocumentMacro \ered {\red [\eta]}

\DeclareDocumentMacro \bered {\red [\beta\eta]}

\DeclareDocumentMacro \xred {\red [X]}

% - `\equal`: equivalence relation with some letter over the symbol
\DeclareDocumentCommand \equal { o } {
  \IfNoValueTF {#1}
  {\eq}
  {\stackrel{#1}{\eq}}
}

\DeclareDocumentMacro \aeq {\equal [\alpha]}

% - `\eqs`: syntactic equivalent
\DeclareDocumentMacro \eqs {\equiv}

% - `\redpar`: parallel reduction

\DeclareDocumentCommand \redpar { o } {
  \IfNoValueTF {#1}
  {\xLongrightarrow{}}
  {\xLongrightarrow{#1}}
}

\DeclareDocumentMacro \bredpar {\redpar [\beta]}

\DeclareDocumentMacro \beredpar {\redpar [\beta\eta]}

\DeclareDocumentMacro \eqa {\equal{\alpha}}

\DeclareDocumentMacro \eqe {\equal{\eta}}

\DeclareDocumentMacro \ext {\ensuremath{\mathit{ext}}}

% - `\cd`: complete development

\DeclareDocumentCommand \cd { o m } {
  \IfNoValueTF {#1}
  {{ #2 }^*}
  {{ #2 }^{* {#1} }}
}

\DeclareDocumentCommand \bcd { m } {
  \cd[\beta]{#1}
}

\DeclareDocumentCommand \becd { m } {
  \cd[\beta\eta]{#1}
}

% - `\lambd[x][!A]`: lambda abstract

\DeclareDocumentCommand \lambd { o o } {
    \IfNoValueTF {#1} 
        { \lambda }    % no arguments
        { \lambda #1 } % one argument
    \IfNoValueTF {#2} 
        \relax
        { .\, #2 }      % two arguments
}

% Typed Lambda Calculus
% ---------------------

\DeclareDocumentCommand \pair { m m } {\tuple{#1,#2}}
\DeclareDocumentCommand \proj { m m } {\pi_{#1}(#2) }
\DeclareDocumentCommand \dcase { m m m m m } {\delta\, #1\, #2.#3\, #4.#5}
\DeclareDocumentCommand \inj {o m m} {
  \IfNoValueTF {#1} 
    { \iota_{#2}(#3) }
    { \iota_{#2}^{#1}(#3) }}
\DeclareDocumentCommand \abort {m m} {\varepsilon^{#1}(#2)}

% Arithmetization
% ---------------

% - `\num{n}` : numeral corresponding to a number

\DeclareDocumentCommand \num { m } {\overline{#1}}

% - `\scode{s}`: code for a symbol

\DeclareDocumentCommand \scode { m } {\fn{c}_{#1}}

% - `\Gn{!A}`: Gödel number of a string of symbols. (Corner quotes are
%   produced using `\gn{!A}`.)

\DeclareDocumentCommand \Gn { m } {{^{\reflectbox{\tiny\#}}}{#1}{^{\mbox{\tiny\#}}}}

% Modal Logic 
% -----------

% - `\mModel{M}` - modal structures; default: set first token in
% arguemnt in Fraktur

\DeclareDocumentCommand \mModel { m }{\applytofirst{\mathfrak}{#1}}

% - `\mSat[/]{M}{!A}[w]`, the relation of being satisfied in a
% model (at a world), is provided as the command
% `\mSat` with two mandatory arguments (the model and the formula)
% and one optional argument (the world).  Use `\mSat/` to create
% the negated relation.  By default, `\mSat{M}{!A}[w]` is typeset as
% $\mathfrak{M}, w \models \varphi$.

\DeclareDocumentCommand \mSat { t{/} m m o } {%
  \IfBooleanTF{#1}{%
    % negated
    \IfNoValueTF {#4} 
        { \mModel{#2} \nVdash #3 }
        { \mModel{#2}, #4 \nVdash #3}}{%
    % not negated
    \IfNoValueTF {#4} 
        { \mModel{#2} \Vdash #3 }
        { \mModel{#2}, #4 \Vdash #3 }}}

% - `\mClass{C}` --- typeset class of models

\DeclareDocumentCommand \mClass { m }{\mathcal{#1}}

% - `\Nec`: produces abbreviation for Necessitation.

\DeclareDocumentMacro \Nec {\textsc{nec}}

% - `\RK`: produces abbreviation for Rule K

\DeclareDocumentMacro \RK {\textsc{rk}}

% - `\Dual`: produces abbreviation for Dual

\DeclareDocumentMacro \Dual {\textsc{dual}}

% - `\Taut`: produces abbreviation for Dual

\DeclareDocumentMacro \Taut {\textsc{taut}}

% - `\PL`: produces abbreviation for ``Propositional Logic''

\DeclareDocumentMacro \PL {\textsc{pl}}

% - `\Prop{M}{A}`: the proposition defined by $A$ in $\mathfrak{M}$

\DeclareDocumentCommand \Prop { m m } {
  {[\!\![} #2 {]\!\!]_{\mModel{#1}}}
}

% - `\ST`: The standard translation

\DeclareDocumentMacro \ST {\mathord{\mathrm{ST}}}

% - TikZ style for modal models

\tikzset{
  modal/.style={>=stealth',
    shorten >=1pt,
    shorten <=1pt,
    auto,
    node distance=1.5cm,
    label distance=2pt,
    semithick},
  every label/.style={phantom,align=left},
  world/.style = {circle,draw,minimum size=0.5cm,fill=gray!15},
  modal every node/.style={world},
  point/.style={circle,draw,inner sep=0.5mm,fill=black},
  phantom/.style={rectangle,inner sep=0pt,draw=none,fill=none},
  reflexive above/.style={->,loop,looseness=7,in=60,out=120},
  reflexive below/.style={->,loop,looseness=7,in=240,out=300},
  reflexive left/.style={->,loop,looseness=7,in=150,out=210},
  reflexive right/.style={->,loop,looseness=7,in=30,out=330}
}

\DeclareDocumentCommand \mTrue { m }{\ensuremath{#1}}
\DeclareDocumentCommand \mFalse { m }{\ensuremath{\lnot #1}}

% Special modal operators

\DeclareDocumentMacro {\Knows} {\mathord{\mathsf{K}}}
\DeclareDocumentMacro {\EKnows} {\mathord{\mathsf{E}}}
\DeclareDocumentMacro {\CKnows} {\mathord{\mathsf{C}}}

\DeclareDocumentMacro {\Ptemp} {\mathord{\mathsf{P}}}
\DeclareDocumentMacro {\Htemp} {\mathord{\mathsf{H}}}
\DeclareDocumentMacro {\Ftemp} {\mathord{\mathsf{F}}}
\DeclareDocumentMacro {\Gtemp} {\mathord{\mathsf{G}}}
\DeclareDocumentMacro {\Since} {\mathord{\mathsf{S}}}
\DeclareDocumentMacro {\Until} {\mathord{\mathsf{U}}}

% Proof theory
% ------------

% height of a derivation

\settexttoken{height}{height}{heights}
\settexttoken{hp}{hp}{hp}

\DeclareDocumentCommand \pheight { m }{\fn{ht}(#1)}

% depth of a formula

\settexttoken{depth}{depth}{depths}

\DeclareDocumentCommand \depth { m }{\fn{dp}(#1)}

% cut measures

\DeclareDocumentCommand \cheight { m }{\fn{ch}(#1)}
\DeclareDocumentCommand \cutr { m }{\fn{cr}(#1)}

\DeclareDocumentMacro \CutCS {\ensuremath{\mathrm{Cut}_\mathrm{CS}}}

% delimiter for Maehara's lemma

\DeclareDocumentCommand \maeh { m m }{{#1 \mathrel{;} #2}}

% Special Sets and Mathematical Symbols
% -------------------------------------

% ### Set-theoretic operators

% - Set abstracts: Use `\Setabs{x}{!A(x)}` to produce the set abstract
% $\{ x : \varphi(x) \}$. If you prefer a $\mid$ to :, change the
% definition accordingly.

\DeclareDocumentCommand \Setabs { m m }{\{ #1 : #2 \}}

% - Fregean extensions: Use `\fregeext{x}{!A(x)}` to produce
%   $\epsilon x\, \varphi(x)$.

\DeclareDocumentCommand \fregeext { m m }{\oldepsilon #1 \, #2 }

% - Fregean number: Use `\fregenum{x}{!A(x)}` to produce 
%   $\# x\, \varphi(x)$.

\DeclareDocumentCommand \fregenum { m m }{\# #1 \, #2 }

% - `\Pow{X}`: Power set, produces $\wp(X)$

\DeclareDocumentCommand \Pow { m }{\wp(#1)}

% - `\dom{f}`: domain of a function

\DeclareDocumentCommand \dom { m }{\fn{dom}(#1)}

% - `\ran{f}`: range of a function
\DeclareDocumentCommand \ran { m }{\fn{ran}(#1)}

% - `\len{s}`: length of a sequence
\DeclareDocumentCommand \len { m }{\fn{len}(#1)}

% - `\emptyseq`: the empty sequence
\DeclareDocumentMacro \emptyseq {\Lambda}

% - `\restrict`: restriction of a function to a set (infix operator)
\DeclareDocumentMacro \restrict {\upharpoonright}

% - `\Complement{X}`: complement of a set
\DeclareDocumentCommand \Complement { m } {\overline{#1}}

% - `\card{X}`: cardinality of a set
\DeclareDocumentCommand \card { m } {\left| #1 \right|}

% - `\cardle{X}{Y}`: X is no larger than Y
\DeclareDocumentCommand \cardle { m m } {#1 \preceq #2}

% - `\cardless{X}{Y}`: X is smaller than Y
\DeclareDocumentCommand \cardless { m m } {#1 \prec #2}

% - `\cardeq{X}{Y}`: X is equinumerous with Y
\DeclareDocumentCommand \cardeq { m m } {#1 \approx #2}

% - `\tuple{x,y}`: pairs, tuples, sequences
\DeclareDocumentMacro \openTuple {\langle}
\DeclareDocumentMacro \closeTuple {\rangle}
\DeclareDocumentCommand \tuple { m } {\openTuple #1 \closeTuple}

% - `\comp{f}{g}`: composition of f with g, defaults to $g \circ f$
\DeclareDocumentCommand \comp { m m }{#2 \circ #1}

% - `\pto`: partial function arrow

\DeclareDocumentMacro \pto {\mathrel{\ooalign{\hfil$\mapstochar\mkern
      5mu$\hfil\cr$\to$}}}

% - `\fdefined`, `\fundefined`: postfix for defined, undefined
% functions

\DeclareDocumentMacro \fdefined {\downarrow}
\DeclareDocumentMacro \fundefined {\uparrow}

% - `cutrank`: cut rank

\DeclareDocumentCommand \cutrank { m }{\fn{cr}(#1)}

% - `maxrank`: max rank

\DeclareDocumentCommand \maxrank { m }{\fn{mr}(#1)}

% ### Particular sets

% - Natural numbers: `\Nat`
\DeclareDocumentMacro \Nat {\mathbb{N}}

% - Integers: `\Int`
\DeclareDocumentMacro \Int {\mathbb{Z}}

% - Positive integers: `\PosInt`
\DeclareDocumentMacro \PosInt {\mathbb{Z}^+}

% - Real numbers: `\Real`
\DeclareDocumentMacro \Real {\mathbb{R}}

% - Rational numbers: `\Rat`
\DeclareDocumentMacro \Rat {\mathbb{Q}}

% - The set $\{0, 1\}$: `\Bin`
\DeclareDocumentMacro \Bin {\mathbb{B}}

% - Identity relation: `\Id{X}`
\DeclareDocumentCommand \Id { m } {\mathord{\mathrm{Id}_{#1}}}

% Topological notions
% -------------------

% - `\Top{O}`: Open sets

\DeclareDocumentCommand \Top { m }{\mathcal{#1}}

% - `\Interior{V}`: the interior of $V$

\DeclareDocumentCommand \Interior { m }{\mathrm{Int}(#1)}

% ### Symbols for Turing Machines

% - `\TMendtape` - symbol indicating left end of tape
\DeclareDocumentMacro \TMendtape {\triangleright}

% - `\TMblank` - symbol for a blank
\DeclareDocumentMacro \TMblank {0}

% - `\TMstroke` - single stroke symbol on tape
\DeclareDocumentMacro \TMstroke {1}

% - `\TMright` - symbol for move right instruction
\DeclareDocumentMacro \TMright {R}

% - `\TMleft` - symbol for move left instruction
\DeclareDocumentMacro \TMleft {L}

% - `\TMstay` - symbol for the stay instruction
\DeclareDocumentMacro \TMstay {N}

% - `\TMtrans` - typeset a TM transition

\DeclareDocumentCommand \TMtrans { m m m } {\ensuremath{#1, #2, #3}}

% ### Functions and Function/Relation symbols

% - `\Part`: the parthood predicate 

\DeclareDocumentCommand \Part { m m } {\Atom{\Obj P}{#1, #2}}

% - `\Prf`: the proof relation

\DeclareDocumentCommand \Prf { o } { \mathrm{Prf}\IfNoValueTF {#1} {} {_{#1}}}
\DeclareDocumentCommand \OPrf { o } { \mathsf{Prf}\IfNoValueTF {#1} {} {_{#1}}}

% - `\Refut`: the refutation relation

\DeclareDocumentCommand \Refut { o } { \mathrm{Ref}\IfNoValueTF {#1} {} {_{#1}}}
\DeclareDocumentCommand \ORefut { o } { \mathsf{Ref}\IfNoValueTF {#1} {} {_{#1}}}

% - `\Prov`: the provability predicate

\DeclareDocumentCommand \Prov { o } { \mathrm{Prov}\IfNoValueTF {#1} {} {_{#1}}}
\DeclareDocumentCommand \OProv { o } { \mathsf{Prov}\IfNoValueTF {#1} {} {_{#1}}}

% - `\RProv`: the Rosser provability relation

\DeclareDocumentCommand \RProv { o } { \mathrm{RProv}\IfNoValueTF {#1} {} {_{#1}}}
\DeclareDocumentCommand \ORProv { o } { \mathsf{RProv}\IfNoValueTF {#1} {} {_{#1}}}

% - `\OCon`: the consistency statement

\DeclareDocumentCommand \OCon { o } { \mathsf{Con}\IfNoValueTF {#1} {} {_{#1}}}

% Typesetting commands for logical concepts
% =========================================

% In order to unformly typeset certain types of symbols uniformly, the
% OLP texts use special commands which carry out the
% typesetting. Thus, e.g., all structures, which appear in the texts,
% say, as `\Struct{M}`, can be typeset according to preference. By
% default, they are typeset in fraktur (e.g., $\mathfrak{M}$) but this
% can be configured by changing the definition of the `\Struct`
% command.  Note that often the default behavior is to only apply the
% typeface command to the first token in the argument, e.g., `\Struct
% M_n` will generate $\mathfrak M_n$ and not $\mathfrak{M_n}$.

% - `\Struct{M}` - First-order structures; by default, the first token
% in Fraktur

% - `\applytofirst` will apply #1 to #2 after expanding #2 once. We
%   use it to apply formatting to only the first token in the argument
%   so that, e.g., `\Struct{M_k}` produces $\mathfrak{M}_k$ and not
%   $\mathfrak{M_k }$.

\def\applytofirst#1#2{{\expandafter#1#2}}

\DeclareDocumentCommand \Struct { m }{\applytofirst{\mathfrak}{#1}}

% - `\Lang{L}` - Languages; default: set first token in callgraphic
% font

\DeclareDocumentCommand \Lang { m }{\applytofirst{\mathcal}{#1}}

% - `\Log{L}` - Logics; default: set entirely in boldface

\DeclareDocumentCommand \Log { m o }{\ensuremath{\mathbf{#1}
\IfNoValueTF {#2}{}{_{#2}}}}

% - We include names for some specific logics

\DeclareDocumentMacro {\LogCL} {\Log{C}}
\DeclareDocumentMacro {\LogIL} {\Log{I}}
\DeclareDocumentMacro {\LogLuk} {\Log{\textbf{\L}}}
\DeclareDocumentMacro {\LogGod} {\Log{G}}
\DeclareDocumentMacro {\LogKs} {\Log{Ks}}
\DeclareDocumentMacro {\LogKw} {\Log{Kw}}
\DeclareDocumentMacro {\LogLP} {\Log{LP}}
\DeclareDocumentMacro {\LogRM} {\Log{RM}}
\DeclareDocumentMacro {\LogHal} {\Log{Hal}}

% - `\Obj` - Object-language symbols; default: set entirely in
% sans-serif italics

\DeclareDocumentCommand \Obj { m }{\mathsfit{#1}}

%  - `\Atom{P}{t_1, t_2)` - Atomic formula or term; default produces
%  predicate symbol followed by arguments surrounded by
%  parentheses. Some prefer no parentheses around the arguments.

\DeclareDocumentCommand \Atom { m m }{ \mathord{#1}(#2) }

% - `\Ax{A}`: typeset an axiom

\DeclareDocumentCommand \Ax { m } {\ensuremath{\mathrm{#1}}}

% - `\PIso` - Set of all partial isomorphisms

\DeclareDocumentCommand \PIso { m }{\mathcal{#1}}

% - `\fn{func}` -- typeset a function name

\DeclareDocumentCommand \fn { m } {\mathrm{#1}}

% - `\Th{T}` -- typeset name of a theory

\DeclareDocumentCommand \Th { m } {\mathbf{#1}}

% Sets of Expressions
% ===================
%
% The following commands provide uniform notation for sets of
% expressions, such as the set of formulas of a language. Typically
% the parameter (language) can be providedas an optional argument.  By
% default, if the argument is given, they aretypeset following the
% symbol within parentheses, i.e., the symbols are treated as
% operators (e.g., $\mathrm{Frm}(\mathcal{L})$. Redefine the commands
% to, e.g., typeset the parameters as subscripts (e.g.,
% $\mathrm{Frm}_\mathcal{L}$.

% - `\Var`: the set of individual variables

\DeclareDocumentMacro \Var { \mathrm{Var} }

% - `\PVar`: the set of propositional variables

\DeclareDocumentMacro \PVar { \mathrm{At}_0 }

% - `\Trm[L]`: the set of terms (of a language)

\DeclareDocumentCommand \Trm { o } {
    \IfNoValueTF {#1} 
        { \mathrm{Trm} }
        { \mathrm{Trm}({\Lang #1}) }
}

% - `\Frm[L]`: the set of formulas (of a language)
\DeclareDocumentCommand \Frm { o } {
    \IfNoValueTF {#1} 
        { \mathrm{Frm} }
        { \mathrm{Frm}({\Lang #1}) }
}

% - `\Trm2[L]`: the set of second-order terms (of a language)

\DeclareDocumentCommand \TrmSOL { o } {
    \IfNoValueTF {#1} 
        { \mathrm{Trm}^2 }
        { \mathrm{Trm}^2({\Lang #1}) }
}

% - `\Frm2[L]`: the set of second-order formulas (of a language)
\DeclareDocumentCommand \FrmSOL { o } {
    \IfNoValueTF {#1} 
        { \mathrm{Frm}^2 }
        { \mathrm{Frm}^2({\Lang #1}) }
}

% - `\SubFrm{!A}`: the set of subformulas of a formula (mandatory
% argument: formula)

\DeclareDocumentCommand \SubFrm { m } {
        \mathrm{SFrm}({#1})
}

% - `\FV{!A}`: set of free variables of a formula or term

\DeclareDocumentCommand \FV { m } {
        \mathrm{FV}({#1})
}


% - `\Sent[L]`: the set of sentences (of a language)
\DeclareDocumentCommand \Sent { o } {
    \IfNoValueTF {#1} 
        { \mathrm{Sent} }
        { \mathrm{Sent}({\Lang{#1}}) }
}

% Additional set theory stuff
% ---------------------------
% From Tim Button's Open Set Theory

\DeclareDocumentMacro \unitline {\text{L}}
\DeclareDocumentMacro \unitsquare {\text{S}}
\newcommand{\onesphere}{\mathbf{S}}
\newcommand\rotationsgroup{R}

\DeclareDocumentCommand \cardneq { m m } {#1 \not\approx #2}
\DeclareDocumentCommand \cardnless { m m } {#1 \npreceq #2}
\DeclareDocumentCommand \ordeq { m m } {#1 \cong #2}
\DeclareDocumentCommand \ordneq { m m } {#1 \ncong #2}
\DeclareDocumentCommand \funimage { m m } {#1[#2]}

\newcommand\stageshier{\emph{Stages-are-key}}
\newcommand\stagesord{\emph{Stages-are-ordered}}
\newcommand\stagesacc{\emph{Stages-accumulate}}
\newcommand\stagessucc{\emph{Stages-keep-going}}
\newcommand\stagesinf{\emph{Stages-hit-infinity}}
\newcommand\limofsize{\emph{Limitation-of-size}}
\newcommand\stagesinex{\emph{Stages-are-inexhaustible}}
\newcommand\stagescofin{\emph{Stages-are-super-cofinal}}

\usetikzlibrary{lindenmayersystems}
\pgfdeclarelindenmayersystem{Hilbert curve}{
	\rule{L -> +RF-LFL-FR+}
	\rule{R -> -LF+RFR+FL-}}

\newcommand\closureofunder[2]{\mathrm{clo}_{#1}(#2)}
\newcommand\Closureofunder[2]{\mathrm{Clo}_{#1}(#2)}
\newcommand\equivrep[2]{[#1]_{#2}}
\newcommand\equivclass[2]{#1/_{\!{#2}}}
\newcommand\Intequiv{\sim}
\newcommand\Ratequiv{\backsim}
\newcommand\Realequiv{\Bumpeq}
\newcommand\funrestrictionto[2]{#1\mathord{\restriction}_{#2}}
\newcommand\isomorphic{\cong}
\newcommand\nisomorphic{\ncong}
\newcommand\precdot{\mathrel{\prec{\mkern -12mu \cdot}}}
\newcommand\disjointsum{\sqcup}
\newcommand\ordtype[1]{\mathrm{ord}(#1)}
\newcommand\ordsucc[1]{#1^{+}}
\newcommand\cardsucc[1]{#1^{\oplus}}
\newcommand\rlexless{\mathrel{\sphericalangle}}
\newcommand\canonord\lhd
\newcommand\ordplus{+}
\newcommand\ordtimes{\cdot}
\newcommand\ordexpo[2]{#1^{(#2)}}
\newcommand\cardplus{\oplus}
\newcommand\cardtimes{\otimes}
\newcommand\cardexpo[2]{#1^{#2}}
\newcommand\funfromto[2]{{}^{#1}{#2}}
\newcommand\setrank[1]{\mathrm{rank}(#1)}
\DeclareMathOperator*{\supstrict}{\mathrm{lsub}}
\DeclareMathOperator\lcm{\mathrm{lcm}}
\newcommand\trcl[1]{\mathrm{trcl}(#1)}
\newcommand\ZF{\Th{ZF}}
\newcommand\SP{\Th{SP}}
\newcommand\ZFC{\Th{ZFC}}
\newcommand\Z{\Th{Z}}
\newcommand\ZFminus{\ZF^{-}}
\newcommand\Zminus{\Z^{-}}
\newcommand\Zr{\Th{Zr}}
\newcommand\LT{\Th{LT}}

\newcommand\cardfont[1]{\mathfrak{#1}}

% Miscellaneous
% -------------

% `\fact` -- factorial function

\DeclareDocumentCommand \fact {m} {#1\,\mathexclaim}

% Commands for uniform formulations
% =================================

% Inductive definitions
% ---------------------

% Inductive definitions typically divide into cases depening on the
% form of a formula for which a concept if defined.  To uniformly
% typeset these definitions flexibly, we provide a command
% `\indcase{formula}{complex formula}{case text}` which (a) typesets a
% uniform description of a case and (b) defines `\indfrm` and
% `\indcomplex` which can then be used in the definitions. For
% instance, in an inductive definition of $\models A$, you might say
% `\indcase{A}{B \land C}{$\models \indfrm$ iff $\models B$ and
% $\models C$}` to produce: "If $A \equiv B \land C$, then $\models A$
% iff $\models B$ and $\models C$" or, alternatively and more
% succinctly: "$\models B \land C$ iff $\models B$ and $\models C$".
% Use the starred version for the atomic case, and a ! instead of the
% star for a case you want to leave as an exercise.

\DeclareDocumentCommand \indcase { s t{!} m m +m }{%
  \DeclareDocumentMacro \indfrm {#3}%
  \DeclareDocumentMacro \indfrmp {#3}%
  \DeclareDocumentMacro \indcomplex {#4}%
  \IfBooleanTF{#1}
     {$#3$ is atomic: }{$#3 \ident #4$: }
  \IfBooleanTF{#2}
     {exercise.}
     {#5}}

% Tokens
% ======

% The following terms are *tokenized* throughout OLP. This means that
% by changing the definition in the configuration file, the term as
% printed will also change. This is simpler than searching and
% replacing these terms in all OLP texts, and it will also treat
% plurals as well as occurrences of the term at the beginning of a
% sentence (where it should be capitalized) correctly.

% Tokens are defined using the `\settexttoken` command.
% ```
% \settexttoken{token}{singular}{plural}[Singular][Plural]
% ```
% Here `token` is the term as it is used in the source text, where it
% typically is used as `!!{token}`.  `singular` and `plural` are the
% text you want printed wherever an OLP text contains `!!{token}` or
% `!!{token}s`.  In sentence-initial position, OLP texts would use
% `!!^{token}` and `!!^{token}s` to create capitalized versions of
% these token replacements.  By default, they are generated from
% `singluar` and `plural` by capitalizing the first character, but can
% be provided explicitly to `\settexttoken` as optional arguments.
% `!!a{token}` produces an indefinite article plus the token
% replacement. This is usually "a" unless the settexttoken command is
% used with a star, as in `\settexttoken{element}*{element}{elements}`,
% in which case it produces "an". This can be combined with `^` to
% produce the uppercase version, e.g., `!!^a{element}` for "An
% element".  `\article{token}` and `\Article{token}` produce just the
% article by itself (lower or uppercase, respectively).

% - `language`: defaults to "language", redefine for, e.g.,
% "signature"

\settexttoken{language}{language}{languages}

% - `formula`: defaults to "formula/formulas", redefine for
% plural "formulae," or for "wff".

\settexttoken{formula}{formula}{formulas}

% - `subformula`: defaults to "subformula", redefine for plural
% "subformulae," hyphenated spelling "sub-formula", or "sub-wff".

\settexttoken{subformula}{subformula}{subformulas}

% - `sentence`: defaults to "sentence", redefine for
% "closed formula" etc.

\settexttoken{sentence}{sentence}{sentences}

% - `variable`: defaults to "variable/variables", redefine to be more
% specific, e.g., "individual variable", "object veriable".

\settexttoken{variable}{variable}{variables}

% - `propositional variable`: defaults to "propositional
% variable/variables", redefine for, e.g., "sentence
% letter"

\settexttoken{propositional variable}{propositional variable}{propositional variables}

% - `constant`: defaults to "constant", redefine for "individual
% constant", "constant symbol."

\settexttoken{constant}{constant symbol}{constant symbols}

% - `predicate`: defaults to "predicate symbol".

\settexttoken{predicate}{predicate symbol}{predicate symbols}

% - `function`: defaults to "function symbol".

\settexttoken{function}{function symbol}{function symbols}

% - `operator`: defaults to "logical operator", redefine for "connective".

\settexttoken{operator}{logical operator}{logical operators}

% - `main operator`: defaults to "main operator", redefine for
% "outermost operator".

\settexttoken{main operator}{main operator}{main operators}

% - `free for`: defaults to "free for", redefine for
% "substitutable for" as in Enderton.

\settexttoken{free for}{free for}{free for}

% - `identity`: defaults to "identity predicate", redefine for
% "equality predicate."

\settexttoken{identity}*{identity predicate}{identity predicates}

% - `conditional`: defaults to "conditional", redefine for
% "implication."

\settexttoken{conditional}{conditional}{conditionals}

% - `biconditional`: defaults to "biconditional", redefine for
% "equivalence."

\settexttoken{biconditional}{biconditional}{biconditionals}

% - `falsity`: name of the falsity symbol, defaults to "falsity",
% redefine for "absurdity."

\settexttoken{falsity}{falsity}{falsities}

% - `truth`: name of the truth symbol, defaults to "truth", redefine
% for "verum" or "top".

\settexttoken{truth}{truth}{truth}

% - `structure`: term for first-order structures, defaults to
% "structure", redefine for "interpretation", "model".

\settexttoken{structure}{structure}{structures}

% - `valuation`: valuation, truth-value assignment

\settexttoken{valuation}{valuation}{valuations}

% - `domain`: domain of a structure

\settexttoken{domain}{domain}{domains}

% - `value`: value (denotation) of a term

\settexttoken{value}{value}{values}

% - `relational model`: term for modal structures, defaults to
% "relational model", redefine for "Kripke model".

\settexttoken{relational model}{relational model}{relational models}

% - `derivation`: derivation in a calculus, proof

\settexttoken{derivation}{derivation}{derivations}

% - `derive`: derive in a calculus, prove

\settexttoken{derive}{derive}{derives}

% - `derivable`: derivable in a calculus, provable

\settexttoken{derivable}{derivable}{derivable}

% - `derivability`: derivability in a calculus, provability

\settexttoken{derivability}{derivability}{derivabilities}

% - `nonderivability`: derivability in a calculus, unprovability

\settexttoken{nonderivability}{non-derivability}{non-derivabilities}

% - `proof' and cognates: used in section on Proof Theory, mainly
% because writing "derivation" when seems wrong there. But defined
% as "derivation" for uniformity

\settexttoken{proof}{derivation}{derivations}
\settexttoken{prove}{derive}{derives}
\settexttoken{proving}{deriving}{deriving}
\settexttoken{provable}{derivable}{derivable}
\settexttoken{provability}{derivability}{derivabilities}
\settexttoken{nonprovability}{non-derivability}{non-derivabilities}

\settexttoken{introduction}*{introduction}{introductions}
\settexttoken{elimination}*{elimination}{elimination}

% - `tableau`: tableau, tableaux; or truth tree

\settexttoken{tableau}{tableau}{tableaux}

% - `signed formula`: signed formula in a tableau

\settexttoken{signed formula}{signed formula}{signed formulas}

% - `complete`: negation complete, syntactically complete (of theories)

\settexttoken{complete}{complete}{complete}

% - `axiomatizable`: effectively/recursively axiomatizable

\settexttoken{axiomatizable}*{axiomatizable}{axiomatizable}
\settexttoken{axiomatized}*{axiomatized}{axiomatized}
\settexttoken{axiomatizability}*{axiomatizability}{axiomatizability}

% - `represents`, `representable`

\settexttoken{represents}{represents}{represent}
\settexttoken{representable}{representable}{representable}

% - `discharge`: discharge an assumption in a natural deduction proof,
% cancel, close. Also: undischarged, non-cancelled, open.

\settexttoken{discharge}{discharge}{discharges}
\settexttoken{discharged}{discharged}{discharged}
\settexttoken{undischarged}*{undischarged}{undischarged}

% - `complete`: syntactic completeness of a set of sentences

\settexttoken{complete}{complete}{complete}

% - `enumerable`: term for finite or countably infinite; defaults to
% "enumerable", redefine for "countable".

\settexttoken{enumerable}*{enumerable}{enumerable}

% - `nonenumerable`: term for uncountable; defaults to
% "non-enumerable", redefine for "uncountable".

\settexttoken{nonenumerable}{non-enumerable}{non-enumerable}

% - `denumerable`: term for countably infinite; defaults to
% "denumerable".

\settexttoken{denumerable}{denumerable}{denumerable}

% - `element`: element of a set; redefine for "member"

\settexttoken{element}*{element}{elements}

% - `injective`, `injection`: redefine for "one-one" and "one-one
% function"

\settexttoken{injective}*{injective}{injective}
\settexttoken{injection}*{injection}{injections}

% - `surjective`, `surjection`: redefine for "onto" and "onto function"

\settexttoken{surjective}{surjective}{surjective}
\settexttoken{surjection}{surjection}{surjections}

% - `bijective`, `bijection`: redefine for "one-one onto" and "one-one
% onto function" or "correspondence"

\settexttoken{bijective}{bijective}{bijective}
\settexttoken{bijection}{bijection}{bijections}

% - `decidable`:

\settexttoken{decidable}{decidable}{decidable}

\settexttoken{computably enumerable}{computably enumerable}{computably enumerable}
\settexttoken{c.e.}{c.e.\@}{c.e.\@}

\settexttoken{argument}*{argument}{arguments}
\settexttoken{parameter}{parameter}{parameters}


% - `lambda define`: Also: represent.

\settexttoken{lambda define}{$\lambd$-define}{$\lambd$-defines}[$\lambd$-Define][$\lambd$-Defines]
\settexttoken{lambda defined}{$\lambd$-defined}{$\lambd$-defined}[$\lambd$-Defined]
\settexttoken{lambda definable}{$\lambd$-definable}{$\lambd$-definable}[$\lambd$-Definable]

% Tags
% ====

% Tags are used to guide selective compilation, using
% `sty/open-logic-selective.sty`.  Tags are initialized using
% `\tagtrue` and `\tagfalse`, which also initialize, for each `tag`
% given as argument, a corresponding tag `nottag` with opposite truth
% value.

% - `prvNot`, `prvOr`, `prvAnd`, `prvIf`, `prvIff`, `prvTrue`,
%   `prvFalse`, `prvEx`, `prvAll` - Primitives: tags for (sets of)
%   operators which are treated as primitives. Default: all as
%   primitives.

\tagtrue{prvNot,prvOr,prvAnd,prvIf,prvIff,prvTrue,prvFalse,prvEx,prvAll,prvBox,prvDiamond}

% - `defNot`, `defOr`, `defAnd`, `defIf`, `defIff`, `defTrue`,
%  `defFalse`, `defEx`, `defAll` - Defined operators: tags for
%  operators which are defined, not primitive. Default: none.  Note:
%  Not all combinations of primitive/defined operators will result in
%  complete definitions!

\tagfalse{defNot,defOr,defAnd,defIf,defIff,defTrue,defFalse,defEx,defAll,defBox,defDiamond}

% - `probNot`, `probOr`, `probAnd`, `probIf`, `probIff`, `probEx`,
%   `probAll` - Cases in proofs: tags for (sets of) operators for
%   which cases are proved; if the corresponding tag is on then the
%   case is added as a problem. Default: prove all cases. Note:
%   propositional constants are part of induction base case and are
%   always treated, if included.

\tagfalse{probNot,probOr,probAnd,probIf,probIff,probEx,probAll,probBox,probDiamond}

% - `limitclause` - Limit clause in inductive definitions: do you want
% inductive definitions to have a "Nothing else is a ..." clause?

\tagtrue{limitClause}

% - `tagTrue` - a true tag respectively.

\tagtrue{tagTrue}

% - `TMs` - Turing machines have been discussed

\tagtrue{TMs}

% - `lambda` - Lambda calculus has been discussed

\tagtrue{lambda}

% - prfND, prfSC, prfAX, prfTab - alternative coverage of proof systems. Set
% `prfND` to true if you want to include material on natural
% deduction, `prfSC` for the sequent calculus, `prfAX` for
% axiomatic deduction, `prfTab` for tableaux.  By default, we include all.

\tagtrue{prfSC}
\tagtrue{prfND}
\tagtrue{prfAX}
\tagtrue{prfTab}

% - `FOL` - if true, we produce text for FOL, otherwise for PL

\tagtrue{FOL}

% - `cmplCCS` - prove completeness via generating a complete
% consistent set
% - `cmplMCS` - prove completeness via maximally consistent sets

\tagtrue{cmplCCS}
\tagtrue{cmplMCS}

% - `novice` - for material aimed at novice readers with little math
%   background

\tagtrue{novice}

% - `math` - examples etc. for readers with a math background

\tagtrue{math}

% - `compsci` - examples etc. for readers with a CS background

\tagtrue{compsci}

% - `phil` - examples etc. for readers with a philosophy background

\tagtrue{phil}

% Colors
% ======

\colorlet{oldiagcolorA}{black}
\colorlet{oldiagcolorB}{gray}
\definecolor{oldiagcolorC}{HTML}{a81c21}
\definecolor{oldiagcolorD}{HTML}{1973ba}
\definecolor{oldiagcolorE}{HTML}{4d6f39}

\settexttoken{colorC}{red}{red}
\settexttoken{colorD}{blue}{blue}
\settexttoken{colorE}{green}{green}