Quelle  root.tex

\documentclass[a4paper,enabledeprecatedfontcommands,abstract=on,twoside=true]{article}
\usepackage{isabelle,isabellesym}
\usepackage{url}
\usepackage{xr}
\usepackage[usenames]{color}
\usepackage{csquotes}
\usepackage{graphicx}
\usepackage{geometry}
\usepackage{epigraph}
\usepackage{tabularx}
\usepackage{array}
\usepackage[all]{nowidow}
\usepackage[stable]{footmisc}
\usepackage[ngerman,english]{babel}
\newcommand{\embeddedstyle}[1]{{\color{blue}#1}}
\newcommand{\bigbox}{}
\newcommand{\linelabel}[1]{}

\setcounter{secnumdepth}{2}
\setcounter{tocdepth}{1}

% 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{amsthm}

\usepackage{amsmath}

%\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}
\definecolor{linkcolor}{rgb}{0,0,0}
\definecolor{citecolor}{rgb}{0,0,0}
% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

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

\begin{document}

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


\begin{abstract}
We utilize and extend the method of \emph{shallow semantic embeddings} (SSEs) in classical higher-order logic (HOL) to construct a custom theorem proving environment
for \emph{abstract objects theory} (AOT) on the basis of Isabelle/HOL.

SSEs are a means for universal logical reasoning by translating a target logic to HOL using a representation of its semantics.
AOT is a foundational metaphysical theory, developed by Edward Zalta, that explains the objects presupposed by the sciences as \emph{abstract objects} that reify property patterns. In particular, AOT aspires to provide a philosphically grounded basis for the construction and analysis of the objects of mathematics.

We can support this claim by verifying Uri Nodelman's and Edward Zalta's reconstruction of Frege's theorem: we can confirm that the Dedekind-Peano postulates for natural numbers are consistently derivable in AOT using Frege's method. Furthermore, we can suggest and discuss generalizations and variants of the construction and can thereby provide theoretical insights into, and contribute to the philosophical justification of, the construction.

In the process, we can demonstrate that our method allows for a nearly transparent exchange of results between traditional pen-and-paper-based reasoning and the computerized implementation, which in turn can retain the automation mechanisms available for Isabelle/HOL.

During our work, we could significantly contribute to the evolution of our target theory itself, while simultaneously solving the technical challenge of using an SSE to implement a theory that is based on
logical foundations that significantly differ from the meta-logic HOL.

In general, our results demonstrate the fruitfulness of the practice of Computational Metaphysics, i.e. the application of computational methods to metaphysical questions and theories.

A full description of this formalization including references can be found at \url{http://dx.doi.org/10.17169/refubium-35141}.

The version of Principia Logico-Metaphysica (PLM) implemented in this formalization
can be found at \url{http://mally.stanford.edu/principia-2021-10-13.pdf}, while
the latest version of PLM is available at \url{http://mally.stanford.edu/principia.pdf}.
\end{abstract}

\cleardoublepage

\tableofcontents

\cleardoublepage

% generated text of all theories

\newgeometry{margin=1in}

\input{session}

\restoregeometry

\end{document}

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