Adjustments for initial AFP submission.

AOT_PLM.thy

@@ -8585,9 +8585,9 @@ proof -
                [\<lambda>z [\<lambda>xy \<forall>F ([F]x \<equiv> [F]y)]zy])\<close>
     using "\<exists>E"[rotated] by blast
   AOT_have \<open>[\<lambda>z [\<lambda>xy \<forall>F ([F]x \<equiv> [F]y)]zx]x\<close>
-    by (auto intro!: "\<beta>\<leftarrow>C"(1) "cqt:2";
-        simp add: "&I" "ex:1:a" prod_denotesI "rule-ui:3"
-                  "oth-class-taut:3:a" "universal-cor")
+    by (auto intro!: "\<beta>\<leftarrow>C"(1) "cqt:2"
+             simp: "&I" "ex:1:a" prod_denotesI "rule-ui:3"
+                   "oth-class-taut:3:a" "universal-cor")
   AOT_hence \<open>[\<lambda>z [\<lambda>xy \<forall>F ([F]x \<equiv> [F]y)]zy]x\<close>
     by (rule "rule=E"[rotated, OF 0[THEN "&E"(2)]])
   AOT_hence \<open>[\<lambda>xy \<forall>F ([F]x \<equiv> [F]y)]xy\<close>

AOT_misc.thy

@@ -2,6 +2,8 @@ theory AOT_misc
   imports AOT_NaturalNumbers
 begin
 
+section\<open>Miscellaneous Theorems\<close>
+
 AOT_theorem PossiblyNumbersEmptyPropertyImpliesZero:
   \<open>\<diamond>Numbers(x,[\<lambda>z O!z & z \<noteq>\<^sub>E z]) \<rightarrow> x = 0\<close>
 proof(rule "\<rightarrow>I")

AOT_model.thy

@@ -6,6 +6,18 @@ begin
 declare[[typedef_overloaded]]
 (*>*)
 
