\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{authblk}
%\usepackage{a4wide}
\usepackage{isabelle,isabellesym}

% further packages required for unusual symbols (see also
% isabellesym.sty), use only when needed

\usepackage{amssymb}
  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
  %\<triangleq>, \<yen>, \<lozenge>

%\usepackage{eurosym}
  %for \<euro>

%\usepackage[only,bigsqcap]{stmaryrd}
  %for \<Sqinter>

%\usepackage{eufrak}
  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)

%\usepackage{textcomp}
  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
  %\<currency>

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

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

% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}


\begin{document}

\title{Types, Tableaus and G\"odel's God \\ in Isabelle/HOL}
%\author{David Fuenmayor, Christoph Benzm\"uller}
\author[1]{David Fuenmayor}
\author[2,1]{Christoph Benzm\"uller}
\affil[1]{Freie Universit\"at Berlin, Germany}
\affil[2]{University of Luxembourg, Luxembourg}

\maketitle

\begin{abstract}
	A computer-formalisation of the essential parts of Fitting's textbook
	\emph{Types, Tableaus and G\"odel's Go}d in Isabelle/HOL is
	presented. In particular, Fitting's (and Anderson's) variant of the ontological
	argument is verified and confirmed. This variant avoids the modal
	collapse, which has been criticised as an undesirable side-effect of Kurt G\"odel's (and
	Dana Scott's) versions of the ontological argument. Fitting's work
	is employing an intensional higher-order modal logic, which we
	shallowly embed here in classical higher-order logic. We then
	utilize the embedded logic for the formalisation of Fitting's argument.
\end{abstract}

\tableofcontents

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


\pagebreak 
% generated text of all theories
\input{session}

% optional bibliography
\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

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