diff --git a/thys/GoedelGod/GoedelGod.thy b/thys/GoedelGod/GoedelGod.thy
--- a/thys/GoedelGod/GoedelGod.thy
+++ b/thys/GoedelGod/GoedelGod.thy
@@ -1,208 +1,208 @@
(*<*)
theory GoedelGod
imports Main
begin
(*>*)
section \Introduction\
- text \Dana Scott's version \<^cite>\"ScottNotes"\ (cf.~Fig.~1)
- of G\"odel's proof of God's existence \<^cite>\"GoedelNotes"\ is
+ text \Dana Scott's version \cite{ScottNotes} (cf.~Fig.~1)
+ of G\"odel's proof of God's existence \cite{GoedelNotes} is
formalized in quantified modal logic KB (QML KB) within the proof assistant Isabelle/HOL.
QML KB is modeled as a fragment of classical higher-order logic (HOL);
thus, the formalization is essentially a formalization in HOL. The employed embedding
- of QML KB in HOL is adapting the work of Benzm\"uller and Paulson \<^cite>\"J23" and "B9"\.
+ of QML KB in HOL is adapting the work of Benzm\"uller and Paulson \cite{J23,B9}.
Note that the QML KB formalization employs quantification over individuals and
quantification over sets of individuals (properties).
The gaps in Scott's proof have been automated
- with Sledgehammer \<^cite>\"Sledgehammer"\, performing remote calls to the higher-order automated
- theorem prover LEO-II \<^cite>\"LEO-II"\. Sledgehammer suggests the
- Metis \<^cite>\"Metis"\ calls, which result in proofs that are verified by Isabelle/HOL.
- For consistency checking, the model finder Nitpick \<^cite>\"Nitpick"\ has been employed.
+ with Sledgehammer \cite{Sledgehammer}, performing remote calls to the higher-order automated
+ theorem prover LEO-II \cite{LEO-II}. Sledgehammer suggests the
+ Metis \cite{Metis} calls, which result in proofs that are verified by Isabelle/HOL.
+ For consistency checking, the model finder Nitpick \cite{Nitpick} has been employed.
The successfull calls to Sledgehammer
are deliberately kept as comments in the file for demonstration purposes
(normally, they are automatically eliminated by Isabelle/HOL).
Isabelle is described in the textbook by Nipkow,
- Paulson, and Wenzel \<^cite>\"Isabelle"\ and in tutorials available
+ Paulson, and Wenzel \cite{Isabelle} and in tutorials available
at: @{url "http://isabelle.in.tum.de"}.
\subsection{Related Work}
- The formalization presented here is related to the THF \<^cite>\"J22"\ and
- Coq \<^cite>\"Coq"\ formalizations at
+ The formalization presented here is related to the THF \cite{J22} and
+ Coq \cite{Coq} formalizations at
@{url "https://github.com/FormalTheology/GoedelGod/tree/master/Formalizations/"}.
- An older ontological argument by Anselm was formalized in PVS by John Rushby \<^cite>\"rushby"\.
+ An older ontological argument by Anselm was formalized in PVS by John Rushby \cite{rushby}.
\
section \An Embedding of QML KB in HOL\
text \The types \i\ for possible worlds and $\mu$ for individuals are introduced.\
typedecl i \ \the type for possible worlds\
typedecl \ \ \the type for indiviuals\
text \Possible worlds are connected by an accessibility relation \r\.\
consts r :: "i \ i \ bool" (infixr "r" 70) \ \accessibility relation r\
text \QML formulas are translated as HOL terms of type @{typ "i \ bool"}.
This type is abbreviated as \\\.\
type_synonym \ = "(i \ bool)"
text \The classical connectives $\neg, \wedge, \rightarrow$, and $\forall$
(over individuals and over sets of individuals) and $\exists$ (over individuals) are
lifted to type $\sigma$. The lifted connectives are \m\\, \m\\, \m\\,
\\\, and \\\ (the latter two are modeled as constant symbols).
Other connectives can be introduced analogously. We exemplarily do this for \m\\ ,
\m\\, and \mL=\ (Leibniz equality on individuals). Moreover, the modal
operators \\\ and \\\ are introduced. Definitions could be used instead of
abbreviations.\
abbreviation mnot :: "\ \ \" ("m\") where "m\ \ \ (\w. \ \ w)"
abbreviation mand :: "\ \ \ \ \" (infixr "m\" 65) where "\ m\ \ \ (\w. \ w \ \ w)"
abbreviation mor :: "\ \ \ \ \" (infixr "m\" 70) where "\ m\ \ \ (\w. \ w \ \ w)"
abbreviation mimplies :: "\ \ \ \ \" (infixr "m\" 74) where "\ m\ \ \ (\w. \ w \ \ w)"
abbreviation mequiv:: "\ \ \ \ \" (infixr "m\" 76) where "\ m\ \ \ (\w. \ w \ \ w)"
abbreviation mforall :: "('a \ \) \ \" ("\") where "\ \ \ (\w. \x. \ x w)"
abbreviation mexists :: "('a \ \) \ \" ("\") where "\ \ \ (\w. \x. \ x w)"
abbreviation mLeibeq :: "\ \ \ \ \" (infixr "mL=" 90) where "x mL= y \ \(\\. (\ x m\ \ y))"
abbreviation mbox :: "\ \ \" ("\") where "\ \ \ (\w. \v. w r v \ \ v)"
abbreviation mdia :: "\ \ \" ("\") where "\ \ \ (\w. \v. w r v \ \ v)"
text \For grounding lifted formulas, the meta-predicate \valid\ is introduced.\
(*<*) no_syntax "_list" :: "args \ 'a list" ("[(_)]") (*>*)
abbreviation valid :: "\ \ bool" ("[_]") where "[p] \ \w. p w"
section \G\"odel's Ontological Argument\
text \Constant symbol \P\ (G\"odel's `Positive') is declared.\
consts P :: "(\ \ \) \ \"
text \The meaning of \P\ is restricted by axioms \A1(a/b)\: $\all \phi
[P(\neg \phi) \biimp \neg P(\phi)]$ (Either a property or its negation is positive, but not both.)
and \A2\: $\all \phi \all \psi [(P(\phi) \wedge \nec \all x [\phi(x) \imp \psi(x)])
\imp P(\psi)]$ (A property necessarily implied by a positive property is positive).\
axiomatization where
A1a: "[\(\\. P (\x. m\ (\ x)) m\ m\ (P \))]" and
A1b: "[\(\\. m\ (P \) m\ P (\x. m\ (\