-
Notifications
You must be signed in to change notification settings - Fork 0
/
mylogic.sty
109 lines (91 loc) · 3.29 KB
/
mylogic.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
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
\newcommand{\horizontalrule}{\noindent \rule{\linewidth}{0.5pt}}
% theorem environments
% \newtheorem{theorem}{Theorem}[section]
% \newtheorem{lemma}[theorem]{Lemma}
% \newtheorem{proposition}[theorem]{Proposition}
% \newtheorem{definition}[theorem]{Definition}
% \newtheorem{corollary}[theorem]{Corollary}
% special fonts for theory names, functions, axioms, etc.
\newcommand{\fn}[1]{\mathit{#1}} % function; e.g. successor
\newcommand{\mdl}[1]{\frak{#1}} % model; e.g. M
% logical connectives
\newcommand{\liff}{\leftrightarrow}
\newcommand{\ex}[1]{\exists #1 \;} % exists x ...
\newcommand{\fa}[1]{\forall #1 \;} % forall x ...
\newcommand{\lam}[1]{\lambda #1 \;} % forall x ...
\newcommand{\exunique}[1]{\exists ! #1 \;}
% useful symbols
\newcommand{\proves}{\vdash}
\newcommand{\nproves}{\nvdash}
\newcommand{\forces}{\Vdash}
\newcommand{\nforces}{\nVdash}
\newcommand{\ph}{\varphi}
\newcommand{\st}{\mid} % x such that ...
\newcommand{\dash}{\mathord{\mbox{-}}}
\newcommand{\inv}{^{-1}}
% useful abbreviations
\newcommand{\NN}{\mathbb{N}}
\newcommand{\ZZ}{\mathbb{Z}}
\newcommand{\QQ}{\mathbb{Q}}
\newcommand{\RR}{\mathbb{R}}
\newcommand{\CC}{\mathbb{C}}
\newcommand{\lqt}{\mbox{`}}
\newcommand{\rqt}{\mbox{'}}
\newcommand{\true}{\mathbf{T}}
\newcommand{\false}{\mathbf{F}}
\newcommand{\MM}{\mathcal{M}}
% BussProofs abbreviations
\newcommand{\AXM}[1]{\AXC{$#1$}}
\newcommand{\UIM}[1]{\UIC{$#1$}}
\newcommand{\BIM}[1]{\BIC{$#1$}}
\newcommand{\TIM}[1]{\TIC{$#1$}}
\newcommand{\AXN}[1]{\AX$#1$}
\newcommand{\BIN}[1]{\BI$#1$}
\newcommand{\UIN}[1]{\UI$#1$}
\newcommand{\TIN}[1]{\TI$#1$}
% \newcommand{\RLM}[1]{\RL{$\mathrm{#1}$}}
\newcommand{\RLM}[1]{\RL{$\scriptstyle #1$}}
% common predicates and relations
\newcommand{\even}{\ensuremath{\fn{even}}}
\newcommand{\odd}{\ensuremath{\fn{odd}}}
\newcommand{\primep}{\ensuremath{\fn{prime}}}
\newcommand{\suc}{\ensuremath{\fn{succ}}}
\newcommand{\tsub}{\mathbin{\mathchoice% truncated subtraction
{\buildrel .\lower.6ex\hbox{\vphantom{.}} \over {\smash-}}%
{\buildrel .\lower.6ex\hbox{\vphantom{.}} \over {\smash-}}%
{\buildrel .\lower.4ex\hbox{\vphantom{.}} \over {\smash-}}%
{\buildrel .\lower.3ex\hbox{\vphantom{.}} \over {\smash-}}}}
\EnableBpAbbreviations
%\newcommand{\FGrp}{F_{\mathbf{Grp}}}
\newcommand{\Sg}{\mathsf{Sg}}
\newcommand{\Hom}{\mathsf{Hom}}
\newcommand{\epi}{\mathsf{Epi}}
\newcommand{\aut}{\mathsf{Aut}}
\newcommand{\mono}{\mathsf{Mono}}
\newcommand{\Af}{\langle A, f \rangle}
\newcommand{\dom}{\mathsf{dom}}
\newcommand{\cod}{\mathsf{cod}}
\newcommand{\ran}{\mathsf{ran}}
\newcommand{\id}{\mathsf{id}}
\newcommand{\Id}{\mathsf{id}}
\newcommand{\im}{\mathrm{im}}
\newcommand{\Proj}{\mathsf{pr}}
\newcommand{\Con}{\mathsf{Con}}
\newcommand{\Clo}{\mathsf{Clo}}
\newcommand{\Pol}{\mathsf{Pol}}
\newcommand{\Op}{\mathsf{Op}}
\newcommand{\Th}{\mathsf{Th}}
\newcommand{\Mod}{\mathsf{Mod}}
\newcommand{\src}{\mathsf{src}}
\newcommand{\tar}{\mathsf{tar}}
\newcommand{\eval}{\mathsf{eval}}
\newcommand{\fork}{\mathsf{fork}}
\newcommand{\Type}{\mathsf{Type}}
\newcommand{\comp}{\circ}
% \providecommand{\FGrp}{\operatorname{F}_{\mathbf{Grp}}}
% \newcommand\epi{\operatorname{Epi}}
% \renewcommand\hom{\operatorname{Hom}}
% \newcommand{\Sg}{\mathsf{Sg}}
% \newcommand\aut{\operatorname{Aut}}
% \newcommand\mono{\operatorname{Mono}}
%% \newcommand\Af{\ensuremath{\langle A, f \rangle}}