\documentclass{article}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{geometry}

%TCIDATA{OutputFilter=LATEX.DLL}
%TCIDATA{Version=5.00.0.2552}
%TCIDATA{<META NAME="SaveForMode" CONTENT="1">}
%TCIDATA{Created=Thursday, June 16, 2005 10:14:00}
%TCIDATA{LastRevised=Thursday, June 16, 2005 10:49:33}
%TCIDATA{<META NAME="GraphicsSave" CONTENT="32">}
%TCIDATA{<META NAME="DocumentShell" CONTENT="Standard LaTeX\Blank - Standard LaTeX Article">}
%TCIDATA{CSTFile=40 LaTeX article.cst}

\newtheorem{theorem}{Theorem}
\newtheorem{acknowledgement}[theorem]{Acknowledgement}
\newtheorem{algorithm}[theorem]{Algorithm}
\newtheorem{axiom}[theorem]{Axiom}
\newtheorem{case}[theorem]{Case}
\newtheorem{claim}[theorem]{Claim}
\newtheorem{conclusion}[theorem]{Conclusion}
\newtheorem{condition}[theorem]{Condition}
\newtheorem{conjecture}[theorem]{Conjecture}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{criterion}[theorem]{Criterion}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{example}[theorem]{Example}
\newtheorem{exercise}[theorem]{Exercise}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{notation}[theorem]{Notation}
\newtheorem{problem}[theorem]{Problem}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{remark}[theorem]{Remark}
\newtheorem{solution}[theorem]{Solution}
\newtheorem{summary}[theorem]{Summary}
\newenvironment{proof}[1][Proof]{\noindent\textbf{#1.} }{\ \rule{0.5em}{0.5em}}
\input{tcilatex}
\geometry{left=1in,right=1in,top=1in,bottom=1in}
\begin{document}


\section{Presburger Arithmetic: Formal Theory Description}

\begin{enumerate}
\item $\forall x:\lnot (0=x+1)$

\item $\forall x\forall y:\lnot (x=y)\Rightarrow \lnot (x+1=y+1)$

\item $\forall x:x+0=x$

\item $\forall x\forall y:(x+y)+1=x+(y+1)$

\item If $P(x)$ is any formula involving the constants $0,1,+,=$ and a
single free variable $x$, then the following formula is an axiom:%
\[
(P(0)\wedge \forall x:P(x)\Rightarrow P(x+1))\Rightarrow \forall x:P(x) 
\]
\end{enumerate}

Not that such concepts as divisibility of prime numbers cannot be formalized
in Presburger arithmetic. Here is a typical theorem that can be proven from
the above axioms:%
\[
\forall x\forall y:((\exists z:x+z=y+11)\Rightarrow (\forall z:\lnot
(((1+y)+1)+z=x))) 
\]

\end{document}