\documentclass[12pt]{article}
\usepackage{amsmath,amsfonts,amssymb,amsthm}

\usepackage{multicol}

\setlength{\oddsidemargin}{-0.5in}
\setlength{\evensidemargin}{-0.5in}
\setlength{\topmargin}{-0.5in}
\setlength{\headheight}{0.0in}
\setlength{\headsep}{0.0in}
\setlength{\topskip}{0.0in}
\setlength{\textheight}{9.5in}
\setlength{\textwidth}{7.5in}

\begin{document}

\newcommand{\limp}{\rightarrow}
\newcommand{\liff}{\leftrightarrow}

\pagestyle{empty}

\begin{center}
\Large \sc Formal Number Theory: Proofs in E and PA
\end{center}

\noindent {\large \bf Axioms:}

\vspace{-0.1in}

\begin{description} 
\setlength{\itemsep}{2pt}
   \item[\qquad Axiom 1:]  $A \to ( B \to A)$
   \item[\qquad Axiom 2:]  $(A \to (B \to C)) \to ((A \to B) \to (A \to C))$
   \item[\qquad Axiom 3:]  $( \neg B \to \neg A ) \to (( \neg B \to A ) \to B)$
   \item[\qquad Axiom 4:]  $( \forall x A(x) ) \to A(t)$, provided that $t$ is free for $x$ in $A(x)$.
   \item[\qquad Axiom 5:]  $ \forall x ( A \to B) \to (A \to \forall x B )$, provided that $x$ does not occur free in $A$.
   \item[\qquad Axiom 6:]  $\forall x (x=x)$.
   \item[\qquad Axiom 7:]  For every formula $\psi (x,y)$, with free variable $x$, if $y$ is free for $x$ in $\psi (x,x)$ then 

\vspace{-0.2in}

   \[ x=y \to (\psi (x,x) \to \psi (x,y) ). \]

\vspace{-0.1in}

   \item[\qquad Axiom 8:]  $\forall x \forall y (x=y \to x ^\prime = y ^\prime )$
   \item[\qquad Axiom 9:]  $\forall x (0 \neq x ^\prime )$
   \item[\qquad Axiom 10:]  $\forall x \forall y ( x ^\prime = y ^\prime \to x = y)$
   \item[\qquad Axiom 11:]  $\forall x (x + 0 = x)$
   \item[\qquad Axiom 12:]  $\forall x \forall y ( x + (y ^\prime ) = (x+y) ^\prime )$
   \item[\qquad Axiom 13:]  $\forall x ( x \cdot 0 = 0 )$
   \item[\qquad Axiom 14:]  $\forall x \forall y ( x \cdot (  y ^\prime ) = (x \cdot y) + x)$
   \item[\qquad Axiom 15:]  If $A(x)$ is a formula of $S$, then $A(0) \to (  \forall n (A(n) \to A (n ^\prime )) \to \forall n A(n))$
\end{description}

\noindent {\large \bf Rules of Inference:}

\vspace{-0.1in}

\begin{description}
   \item[\qquad Modus Ponens (MP):] From $A$ and $A \to B$ deduce $B$.
   \item[\qquad Generalization (GEN):] From $A$, deduce $\forall x A$.
\end{description}

\noindent {\large \bf Shortcuts:}

\vspace{0.05in}

\qquad The same shortcuts for L and K apply as well as abbreviations for $\lor$, $\land$, $\liff$, and $\exists$.

\vspace{0.2in}

\noindent {\large \bf Theorems:}

\vspace{-0.2in}

\begin{multicols}{2} 
\begin{description}
   \item[\qquad E1:] $\vdash_E \forall x \forall y (x = y \to y=x)$
   \item[\qquad E2:] $\vdash_E (x=y \to ( y=z \to x=z ))$
   \item[\qquad E3:] $\vdash_E (x=y \land x=z ) \to y=z$
   \item[\qquad E4:] $\vdash_E \forall x \forall y \forall z (y=x  \to ( z=x  \to y=z )$\\ 
   
   
   \item[\qquad PA1:] $\vdash_{PA} \forall n ( 0 \cdot n = 0 \to 0 \cdot (n ^\prime ) =0)$.
   \item[\qquad PA2:] $\vdash_{PA} \forall n ( 0 \cdot n = 0)$.
   \item[\qquad PA3:] $\vdash_{PA} \forall n ( n = 0 + n)$.
   \item[\qquad PA4:] $\vdash_{PA} \forall x \forall y ( x + y = y + x ) $
   \item[\qquad PA5:] $\vdash_{PA} \forall x \forall y ( x \cdot y = y \cdot x )$
\end{description}
\end{multicols}

\end{document}


