-
Notifications
You must be signed in to change notification settings - Fork 2
/
ic-config.sty
41 lines (23 loc) · 1.07 KB
/
ic-config.sty
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
% Configuration file for Logic II textbook
% Let's be unpretentious and use A, B, C, etc. for formulas ...
\ollatinformulas
% ... and use bold italic instead of Fraktur for structures
\DeclareMathAlphabet{\mathbi}{OT1}{pplx}{b}{it}
\DeclareDocumentCommand \Struct { m }{\applytofirst{\mathbi}{#1}}
% - `\TMblank` - symbol for a blank
\DeclareDocumentMacro \TMblank {\sqcup}
% - `\TMstroke` - single stroke symbol on tape
\DeclareDocumentMacro \TMstroke {I}
% 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}
% Which proof system? Not sure yet, let's use natural deduction for
% now. prfND is on by default, we just have to supress includion of
% the sequent calculus.
\tagfalse{prfSC,prfAX,prfTab}