\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym,amsmath,amssymb,a4wide}
\usepackage{graphicx,xcolor}

\newcommand{\imp}{\rightarrow}
\newcommand{\biimp}{\leftrightarrow}
\newcommand{\all}{\forall}
\newcommand{\ex}{\exists}
\newcommand{\seq}{\vdash}
\newcommand{\nec}{\Box} % necessarily
\newcommand{\pos}{\Diamond} % possibly
\newcommand{\ess}[2]{#1 \ \mathit{ess.} \ #2}
\newcommand{\NE}{\mathit{NE}}

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}


\begin{document}

\title{G\"odel's God in Isabelle/HOL}
\author{Christoph Benzm\"uller and Bruno Woltzenlogel Paleo}
%\date{November 1, 2013}
\maketitle

%\noindent\colorbox{gray}{\includegraphics[width=.99\textwidth]{$HOME/GoedelGod/Talks/FU-Berlin/ScottsScriptGrab}} %$

\begin{figure}[h]
\noindent\fcolorbox{gray}{white}{
\begin{minipage}{.96\textwidth}\small
\begin{itemize}
\item[A1] Either a property or its negation is positive, but not
  both:  \hfill 
  $\all \phi [P(\neg \phi) \biimp \neg P(\phi)]$ \\[-1.5em]
\item[A2] A property necessarily implied \\ by a
  positive property is positive: \phantom{b} \hfill 
  $\all \phi \all \psi [(P(\phi) \wedge \nec \all x [\phi(x)
  \imp \psi(x)]) \imp P(\psi)]$ \\[-1.5em]
\item[T1] Positive properties are possibly exemplified: \hfill $\all
  \phi [P(\phi) \imp \pos \ex x \phi(x)]$ \\[-1.5em]
\item[D1] A \emph{God-like} being possesses all positive properties: \hfill
  $G(x) \biimp \forall \phi [P(\phi) \to \phi(x)]$ \\[-1.5em]
\item[A3]  The property of being God-like is positive: \hfill   $P(G)$ \\[-1.5em]
\item[C\phantom{1}] Possibly, God exists: \hfill $\pos \ex x G(x)$ \\[-1.5em]
\item[A4]  Positive properties are necessarily positive: \hfill 
  $\all \phi [P(\phi) \to \Box \; P(\phi)]$ \\[-1.5em]
\item[D2] An \emph{essence} of an individual is a property possessed by it \\ and necessarily implying any of its properties: \\
  \phantom{b} \hfill $\ess{\phi}{x} \biimp \phi(x) \wedge \all
  \psi (\psi(x) \imp \nec \all y (\phi(y) \imp \psi(y)))$ \\[-1.5em]
\item[T2]  Being God-like is an essence of any
  God-like being: \hfill $\all x [G(x) \imp \ess{G}{x}]$ \\[-1.5em]
\item[D3] \emph{Necessary existence} of an individual is \\ the necessary exemplification of all its essences: 
  \phantom{b} \hfill $\NE(x) \biimp \all \phi [\ess{\phi}{x} \imp \nec
  \ex y \phi(y)]$ \\[-1.5em]
\item[A5] Necessary existence is a positive property: \hfill $P(\NE)$ \\[-1.5em]
\item[T3] Necessarily, God exists: \hfill $\nec \ex x G(x)$ 
\end{itemize}
\end{minipage}
}
\caption{Scott's version of G\"odel's ontological argument \cite{ScottNotes}.} 
\end{figure}
\vskip1em

%\tableofcontents

% sane default for proof documents
\parindent 0pt\parskip 0.5ex

% generated text of all theories
\input{session}

\paragraph{Acknowledgments:} Nik Sultana, Jasmin Blanchette and Larry Paulson provided 
very important help on issues related to consistency checking in Isabelle. Jasmin Blanchette instructed us on 
producing Isabelle sessions and he showed us some useful tricks in Isabelle.

\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
