\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 Predicate Logic: Proofs in K
\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)$
   \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$.
\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.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 Rule T:]  Any instance of a tautology may be inserted as a line in a predicate calculus proof.
   \item[\qquad Deduction Theorem:] If there is a proof of $A \vdash B$ with no applications of generalization to any variables that occur free in $A$,
                      then there is a proof of $\vdash A \to B$.
   \item[\qquad Add $\exists x$ Rule:] If $A(t)$ is the result of replacing every free occurrence of $x$ in $A(x)$ with $t$, and $t$ is free for $x$ in
                     $A(x)$, then from $A(t)$ we may deduce $\exists x A(x)$.
   \item[\qquad Rule C:] If $\exists x A(x)$ is a previous line in a proof, we may write $A ( \underline c )$ as a line, provided that
                    the following two conditions hold.
                    
                    \vspace{-0.15in}
                    
   \begin{enumerate}
      \item  $\underline c$ is a new constant symbol. 
      \item If some variable (say $y$) appears free in the formula $\exists x A(x)$, then GEN is never applied
                    to $y$ in the proof.
   \end{enumerate}
\end{description}

\noindent {\large \bf Abbreviations:}

\vspace{-0.1in}

\begin{description}
   \item[\qquad Existential Quantifier:] $\exists x A$ abbreviates $\neg \forall x \neg A$
   \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}

\newpage

\vspace*{1in}

\noindent {\large \bf Theorems:}

\vspace{-0.2in}

\begin{multicols}{2} 
\begin{description}
\item[K1:] $\vdash \forall x (A(x) \to (B(x) \to A(x)))$.
\item[K2:] $\forall x \forall y A(x,y) ~ \vdash ~ \forall y \forall x A(x,y)$.
\item[K3:] $A(x) \land B(x) ~ \vdash ~ A(x)$.
\item[K4:] $\vdash \forall x \forall y A(x,y) \to \forall y \forall x A(x,y)$
\item[K5:] $\vdash \forall x (A(x) \land B(x)) \to \forall x A(x)$
\item[K6:] $\vdash [ \forall x A(x) ] \to \forall x ( A(x) \lor B(x) )$
\item[K7:] $\vdash \forall x (A(x) \to B(x)) \to ( \forall x A(x) \to \forall x B(x) )$
\item[K8:] $\vdash \forall x B(x) \to \forall x (A(x) \to B(x))$
\item[K9:] $\vdash \forall x \forall y A(x,y) \to \forall y \forall x A(y,x)$
\item[K10:] $\vdash \forall x (A(x) \lor B(x)) \to ( \forall x \neg A(x) \to \forall x B(x))$
\item[K11:] $A(x) \vdash \exists x A(x)$
\item[K12:] $A(y,y) \vdash \forall y \exists x A(x,y)$
\item[K13:] $\vdash \forall x A(x) \to \exists x A(x)$
\item[K14:] $\vdash \forall y A(y) \to \exists x A(x)$
\item[K15:] $\vdash \forall x (A(x) \lor B(x)) \to [ \forall x A(x) \lor \exists x B(x) ]$
\item[K16:] $\neg \exists x A(x) \vdash  \forall x \neg A(x)$
\item[K17:] $\forall x \neg A(x) \vdash  \neg \exists x A(x)$
\item[K18:] $ \exists x \neg A(x) \vdash \neg \forall x A(x)$
\item[K19:] $ \neg \forall x A(x) \vdash \exists x \neg A(x)$
\item[K20:] $\exists x ( A(x) \land B(x) ) \vdash  \exists x A(x)$
\item[K21:] $\vdash \exists x A(x) \to \exists x (A(x) \lor B(x))$
\item[K22:] $\vdash \exists x \forall y A(x,y) \to \forall y \exists x A(x,y)$
\item[K23:] $\vdash \exists x (A(x) \to B(x)) \to ( \forall x A(x) \to  \exists x B(x))$
\item[K24:] $\vdash \exists x B(x) \to \exists x (A (x) \to B(x) )$
\item[K25:] $\vdash \neg \forall x A(x) \to \exists x ( A(x) \to B(x) )$
\item[K26:] $\vdash (\forall x A(x) \to \exists x B(x)) \to \exists x ( A(x) \to B(x))$
\item[K27:] $\vdash \forall x A(x,x) \to \forall x \exists y A(x,y)$
\item[K28:] $\vdash \forall y \exists x ( \neg A(y,x) \lor A(y,y) )$
\item[K29:] $\vdash \exists x (A(x) \lor B(x) ) \to (\exists x A(x) \lor \exists x B(x) )$
\item[K30:] $\vdash (\exists x A(x) \lor \exists x B(x) ) \to \exists x ( A(x) \lor B(x))$.
\item[K31:] $\vdash \exists x (A(x) \land B(x)) \to (\exists x A(x) \land \exists x B(x))$
\item[K32:] $\vdash (\forall x A(x) \land \exists x B(x) ) \to \exists x (A (x) \land B(x))$
\item[K33:] $\vdash (\forall x A(x) \lor \forall x B(x)) \to \forall x ( A(x) \lor B(x) )$
\item[K34:] $\vdash \forall x (A(x) \land B(x) ) \to (\forall x A(x) \land \forall x B(x) )$
\item[K35:] $\vdash (\forall x A(x) \land \forall x B(x) ) \to \forall x (A(x) \land B(x) )$
\item[K36:] $\vdash (\exists x A(x) \to \forall x B(x) ) \to \forall x (A (x) \to B(x) )$
\end{description}
\end{multicols}

\end{document}





