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

% 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 $1$ and `\False` to $0$.

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

% ### 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), use the following line.

% `\DeclareDocumentMacro \lnot {\mathord{\sim}}`

% - Conjunction is `\land` and deaults to $\land$.  to use ampersand,
% uncomment the following line

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

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

\DeclareDocumentMacro \cif {\boxright}

% - The strict conditional `\strictif`

\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 { o o } {
    \IfNoValueTF {#1} 
        { \exists }    % no arguments
        { \exists #1 } % one argument: variable
    \IfNoValueTF {#2} 
        \relax
        { \, #2 }      % 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}

% The sequent symbol in proofs displays as the above sequent symbol.

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

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

\DeclareDocumentMacro \Weakening {\text{W}}

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

\DeclareDocumentMacro \Contraction {\text{C}}

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

\DeclareDocumentMacro \Exchange {\text{X}}

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

\DeclareDocumentMacro \Cut {\text{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 } {\ensuremath{{#1}\mathrm{Intro}}}

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

% - `\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., $[!A]^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}} #2}}

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

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

% Tableaux
% --------

% - Tableau rule names: `\TRule{Sign}{Op}` typesets the name of a the
% 'Sign' rule for operator `Op`, `\TFalse{Op}` does the same for
% 'False' rules. 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}]}


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

% - `\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 } {\mathfrak #1}

% - `\pValue{v}{A}` - Truth value of a formula under a truth-value assignment.

\DeclareDocumentCommand \pValue { m m }{\overline{\pAssign{#1}}(#2)}

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

\DeclareDocumentCommand \pSat { t{/} m m } {
  \IfBooleanTF{#1}{
    % negated
        \pAssign #2 \nvDash #3}{
    % not negated
        \pAssign #2 \vDash #3}
}

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

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

% - `\redone`: one-step reduction

\DeclareDocumentMacro \redone {\mathrel{\triangleright_1}}

% - `\red`: reduction

\DeclareDocumentMacro \red {\triangleright}

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

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

% - `\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\"odel number of a string of symbols

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

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

% Modal logic
% ===========

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

\DeclareDocumentCommand \mModel { m }{\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{\phantom{\lnot}#1}}
\DeclareDocumentCommand \mFalse { m }{\ensuremath{\lnot #1}}

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

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

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

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

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

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

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

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

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

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

\DeclareDocumentCommand \Log { m }{\ensuremath{\mathbf{#1}}}

% - `\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 argumnets 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})
}

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



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

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

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