+section\<open>References\<close>
+
+text\<open>
+A full description of this formalization including references can be found
+at @{url \<open>http://dx.doi.org/10.17169/refubium-35141\<close>}.
+
+The version of Principia Logico-Metaphysica (PLM) implemented in this formalization
+can be found at @{url \<open>http://mally.stanford.edu/principia-2021-10-13.pdf\<close>}, while
+the latest version of PLM is available at @{url \<open>http://mally.stanford.edu/principia.pdf\<close>}.
+
+\<close>
+
 section\<open>Model for the Logic of AOT\<close>
 
 text\<open>We introduce a primitive type for hyperintensional propositions.\<close>
@@ -15,7 +27,7 @@ text\<open>To be able to model modal operators following Kripke semantics,
      we introduce a primitive type for possible worlds and assert, by axiom,
      that there is a surjective function mapping propositions to the
      boolean-valued functions acting on possible worlds. We call the result
-     of applying this function to a proposition the Kripke-extension
+     of applying this function to a proposition the Montague intension
      of the proposition.\<close>
 typedecl w \<comment>\<open>The primtive type of possible worlds.\<close>
 axiomatization AOT_model_d\<o> :: \<open>\<o>\<Rightarrow>(w\<Rightarrow>bool)\<close> where
@@ -26,12 +38,12 @@ consts w\<^sub>0 :: w \<comment>\<open>The designated actual world.\<close>
 axiomatization where AOT_model_nonactual_world: \<open>\<exists>w . w \<noteq> w\<^sub>0\<close>
 
 text\<open>Validity of a proposition in a given world can now be modelled as the result
-     of applying that world to the Kripke-extension of the proposition.\<close>
+     of applying that world to the Montague intension of the proposition.\<close>
 definition AOT_model_valid_in :: \<open>w\<Rightarrow>\<o>\<Rightarrow>bool\<close> where
   \<open>AOT_model_valid_in w \<phi> \<equiv> AOT_model_d\<o> \<phi> w\<close>
 
-text\<open>By construction, we can choose a proposition for any given Kripke-extension,
-     s.t. the proposition is valid in a possible world iff the Kripke-extension
+text\<open>By construction, we can choose a proposition for any given Montague intension,
+     s.t. the proposition is valid in a possible world iff the Montague intension
      evaluates to true at that world.\<close>
 definition AOT_model_proposition_choice :: \<open>(w\<Rightarrow>bool) \<Rightarrow> \<o>\<close> (binder \<open>\<epsilon>\<^sub>\<o> \<close> 8)
   where \<open>\<epsilon>\<^sub>\<o> w. \<phi> w \<equiv> (inv AOT_model_d\<o>) \<phi>\<close>
@@ -893,18 +905,19 @@ next
     apply (subst (asm) (1 2) Abs_urrel_inverse)
     using AOT_model_proposition_choice_simp a_def b_def by force+
   assume \<Pi>_den: \<open>AOT_model_denotes \<Pi>\<close>
-  have \<open>\<exists>r . \<forall> x . Rep_rel \<Pi> (\<omega>\<kappa> x) = Rep_urrel r (\<omega>\<upsilon> x)\<close>
-    apply (rule exI[where x=\<open>rel_to_urrel \<Pi>\<close>])
-    apply auto
-    unfolding rel_to_urrel_def
-    apply (subst Abs_urrel_inverse)
-    apply auto
-     apply (metis (mono_tags, lifting) AOT_model_denotes_\<kappa>_def
+  have \<open>\<not>AOT_model_valid_in w (Rep_rel \<Pi> (SOME xa. \<kappa>\<upsilon> xa = null\<upsilon> x))\<close> for x w
+    by (metis (mono_tags, lifting) AOT_model_denotes_\<kappa>_def
               AOT_model_denotes_rel.rep_eq \<kappa>.exhaust_disc \<kappa>\<upsilon>.simps(1,2,3)
               \<open>AOT_model_denotes \<Pi>\<close> \<upsilon>.disc(8,9) \<upsilon>.distinct(3)
               is_\<alpha>\<kappa>_def is_\<omega>\<kappa>_def verit_sko_ex')
+  moreover have \<open>Rep_rel \<Pi> (\<omega>\<kappa> x) = Rep_rel \<Pi> (SOME y. \<kappa>\<upsilon> y = \<omega>\<upsilon> x)\<close> for x
     by (metis (mono_tags, lifting) AOT_model_denotes_rel.rep_eq
           AOT_model_term_equiv_\<kappa>_def \<kappa>\<upsilon>.simps(1) \<Pi>_den verit_sko_ex')
+  ultimately have \<open>Rep_rel \<Pi> (\<omega>\<kappa> x) = Rep_urrel (rel_to_urrel \<Pi>) (\<omega>\<upsilon> x)\<close> for x
+    unfolding rel_to_urrel_def
+    by (subst Abs_urrel_inverse) auto
+  hence \<open>\<exists>r . \<forall> x . Rep_rel \<Pi> (\<omega>\<kappa> x) = Rep_urrel r (\<omega>\<upsilon> x)\<close>
+    by (auto intro!: exI[where x=\<open>rel_to_urrel \<Pi>\<close>])
   then obtain r where r_prop: \<open>Rep_rel \<Pi> (\<omega>\<kappa> x) = Rep_urrel r (\<omega>\<upsilon> x)\<close> for x
     by blast
   assume \<open>AOT_model_denotes \<Pi>' \<Longrightarrow>
@@ -973,18 +986,19 @@ next
     apply (subst (asm) (1 2) Abs_urrel_inverse)
     using AOT_model_proposition_choice_simp a_def b_def by force+
   assume \<Pi>_den: \<open>AOT_model_denotes \<Pi>\<close>
-  have \<open>\<exists>r . \<forall> x . Rep_rel \<Pi> (\<omega>\<kappa> x) = Rep_urrel r (\<omega>\<upsilon> x)\<close>
-    apply (rule exI[where x=\<open>rel_to_urrel \<Pi>\<close>])
-    apply auto
-    unfolding rel_to_urrel_def
-    apply (subst Abs_urrel_inverse)
-    apply auto
-     apply (metis (mono_tags, lifting) AOT_model_denotes_\<kappa>_def
+  have \<open>\<not>AOT_model_valid_in w (Rep_rel \<Pi> (SOME xa. \<kappa>\<upsilon> xa = null\<upsilon> x))\<close> for x w
+    by (metis (mono_tags, lifting) AOT_model_denotes_\<kappa>_def
           AOT_model_denotes_rel.rep_eq \<kappa>.exhaust_disc \<kappa>\<upsilon>.simps(1,2,3)
           \<open>AOT_model_denotes \<Pi>\<close> \<upsilon>.disc(8) \<upsilon>.disc(9) \<upsilon>.distinct(3)
           is_\<alpha>\<kappa>_def is_\<omega>\<kappa>_def verit_sko_ex')
+  moreover have \<open>Rep_rel \<Pi> (\<omega>\<kappa> x) = Rep_rel \<Pi> (SOME xa. \<kappa>\<upsilon> xa = \<omega>\<upsilon> x)\<close> for x
     by (metis (mono_tags, lifting) AOT_model_denotes_rel.rep_eq
           AOT_model_term_equiv_\<kappa>_def \<kappa>\<upsilon>.simps(1) \<Pi>_den verit_sko_ex')
+  ultimately have \<open>Rep_rel \<Pi> (\<omega>\<kappa> x) = Rep_urrel (rel_to_urrel \<Pi>) (\<omega>\<upsilon> x)\<close> for x
+    unfolding rel_to_urrel_def
+    by (subst Abs_urrel_inverse) auto
+  hence \<open>\<exists>r . \<forall> x . Rep_rel \<Pi> (\<omega>\<kappa> x) = Rep_urrel r (\<omega>\<upsilon> x)\<close>
+    by (auto intro!: exI[where x=\<open>rel_to_urrel \<Pi>\<close>])
   then obtain r where r_prop: \<open>Rep_rel \<Pi> (\<omega>\<kappa> x) = Rep_urrel r (\<omega>\<upsilon> x)\<close> for x
     by blast
 

AOT_semantics.thy

@@ -127,9 +127,9 @@ specification(AOT_exe AOT_lambda)
   \<comment> \<open>Truth conditions of exemplification formulas.\<close>
   AOT_sem_exe: \<open>[w \<Turnstile> [\<Pi>]\<kappa>\<^sub>1...\<kappa>\<^sub>n] = ([w \<Turnstile> \<Pi>\<down>] \<and> [w \<Turnstile> \<kappa>\<^sub>1...\<kappa>\<^sub>n\<down>] \<and>
                                      [w \<Turnstile> \<guillemotleft>Rep_rel \<Pi> \<kappa>\<^sub>1\<kappa>\<^sub>n\<guillemotright>])\<close>
-  \<comment> \<open>\<eta>-conversion for denoting terms; equivalent to AOT's axiom\<close>
+  \<comment> \<open>\eta-conversion for denoting terms; equivalent to AOT's axiom\<close>
   AOT_sem_lambda_eta: \<open>[w \<Turnstile> \<Pi>\<down>] \<Longrightarrow> [w \<Turnstile> [\<lambda>\<nu>\<^sub>1...\<nu>\<^sub>n [\<Pi>]\<nu>\<^sub>1...\<nu>\<^sub>n] = \<Pi>]\<close>
-  \<comment> \<open>\<beta>-conversion; equivalent to AOT's axiom\<close>
+  \<comment> \<open>\beta-conversion; equivalent to AOT's axiom\<close>
   AOT_sem_lambda_beta: \<open>[w \<Turnstile> [\<lambda>\<nu>\<^sub>1...\<nu>\<^sub>n \<phi>{\<nu>\<^sub>1...\<nu>\<^sub>n}]\<down>] \<Longrightarrow> [w \<Turnstile> \<kappa>\<^sub>1...\<kappa>\<^sub>n\<down>] \<Longrightarrow>
                         [w \<Turnstile> [\<lambda>\<nu>\<^sub>1...\<nu>\<^sub>n \<phi>{\<nu>\<^sub>1...\<nu>\<^sub>n}]\<kappa>\<^sub>1...\<kappa>\<^sub>n] = [w \<Turnstile> \<phi>{\<kappa>\<^sub>1...\<kappa>\<^sub>n}]\<close>
   \<comment> \<open>Necessary and sufficient conditions for relations to denote. Equivalent
@@ -455,10 +455,10 @@ instance proof
   have AOT_meta_proj_denotes1: \<open>AOT_model_denotes (Abs_rel (\<lambda>z. AOT_exe \<Pi> (z, \<beta>)))\<close>
     if \<open>AOT_model_denotes \<Pi>\<close> for \<Pi> :: \<open><'a\<times>'b>\<close> and \<beta>
     using that unfolding AOT_model_denotes_rel.rep_eq
-    apply (auto simp: Abs_rel_inverse AOT_meta_prod_equivI(2) AOT_sem_denotes
-                      that intro!: AOT_sem_exe_equiv)
-    apply (metis AOT_model_denotes_prod_def AOT_sem_exe case_prodD)
-    using AOT_model_unary_regular by blast
+    apply (simp add: Abs_rel_inverse AOT_meta_prod_equivI(2) AOT_sem_denotes
+                      that)
+    by (metis (no_types, lifting) AOT_meta_prod_equivI(2) AOT_model_denotes_prod_def
+              AOT_model_unary_regular AOT_sem_exe AOT_sem_exe_equiv case_prodD)
   {
     fix \<kappa> :: 'a and \<Pi> :: \<open><'a\<times>'b>\<close>
     assume \<Pi>_denotes: \<open>AOT_model_denotes \<Pi>\<close>
@@ -1638,15 +1638,19 @@ proof -
         ultimately have \<open>[v \<Turnstile> \<box>([\<Pi>']\<kappa>\<^sub>0 \<equiv> [\<Pi>]\<kappa>\<^sub>0)]\<close>
           using 4 by (auto simp: AOT_sem_forall AOT_sem_imp)
       } note 4 = this
+      {
+        fix \<Pi>'' :: \<open><\<kappa>>\<close>
+        assume \<open>[v \<Turnstile> \<Pi>''\<down>]\<close>
+        moreover assume \<open>[w \<Turnstile> [\<Pi>'']\<kappa>\<^sub>0] = [w \<Turnstile> [\<Pi>']\<kappa>\<^sub>0]\<close> if \<open>[v \<Turnstile> [\<lambda>x \<diamond>E!x]\<kappa>\<^sub>0]\<close> for \<kappa>\<^sub>0 w
+        ultimately have 5: \<open>[v \<Turnstile> x[\<Pi>'']]\<close>
+          using 4 3
+          by (auto simp: AOT_sem_imp AOT_sem_equiv AOT_sem_box)
+      } note 5 = this
       have \<open>[v \<Turnstile> y[\<Pi>']]\<close>
         apply (rule AOT_sem_enc_indistinguishable_all[OF AOT_ExtendedModel])
         apply (fact 0)
-             apply (auto simp: 0 1 \<Pi>_den indist[simplified AOT_sem_forall
-                               AOT_sem_box AOT_sem_equiv])
-        apply (rule 3)
-         apply auto[1]
-        using 4
-        by (auto simp: AOT_sem_imp AOT_sem_equiv AOT_sem_box)
+        by (auto simp: 5 0 1 \<Pi>_den indist[simplified AOT_sem_forall
+                       AOT_sem_box AOT_sem_equiv])
     }
     moreover {
     {
@@ -1659,7 +1663,7 @@ proof -
         assume 2: \<open>[v \<Turnstile> [\<lambda>x \<diamond>[E!]x]z \<rightarrow> \<box>([\<Pi>']z \<equiv> [\<Pi>]z)]\<close> for z
         have \<open>[v \<Turnstile> y[\<Pi>']]\<close>
           using 3
-          apply (auto simp: AOT_sem_forall AOT_sem_imp AOT_sem_box AOT_sem_denotes)
+          apply (simp add: AOT_sem_forall AOT_sem_imp AOT_sem_box AOT_sem_denotes)
           by (metis (no_types, lifting) 1 2 AOT_model.AOT_term_of_var_cases
                                         AOT_sem_box AOT_sem_denotes AOT_sem_imp)
       } note 3 = this
@@ -1676,15 +1680,18 @@ proof -
         ultimately have \<open>[v \<Turnstile> \<box>([\<Pi>']\<kappa>\<^sub>0 \<equiv> [\<Pi>]\<kappa>\<^sub>0)]\<close>
           using 4 by (auto simp: AOT_sem_forall AOT_sem_imp)
       } note 4 = this
+      {
+        fix \<Pi>'' :: \<open><\<kappa>>\<close>
+        assume \<open>[v \<Turnstile> \<Pi>''\<down>]\<close>
+        moreover assume \<open>[w \<Turnstile> [\<Pi>'']\<kappa>\<^sub>0] = [w \<Turnstile> [\<Pi>']\<kappa>\<^sub>0]\<close> if \<open>[v \<Turnstile> [\<lambda>x \<diamond>E!x]\<kappa>\<^sub>0]\<close> for w \<kappa>\<^sub>0
+        ultimately have \<open>[v \<Turnstile> y[\<Pi>'']]\<close>
+          using 3 4 by (auto simp: AOT_sem_imp AOT_sem_equiv AOT_sem_box)
+      } note 5 = this
       have \<open>[v \<Turnstile> x[\<Pi>']]\<close>
         apply (rule AOT_sem_enc_indistinguishable_all[OF AOT_ExtendedModel])
               apply (fact 1)
-             apply (auto simp: 0 1 \<Pi>_den indist[simplified AOT_sem_forall
-                               AOT_sem_box AOT_sem_equiv])
-        apply (rule 3)
-         apply auto[1]
-        using 4
-        by (auto simp: AOT_sem_imp AOT_sem_equiv AOT_sem_box)
+        by (auto simp: 5 0 1 \<Pi>_den indist[simplified AOT_sem_forall
+                       AOT_sem_box AOT_sem_equiv])
     }
   }
   ultimately show \<open>[v \<Turnstile> \<forall>G (\<forall>z (O!z \<rightarrow> \<box>([G]z \<equiv> [\<Pi>]z)) \<rightarrow> x[G])] =
@@ -1750,7 +1757,7 @@ proof -
           by (simp add: y_enc_\<Pi>'')
       } note 2 = this
       AOT_have \<open>\<exists>G(\<forall>z (O!z \<rightarrow> \<box>([G]z \<equiv> [\<Pi>]z)) & y[G])\<close>
-        apply (auto simp: AOT_sem_exists AOT_sem_ordinary
+        apply (simp add: AOT_sem_exists AOT_sem_ordinary
             AOT_sem_imp AOT_sem_box AOT_sem_forall AOT_sem_equiv AOT_sem_conj)
         using 2[simplified AOT_sem_box AOT_sem_equiv AOT_sem_imp AOT_sem_forall]
         by blast

ROOT

@@ -1,5 +1,5 @@
 session "AOT" = "HOL-Cardinals" +
-  options [show_question_marks = false, names_short = true, browser_info]
+  options [show_question_marks = false, names_short = true, browser_info, document = pdf, document_output = "output"]
   sessions
     "HOL-Eisbach"
   theories

document/root.tex

@@ -1,4 +1,4 @@
-\documentclass[a4paper,enabledeprecatedfontcommands,abstract=on,twoside=true]{scrreprt}
+\documentclass[a4paper,enabledeprecatedfontcommands,abstract=on,twoside=true]{article}
 \usepackage{isabelle,isabellesym}
 \usepackage{url}
 \usepackage{xr}
@@ -14,6 +14,8 @@
 \usepackage[ngerman,english]{babel}
 \newcommand{\embeddedstyle}[1]{{\color{blue}#1}}
 \newcommand{\bigbox}{}
+\newcommand{\linelabel}[1]{}
+
 \setcounter{secnumdepth}{2}
 \setcounter{tocdepth}{1}
 
@@ -57,6 +59,36 @@
 % 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}