wi-config.sty

% Configuration file for Logic II textbook

% Let's be unpretentious and use A, B, C, etc. for formulas ...

\ollatinformulas

% use the complex formula in induction cases rather

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

\DeclareDocumentCommand \Struct { m }{\applytofirst{\mathbf}{#1}}
\DeclareDocumentCommand \mModel { m }{\applytofirst{\mathbf}{#1}}
\DeclareDocumentCommand \pAssign { m }{\applytofirst{\mathbf}{#1}}

\DeclareDocumentMacro {\LogLuk} {\Log{\textbf{\textit{\L}}}}

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

% I think I like ``countable'' and ``uncountable'' better?

\settexttoken{enumerable}{countable}{countable}

\settexttoken{nonenumerable}*{uncountable}{uncountable}

\settexttoken{denumerable}{countably infinite}{countably infinite}

% Biconditional, verum are defined symbols

\tagtrue{defIff,defTrue}
\tagfalse{prvIff,prvTrue}

% I'll leave cases for conditional, universal quantifier as exercises

\tagtrue{probAnd,probIf,probAll,probDiamond}

% Which proof system?  We'll need axiomatic deduction and tableaux

\tagfalse{prfSC,prfND}

\tikzset{
   sphere/.style = {dotted,thick},
   proposition/.style={thick,smooth,tension=1.7}
}