attachment:PresburgerAxioms.tex of PresburgerArithmetic

   1 \documentclass{article}
   2 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   3 \usepackage{geometry}
   4 
   5 %TCIDATA{OutputFilter=LATEX.DLL}
   6 %TCIDATA{Version=5.00.0.2552}
   7 %TCIDATA{<META NAME="SaveForMode" CONTENT="1">}
   8 %TCIDATA{Created=Thursday, June 16, 2005 10:14:00}
   9 %TCIDATA{LastRevised=Thursday, June 16, 2005 10:49:33}
  10 %TCIDATA{<META NAME="GraphicsSave" CONTENT="32">}
  11 %TCIDATA{<META NAME="DocumentShell" CONTENT="Standard LaTeX\Blank - Standard LaTeX Article">}
  12 %TCIDATA{CSTFile=40 LaTeX article.cst}
  13 
  14 \newtheorem{theorem}{Theorem}
  15 \newtheorem{acknowledgement}[theorem]{Acknowledgement}
  16 \newtheorem{algorithm}[theorem]{Algorithm}
  17 \newtheorem{axiom}[theorem]{Axiom}
  18 \newtheorem{case}[theorem]{Case}
  19 \newtheorem{claim}[theorem]{Claim}
  20 \newtheorem{conclusion}[theorem]{Conclusion}
  21 \newtheorem{condition}[theorem]{Condition}
  22 \newtheorem{conjecture}[theorem]{Conjecture}
  23 \newtheorem{corollary}[theorem]{Corollary}
  24 \newtheorem{criterion}[theorem]{Criterion}
  25 \newtheorem{definition}[theorem]{Definition}
  26 \newtheorem{example}[theorem]{Example}
  27 \newtheorem{exercise}[theorem]{Exercise}
  28 \newtheorem{lemma}[theorem]{Lemma}
  29 \newtheorem{notation}[theorem]{Notation}
  30 \newtheorem{problem}[theorem]{Problem}
  31 \newtheorem{proposition}[theorem]{Proposition}
  32 \newtheorem{remark}[theorem]{Remark}
  33 \newtheorem{solution}[theorem]{Solution}
  34 \newtheorem{summary}[theorem]{Summary}
  35 \newenvironment{proof}[1][Proof]{\noindent\textbf{#1.} }{\ \rule{0.5em}{0.5em}}
  36 \input{tcilatex}
  37 \geometry{left=1in,right=1in,top=1in,bottom=1in}
  38 \begin{document}
  39 
  40 
  41 \section{Presburger Arithmetic: Formal Theory Description}
  42 
  43 \begin{enumerate}
  44 \item $\forall x:\lnot (0=x+1)$
  45 
  46 \item $\forall x\forall y:\lnot (x=y)\Rightarrow \lnot (x+1=y+1)$
  47 
  48 \item $\forall x:x+0=x$
  49 
  50 \item $\forall x\forall y:(x+y)+1=x+(y+1)$
  51 
  52 \item If $P(x)$ is any formula involving the constants $0,1,+,=$ and a
  53 single free variable $x$, then the following formula is an axiom:%
  54 \[
  55 (P(0)\wedge \forall x:P(x)\Rightarrow P(x+1))\Rightarrow \forall x:P(x) 
  56 \]
  57 \end{enumerate}
  58 
  59 Not that such concepts as divisibility of prime numbers cannot be formalized
  60 in Presburger arithmetic. Here is a typical theorem that can be proven from
  61 the above axioms:%
  62 \[
  63 \forall x\forall y:((\exists z:x+z=y+11)\Rightarrow (\forall z:\lnot
  64 (((1+y)+1)+z=x))) 
  65 \]
  66 
  67 \end{document}