% 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{\na}[1]{\mathit{#1}}    % theory; e.g. WKL_0
\newcommand{\fn}[1]{\mathit{#1}}    % function; e.g. successor
\newcommand{\ax}[1]{\mathit{(#1)}}  % axiom; e.g. (WKL)
\newcommand{\mdl}[1]{\mathcal{#1}}  % model; e.g. M

% text markers
\newcommand{\proof}{\noindent {\em Proof.}\ }
\newcommand{\proofarg}[1]{\noindent {\em Proof #1.}\ }
\newcommand{\proofend}{\hfill \mbox{$\square$} \bigskip}
\newcommand{\proofxend}{\hfill \mbox{$\square$}}    % don't skip a line

% logical connectives
\newcommand{\limplies}{\rightarrow}
\newcommand{\lfollows}{\rightarrow}
\newcommand{\liff}{\leftrightarrow}
\newcommand{\ex}[1]{\exists #1 \;} % exists x ...
\newcommand{\fa}[1]{\forall #1 \;} % forall x ...
\newcommand{\lImplies}{\Rightarrow}
\newcommand{\lFollows}{\Leftarrow}
\newcommand{\lIff}{\Longleftrightarrow}

\newcommand{\inot}{\mathord{\sim}}
\newcommand{\lam}[1]{\lambda #1 \;} % lambda x ...

% useful symbols
\newcommand{\proves}{\vdash}
\newcommand{\forces}{\Vdash}
\newcommand{\nforces}{\nVdash}

\newcommand{\dash}{\mathalpha{\mbox{-}}} % e.g. for Sigma^1_1-AC
\newcommand{\goedel}[1]{\ulcorner #1 \urcorner}
\newcommand{\gn}[1]{\ulcorner #1 \urcorner}

\newcommand{\la}{\langle}
\newcommand{\ra}{\rangle}
\newcommand{\half}{\frac{1}{2}}
\newcommand{\st}{ \; | \; } % x such that ...
\newcommand{\res}{\mathord{\upharpoonright}}
\newcommand{\concat}{\mathord{\hat{\;}}}

\newcommand{\eqdef}{=_{\rm def}}
\newcommand{\equivdef}{\equiv_{\rm def}}

% complexity classes 
\newcommand{\lsig}[2]{\Sigma^{#1}_{#2}}
\newcommand{\lpi}[2]{\Pi^{#1}_{#2}}
\newcommand{\ldelta}[2]{\Delta^{#1}_{#2}}

% other useful symbols
\newcommand{\moprec}{\mathord{\prec}}
\newcommand{\mopreceq}{\mathord{\preceq}}
\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-}}}}

% useful abbreviations
\newcommand{\nf}[1]{{\overline{#1}}} % normal form
\newcommand{\ph}{\varphi}
\newcommand{\N}{\mathbb{N}}
\newcommand{\red}{\rightsquigarrow_1}
\newcommand{\tval}[1]{[\![#1]\!]}

% miscellany
\newcommand{\sigac}{\Sigma^1_1\dash AC}

% margin notes
% \newcommand{\note}[1]{\begin{marginpar}{\small \em \raggedright
%        $\Longleftarrow$ #1} \end{marginpar}}

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

% Other symbols
\newcommand{\slasho}{\symbol{"1C}}
\newcommand{\dotlessi}{\symbol{"10}}