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

\usepackage{multicol}

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

\begin{document}

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

\pagestyle{empty}

\begin{center}
\Large \sc Propositional Logic: Proofs in L
\end{center}

\noindent {\large \bf Axioms:}

\vspace{-0.1in}

\begin{description} 
   \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)$
\end{description}

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

\vspace{-0.1in}

\begin{description}
   \item[\qquad Modus Ponens:] If $A$ and $A \to B$ are lines in a proof, we can write $B$ as a
(later) line.  Here $A$ and $B$ can represent any formulas.
\end{description}

\noindent {\large \bf Shortcuts:}

\vspace{-0.1in}

\begin{description}
   \item[\qquad Lemmas:] You may write an instance of a previously proved (lowed numbered) theorem as a line, if the
   instances of the ``givens'' of that theorem appear as earlier lines.
   \item[\qquad Deduction Theorem:] Instead of proving $G_1,\dots,G_\ell \vdash A \to B$, prove $G_1,\dots,G_\ell,A \vdash B$.
\end{description}

\noindent {\large \bf Abbreviations:}

\vspace{-0.1in}

\begin{description}
\item[\qquad Conjunction:]  $A \land B$ abbreviates $\neg (A \to \neg B )$
\item[\qquad Disjunction:]    $A \lor B$ abbreviates $(\neg A) \to B$
\item[\qquad Double Implication:] $A \liff B$ abbreviates $\neg((A \to B) \to \neg ( B \to A ))$ \\
   {\it Note:} When $A \liff B$ and $(A \to B) \land (B \to A)$ are unabbreviated, they are identical.
\end{description}

\vspace{0.1in}

\noindent {\large \bf Theorems:}

\vspace{-0.2in}

\begin{multicols}{2} 
\begin{description}
   \item[L1:]  $\vdash_L A \to A$
   \item[L2:]  $\vdash_L ( \neg B \to B ) \to B$
   \item[L3:]  $ A \to ( B \to C),~ A \to B \vdash_L A \to C$
   \item[L4:]  $A \to ((B \to A) \to C) \vdash_L A \to C$
   \item[L5:]  $B \vdash_L A \to B$
   \item[L6:]  $A \to (B \to C) , ~ B \vdash_L A \to C$
   \item[L7:]  $A \to (B \to C) \vdash_L B \to (A \to C)$
   \item[L8:]  $A \to B , ~ B \to C \vdash_L A \to C$
   \item[L9:]  $P \to R \vdash_L P \to (Q \to R )$
   \item[L10:] $\vdash_L ( \neg B \to \neg A ) \to (A \to B)$
   \item[L11:] $\vdash_L \neg \neg B \to B$
   \item[L12:] $\vdash_L B \to \neg \neg B$
   \item[L13:] $\vdash_L (A \to (B \to C)) \to (B \to (A \to C))$
   \item[L14:] $\vdash_L A \to ((A \to B) \to B)$
   \item[L15:] $\vdash_L \neg A \to (A \to B)$
   \item[L16:] $\vdash_L (A \to B) \to ( \neg B \to \neg A )$
   \item[L17:] $\vdash_L A \to ( \neg B \to \neg (A \to B))$
   \item[L18:] $A, ~ B \vdash_L A \land B$
   \item[L19:] $A \land B \vdash_L  A$
   \item[L20:] $A \land B \vdash_L   B$
   \item[L21:] $A\vdash_L A \lor B$
   \item[L22:] $B \vdash_L A \lor B$
   \item[L23:] $A \liff B \vdash_L A \to B$
   \item[L24:] $A \liff B \vdash_L B \to A$
   \item[L25:] $A \to B ,B \to A \vdash_L A \liff B$
\end{description}
\end{multicols}

\end{document}
