diff --git a/thys/Goedel_Incompleteness/Abstract_Encoding.thy b/thys/Goedel_Incompleteness/Abstract_Encoding.thy
new file mode 100644
--- /dev/null
+++ b/thys/Goedel_Incompleteness/Abstract_Encoding.thy
@@ -0,0 +1,62 @@
+chapter \<open>Abstract Encoding\<close>
+
+(*<*)
+theory Abstract_Encoding imports Deduction2
+begin
+(*>*)
+
+text \<open>Here we simply fix some unspecified encoding functions: encoding formulas
+and proofs as numerals.\<close>
+
+locale Encode =
+Syntax_with_Numerals
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and num
++
+fixes enc :: "'fmla \<Rightarrow> 'trm" ("\<langle>_\<rangle>")
+assumes
+enc[simp,intro!]: "\<And> \<phi>. \<phi> \<in> fmla \<Longrightarrow> enc \<phi> \<in> num"
+begin
+
+end \<comment> \<open>context @{locale Encode}\<close>
+
+text \<open>Explicit proofs (encoded as numbers), needed only for the harder half of
+Goedel's first, and for both half's of Rosser's version; not needed in Goedel's
+second.\<close>
+
+locale Encode_Proofs =
+Encode
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  enc
++
+Deduct2_with_Proofs
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  dsj
+  num
+  prv bprv
+  "proof" prfOf
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and num
+and eql cnj imp all exi
+and prv bprv
+and enc ("\<langle>_\<rangle>")
+and fls dsj
+and "proof" :: "'proof set" and prfOf
++
+fixes encPf :: "'proof \<Rightarrow> 'trm"
+assumes
+encPf[simp,intro!]: "\<And> pf. pf \<in> proof \<Longrightarrow> encPf pf \<in> num"
+
+
+(*<*)
+end
+(*>*)
\ No newline at end of file
diff --git a/thys/Goedel_Incompleteness/Abstract_First_Goedel.thy b/thys/Goedel_Incompleteness/Abstract_First_Goedel.thy
new file mode 100644
--- /dev/null
+++ b/thys/Goedel_Incompleteness/Abstract_First_Goedel.thy
@@ -0,0 +1,442 @@
+chapter \<open>Abstract Formulations of Gödel's First Incompleteness Theorem\<close>
+
+(*<*)
+theory Abstract_First_Goedel imports Goedel_Formula Standard_Model_More
+begin
+(*>*)
+
+section \<open>Proof-Theoretic Versions of Gödel's First\<close>
+
+context Goedel_Form
+begin
+
+subsection \<open>The easy half\<close>
+
+text \<open>First the "direct", positive formulation:\<close>
+lemma goedel_first_theEasyHalf_pos:
+assumes "prv \<phi>G"   shows "prv fls"
+proof-
+  have "prv (neg (PP \<langle>\<phi>G\<rangle>))" using prv_eqv_prv[OF _ _ assms prv_\<phi>G_eqv] by auto
+  moreover
+  {have "bprv (PP \<langle>\<phi>G\<rangle>)" using HBL1[OF \<phi>G Fvars_\<phi>G assms] unfolding PP_def .
+   from bprv_prv[OF _ _ this, simplified] have "prv (PP \<langle>\<phi>G\<rangle>)" .
+  }
+  ultimately show ?thesis using PP prv_neg_fls by (meson \<phi>G enc in_num)
+qed
+
+text \<open>... then the more standard contrapositive formulation:\<close>
+corollary goedel_first_theEasyHalf:
+"consistent \<Longrightarrow> \<not> prv \<phi>G"
+using goedel_first_theEasyHalf_pos unfolding consistent_def by auto
+
+end \<comment> \<open>context @{locale Goedel_Form}\<close>
+
+
+subsection \<open>The hard half\<close>
+
+text \<open>The hard half needs explicit proofs:\<close>
+context Goedel_Form_Proofs begin
+
+lemma goedel_first_theHardHalf:
+assumes oc: "\<omega>consistent"
+shows "\<not> prv (neg \<phi>G)"
+proof
+  assume pn: "prv (neg \<phi>G)"
+  hence pnn: "prv (neg (neg (wrepr.PP \<langle>\<phi>G\<rangle>)))"
+    using prv_eqv_imp_transi num wrepr.PP \<phi>G fls neg neg_def prv_\<phi>G_eqv prv_eqv_sym
+    by (metis (full_types) enc in_num)
+  note c = \<omega>consistent_implies_consistent[OF oc]
+  have np: "\<not> prv \<phi>G" using pn c unfolding consistent_def3 by blast
+  have "\<forall>p \<in> num. bprv (neg (PPf p \<langle>\<phi>G\<rangle>))" using not_prv_prv_neg_PPf[OF _ _ np] by auto
+  hence 0: "\<forall>p \<in> num. prv (neg (PPf p \<langle>\<phi>G\<rangle>))" using not_prv_prv_neg_PPf[OF _ _ np]
+    by (fastforce intro: bprv_prv)
+  have "\<not> prv (neg (neg (exi yy (PPf (Var yy) \<langle>\<phi>G\<rangle>))))" using 0 oc unfolding \<omega>consistent_def by auto
+  hence "\<not> prv (neg (neg (wrepr.PP \<langle>\<phi>G\<rangle>)))"
+    unfolding wrepr.PP_def by (subst P_def) (simp add:  PPf_def2)
+  thus False using pnn by auto
+qed
+
+theorem goedel_first:
+assumes "\<omega>consistent"
+shows "\<not> prv \<phi>G \<and> \<not> prv (neg \<phi>G)"
+  using assms goedel_first_theEasyHalf goedel_first_theHardHalf \<omega>consistent_implies_consistent by blast
+
+theorem goedel_first_ex:
+assumes "\<omega>consistent"
+shows "\<exists> \<phi>. \<phi> \<in> fmla \<and> \<not> prv \<phi> \<and> \<not> prv (neg \<phi>)"
+  using assms goedel_first by (intro exI[of _ \<phi>G]) blast
+
+
+end \<comment> \<open>context @{locale Goedel_Form_Proofs}\<close>
+
+
+section \<open>Model-Theoretic Versions of Gödel's First\<close>
+
+text \<open>The model-theoretic twist is that of additionally proving
+the truth of Gödel sentences.\<close>
+
+
+subsection \<open>First model-theoretic version\<close>
+
+locale Goedel_Form_Proofs_Minimal_Truth =
+Goedel_Form_Proofs
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  eql cnj imp all exi
+  fls
+  prv bprv
+  enc
+  S
+  dsj
+  "proof" prfOf encPf
+  Pf
++
+Minimal_Truth_Soundness
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  dsj
+  num
+  bprv
+  isTrue
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and eql cnj imp all exi
+and fls
+and dsj
+and num
+and prv bprv
+and enc ("\<langle>_\<rangle>")
+and S
+and "proof" :: "'proof set" and prfOf encPf
+and Pf
+and isTrue
+begin
+
+text \<open>Recall that "consistent" and "$\omega$-consistent" refer to @{term prv}, not to @{term bprv}.\<close>
+
+theorem isTrue_\<phi>G:
+  assumes "consistent"
+  shows "isTrue \<phi>G"
+proof-
+  have "\<forall> n \<in> num. bprv (neg (PPf n \<langle>\<phi>G\<rangle>))"
+  using not_prv_prv_neg_PPf[OF _ _ goedel_first_theEasyHalf[OF assms]] by auto
+  hence "\<forall> n \<in> num. isTrue (neg (PPf n \<langle>\<phi>G\<rangle>))" by (auto intro: sound_isTrue)
+  hence "isTrue (all yy (neg (PPf (Var yy) \<langle>\<phi>G\<rangle>)))" by (auto intro: isTrue_all)
+  moreover have "isTrue (imp (all yy (neg (PPf (Var yy) \<langle>\<phi>G\<rangle>))) \<phi>G)"
+  using bprv_eqv_all_not_PPf_imp_\<phi>G by (auto intro!: sound_isTrue)
+  ultimately show ?thesis by (rule isTrue_imp[rotated -2]) auto
+qed
+
+text \<open>The "strong" form of Gödel's First (also asserting the truth of
+the Gödel sentences):\<close>
+
+theorem goedel_first_strong:
+"\<omega>consistent \<Longrightarrow> \<not> prv \<phi>G \<and> \<not> prv (neg \<phi>G) \<and> isTrue \<phi>G"
+  using goedel_first isTrue_\<phi>G \<omega>consistent_implies_consistent by blast
+
+theorem goedel_first_strong_ex:
+"\<omega>consistent \<Longrightarrow> \<exists> \<phi>. \<phi> \<in> fmla \<and> \<not> prv \<phi> \<and> \<not> prv (neg \<phi>) \<and> isTrue \<phi>"
+  using goedel_first_strong by (intro exI[of _ \<phi>G]) blast
+
+end \<comment> \<open>context @{locale Goedel_Form_Proofs_Minimal_Truth}\<close>
+
+
+subsection \<open>Second model-theoretic version\<close>
+
+locale Goedel_Form_Minimal_Truth_Soundness_HBL1iff_Compl_Pf =
+Goedel_Form
+  var trm fmla Var num
+  FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  prv bprv
+  enc
+  S
+  P
++
+Minimal_Truth_Soundness_HBL1iff_Compl_Pf
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  dsj
+  num
+  enc
+  prv bprv
+  P
+  isTrue
+  Pf
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and eql cnj imp all exi
+and fls
+and dsj
+and num
+and prv bprv
+and enc ("\<langle>_\<rangle>")
+and S
+and isTrue
+and P
+and Pf
+
+
+locale Goedel_Form_Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf =
+Goedel_Form_Minimal_Truth_Soundness_HBL1iff_Compl_Pf
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  dsj
+  num
+  prv bprv
+  enc
+  S
+  isTrue
+  P
+  Pf
++
+Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  dsj
+  num
+  enc
+  prv bprv
+  P
+  isTrue
+  Pf
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and eql cnj imp all exi
+and fls
+and dsj
+and num
+and prv bprv
+and enc ("\<langle>_\<rangle>")
+and S
+and isTrue
+and P
+and Pf
++
+assumes prv_\<omega>consistent: "\<omega>consistent"
+
+(* Semantic Goedel's first, Goedel-style, second variant
+... established as a sublocale statement *)
+sublocale
+  Goedel_Form_Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf <
+  recover_proofs: Goedel_Form_Proofs_Minimal_Truth
+  where prfOf = prfOf and "proof" = "proof" and encPf = encPf
+  and prv = prv and bprv = bprv
+  by standard
+
+(* ... and here is the explicit statement, inside the locale that
+provides all the assumptions *)
+context Goedel_Form_Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf begin
+thm recover_proofs.goedel_first_strong
+
+end
+
+
+section \<open>Classical-Logic Versions of Gödel's First\<close>
+
+
+subsection \<open>First classical-logic version\<close>
+
+locale Goedel_Form_Classical_HBL1_rev_prv =
+Goedel_Form
+  var trm fmla Var num FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  prv bprv
+  enc
+  S
+  P
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var num FvarsT substT Fvars subst
+and eql cnj imp all exi
+and fls
+and prv bprv
+and enc ("\<langle>_\<rangle>")
+and S
+and P
++
+assumes
+\<comment> \<open>NB: we don't really need to assume classical reasoning (double negation)
+for all formulas, but only for the provability predicate:\<close>
+classical_P_prv: "\<And> \<phi>. \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> let PP = (\<lambda>t. subst P t xx) in
+  prv (neg (neg (PP \<langle>\<phi>\<rangle>))) \<Longrightarrow> prv (PP \<langle>\<phi>\<rangle>)"
+and
+HBL1_rev_prv: "\<And> \<phi>. \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> prv (PP \<langle>\<phi>\<rangle>) \<Longrightarrow> prv \<phi>"
+begin
+
+lemma HBL1_rev:
+  assumes f: "\<phi> \<in> fmla" and fv: "Fvars \<phi> = {}" and bp: "bprv (PP \<langle>\<phi>\<rangle>)"
+  shows "prv \<phi>"
+  using assms by (auto intro!: HBL1_rev_prv bprv_prv[OF _ _ bp])
+
+lemma classical_PP_prv: "\<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> prv (neg (neg (PP \<langle>\<phi>\<rangle>))) \<Longrightarrow> prv (PP \<langle>\<phi>\<rangle>)"
+  using classical_P_prv unfolding PP_def by auto
+
+lemma HBL1_iff: "\<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> bprv (PP \<langle>\<phi>\<rangle>) \<longleftrightarrow> prv \<phi>"
+  using HBL1 HBL1_rev unfolding PP_def by auto
+
+lemma HBL1_iff_prv: "\<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> prv (PP \<langle>\<phi>\<rangle>) \<longleftrightarrow> prv \<phi>"
+  by (meson HBL1_PP HBL1_rev_prv PP d_dwf.bprv_prv' enc in_num)
+
+lemma goedel_first_theHardHalf_pos:
+assumes "prv (neg \<phi>G)"   shows "prv fls"
+proof-
+  have "prv (neg (neg (PP \<langle>\<phi>G\<rangle>)))"
+    using assms neg_def prv_\<phi>G_eqv prv_eqv_imp_transi_rev by fastforce
+  hence "prv (PP \<langle>\<phi>G\<rangle>)" using classical_PP_prv by auto
+  hence "prv \<phi>G" using Fvars_\<phi>G HBL1_rev_prv by blast
+  thus ?thesis using assms prv_neg_fls by blast
+qed
+
+corollary goedel_first_theHardHalf:
+"consistent \<Longrightarrow> \<not> prv (neg \<phi>G)"
+  using goedel_first_theHardHalf_pos unfolding consistent_def by auto
+
+theorem goedel_first_classic:
+assumes "consistent"
+shows "\<not> prv \<phi>G \<and> \<not> prv (neg \<phi>G)"
+  using assms goedel_first_theEasyHalf goedel_first_theHardHalf by blast
+
+theorem goedel_first_classic_ex:
+assumes "consistent"
+shows "\<exists> \<phi>. \<phi> \<in> fmla \<and> \<not> prv \<phi> \<and> \<not> prv (neg \<phi>)"
+  using assms goedel_first_classic by (intro exI[of _ \<phi>G]) blast
+
+end \<comment> \<open>context @{locale Goedel_Form_Classical_HBL1_rev_prv}\<close>
+
+
+subsection \<open>Second classical-logic version\<close>
+
+locale Goedel_Form_Classical_HBL1_rev_prv_Minimal_Truth_Soundness_TIP =
+Goedel_Form_Classical_HBL1_rev_prv
+  var trm fmla Var num FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  prv bprv
+  enc
+  S
+  P
++
+Minimal_Truth_Soundness
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  dsj
+  num
+  bprv
+  isTrue
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var num FvarsT substT Fvars subst
+and eql cnj dsj imp all exi
+and fls
+and prv bprv
+and enc ("\<langle>_\<rangle>")
+and S
+and P
+and isTrue
++
+assumes
+\<comment>\<open>Truth of @{term \<phi>} implies provability (TIP) of (the internal representation of) @{term \<phi>}\<close>
+TIP: "\<And> \<phi>. \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow>
+  let PP = (\<lambda>t. subst P t xx) in
+  isTrue (PP \<langle>\<phi>\<rangle>) \<Longrightarrow> prv \<phi>"
+begin
+
+lemma TIP_PP: "\<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> isTrue (PP \<langle>\<phi>\<rangle>) \<Longrightarrow> prv \<phi>"
+  using TIP unfolding PP_def by auto
+
+theorem isTrue_\<phi>G:
+  assumes consistent
+  shows "isTrue \<phi>G"
+proof-
+  {assume "\<not> isTrue \<phi>G"
+   hence 1: "isTrue (neg \<phi>G)" using isTrue_neg by fastforce
+   have "bprv (imp (neg \<phi>G) (neg (neg (PP \<langle>\<phi>G\<rangle>))))"
+   by (auto simp add: bprv_\<phi>G_eqv B.prv_imp_eqvER B.prv_imp_neg_rev)
+   from prv_imp_implies_isTrue[OF _ _ _ _ this 1, simplified]
+   have "isTrue (neg (neg (PP \<langle>\<phi>G\<rangle>)))" .
+   from isTrue_neg_neg[OF _ _ this, simplified] have "isTrue (PP \<langle>\<phi>G\<rangle>)" .
+   hence "prv \<phi>G" using assms TIP_PP by auto
+   hence False using goedel_first_classic assms by auto
+  }
+  thus ?thesis by auto
+qed
+
+theorem goedel_first_classic_strong: "consistent \<Longrightarrow> \<not> prv \<phi>G \<and> \<not> prv (neg \<phi>G) \<and> isTrue \<phi>G"
+  using goedel_first_classic isTrue_\<phi>G by simp
+
+theorem goedel_first_classic_strong_ex:
+"consistent \<Longrightarrow> \<exists> \<phi>. \<phi> \<in> fmla \<and> \<not> prv \<phi> \<and> \<not> prv (neg \<phi>) \<and> isTrue \<phi>"
+  using goedel_first_classic_strong by (intro exI[of _ \<phi>G]) blast
+
+end \<comment> \<open>context @{locale Goedel_Form_Classical_HBL1_rev_prv_Minimal_Truth_Soundness_TIP}\<close>
+
+
+subsection \<open>Third classical-logic version\<close>
+
+locale Goedel_Form_Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf_Classical =
+Goedel_Form
+  var trm fmla Var num FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  prv bprv
+  enc
+  S
+  P
++
+Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf_Classical
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  dsj
+  num
+  enc
+  prv bprv
+  P
+  isTrue
+  Pf
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and eql cnj imp all exi
+and fls
+and dsj
+and num
+and prv bprv
+and enc ("\<langle>_\<rangle>")
+and S
+and isTrue
+and P
+and Pf
+
+
+sublocale Goedel_Form_Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf_Classical <
+  recover_proofs: Goedel_Form_Classical_HBL1_rev_prv_Minimal_Truth_Soundness_TIP where prv = prv and bprv = bprv
+proof (standard, goal_cases classical rev_rpv TIPf)
+  case (classical \<phi>)
+  then show ?case using HBL1_iff classical_P by (simp add: mts_prv_mts.PP_deff)
+next
+  case (rev_rpv \<phi>)
+  then show ?case using HBL1_iff_prv PP_def by simp
+next
+  case (TIPf \<phi>)
+  then show ?case using classical_P by (simp add: SS_def PP_def mts_prv_mts.TIP)
+qed
+
+context Goedel_Form_Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf_Classical begin
+thm recover_proofs.goedel_first_classic_strong
+end \<comment>\<open>context @{locale Goedel_Form_Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf_Classical}\<close>
+
+(*<*)
+end
+(*>*)
diff --git a/thys/Goedel_Incompleteness/Abstract_First_Goedel_Rosser.thy b/thys/Goedel_Incompleteness/Abstract_First_Goedel_Rosser.thy
new file mode 100644
--- /dev/null
+++ b/thys/Goedel_Incompleteness/Abstract_First_Goedel_Rosser.thy
@@ -0,0 +1,348 @@
+chapter \<open>Abstract Formulations of Gödel-Rosser's First Incompleteness Theorem\<close>
+
+(*<*)
+theory Abstract_First_Goedel_Rosser
+  imports Rosser_Formula Standard_Model_More
+begin
+(*>*)
+
+text \<open>The development here is very similar to that of Gödel First Incompleteness Theorem.
+It lacks classical logical variants, since for them Rosser's trick does bring
+any extra value.\<close>
+
+section \<open>Proof-Theoretic Versions\<close>
+
+context Rosser_Form_Proofs
+begin
+
+lemma NN_neg_unique_xx':
+  assumes [simp]:"\<phi> \<in> fmla" "Fvars \<phi> = {}"
+  shows
+    "bprv (imp (NN \<langle>\<phi>\<rangle> (Var xx'))
+          (eql \<langle>neg \<phi>\<rangle> (Var xx')))"
+  using B.prv_subst[of yy _ "Var xx'", OF _ _ _ NN_neg_unique[OF assms]] by fastforce
+
+lemma NN_imp_xx':
+  assumes [simp]: "\<phi> \<in> fmla" "Fvars \<phi> = {}" "\<chi> \<in> fmla"
+  shows "bprv (imp (subst \<chi> \<langle>neg \<phi>\<rangle> xx')
+                   (all xx' (imp (NN \<langle>\<phi>\<rangle> (Var xx')) \<chi>)))"
+proof-
+  have 2: "bprv (imp (eql \<langle>neg \<phi>\<rangle> (Var xx')) (imp (subst \<chi> \<langle>neg \<phi>\<rangle> xx') \<chi>))"
+    using B.prv_eql_subst_trm[of xx' \<chi> "\<langle>neg \<phi>\<rangle>" "Var xx'", simplified] .
+  have 1: "bprv (imp (subst \<chi> \<langle>neg \<phi>\<rangle> xx') (imp (eql \<langle>neg \<phi>\<rangle> (Var xx')) \<chi>))"
+    by (simp add: "2" B.prv_imp_com)
+  have 0: "bprv (imp (subst \<chi> \<langle>neg \<phi>\<rangle> xx') (imp (NN \<langle>\<phi>\<rangle> (Var xx')) \<chi>))"
+    using 1
+    by (elim B.prv_prv_imp_trans[rotated 3])
+      (auto simp add: B.prv_imp_com B.prv_imp_monoR NN_neg_unique_xx')
+  show ?thesis by (rule B.prv_all_imp_gen) (auto simp: 0)
+qed
+
+lemma goedel_rosser_first_theEasyHalf:
+  assumes c: "consistent"
+  shows "\<not> prv \<phi>R"
+proof
+  assume 0: "prv \<phi>R"
+  then obtain "prf" where [simp]: "prf \<in> proof" and "prfOf prf \<phi>R" using prv_prfOf by auto
+  hence 00: "bprv (PPf (encPf prf) \<langle>\<phi>R\<rangle>)" using prfOf_PPf by auto
+  from dwf_dwfd.d_dwf.bprv_prv'[OF _ 00, simplified] have b00: "prv (PPf (encPf prf) \<langle>\<phi>R\<rangle>)" .
+  have "\<not> prv (neg \<phi>R)" using 0 c unfolding consistent_def3 by auto
+  hence "\<forall> prf \<in> proof.  \<not> prfOf prf (neg \<phi>R)" using 00 prv_prfOf by auto
+  hence "bprv (neg (PPf p \<langle>neg \<phi>R\<rangle>))" if "p \<in> num" for p using not_prfOf_PPf Clean_PPf_encPf that
+    by (cases "p \<in> encPf ` proof") auto
+  hence 1: "prv (all zz (imp (LLq (Var zz) (encPf prf)) (neg (PPf (Var zz) \<langle>neg \<phi>R\<rangle>))))"
+    (* here use locale assumption about the order-like relation: *)
+    by (intro LLq_num) auto
+  have 11: "prv (RR (encPf prf) \<langle>\<phi>R\<rangle>)"
+    using NN_imp_xx'[of \<phi>R "neg (PPf (Var zz) (Var xx'))", simplified]
+    by (auto simp add: RR_def2 R_def
+      intro!: prv_all_congW[OF _ _ _ _ 1] prv_imp_monoL[OF _ _ _ dwf_dwfd.d_dwf.bprv_prv'])
+  have 3: "prv (cnj (PPf (encPf prf) \<langle>\<phi>R\<rangle>) (RR (encPf prf) \<langle>\<phi>R\<rangle>))"
+    by (rule prv_cnjI[OF _ _ b00 11]) auto
+  have "prv ((PP' \<langle>\<phi>R\<rangle>))" unfolding PP'_def P'_def
+     using 3 by (auto intro: prv_exiI[of _ _ "encPf prf"])
+  moreover have "prv (neg (PP' \<langle>\<phi>R\<rangle>))"
+    using prv_eqv_prv[OF _ _ 0 prv_\<phi>R_eqv] by auto
+  ultimately show False using c unfolding consistent_def3 by auto
+qed
+
+lemma goedel_rosser_first_theHardHalf:
+  assumes c: "consistent"
+  shows "\<not> prv (neg \<phi>R)"
+proof
+  assume 0: "prv (neg \<phi>R)"
+  then obtain "prf" where [simp,intro!]: "prf \<in> proof" and pr: "prfOf prf (neg \<phi>R)" using prv_prfOf by auto
+  define p where p: "p = encPf prf"
+  have [simp,intro!]: "p \<in> num" unfolding p by auto
+  have 11: "bprv (PPf p \<langle>neg \<phi>R\<rangle>)" using pr prfOf_PPf unfolding p by auto
+  have 1: "bprv (NN \<langle>\<phi>R\<rangle> \<langle>neg \<phi>R\<rangle>)" using NN_neg by simp
+
+  have "\<not> prv \<phi>R" using 0 c unfolding consistent_def3 by auto
+  from not_prv_prv_neg_PPf[OF _ _ this]
+  have b2: "\<forall> r \<in> num. bprv (neg (PPf r \<langle>\<phi>R\<rangle>))" by auto
+  hence 2: "\<forall> r \<in> num. prv (neg (PPf r \<langle>\<phi>R\<rangle>))"
+    by (auto intro: dwf_dwfd.d_dwf.bprv_prv')
+
+  obtain P where P[simp,intro!]: "P \<subseteq>num" "finite P"
+    and 3: "prv (dsj (sdsj {eql (Var yy) r |r. r \<in> P}) (LLq p (Var yy)))"
+    (* here use the other locale assumption about the order-like relation: *)
+    using LLq_num2 by auto
+
+  have "prv (imp (cnj (PPf (Var yy) \<langle>\<phi>R\<rangle>) (RR (Var yy) \<langle>\<phi>R\<rangle>)) fls)"
+  proof(rule prv_dsj_cases[OF _ _ _ 3])
+    {fix r assume r: "r \<in> P" hence rn[simp]: "r \<in> num" using P(1) by blast
+      have "prv (imp (cnj (PPf r \<langle>\<phi>R\<rangle>) (RR r \<langle>\<phi>R\<rangle>)) fls)"
+        using 2 unfolding neg_def
+        by (metis FvarsT_num PPf RR rn \<phi>R all_not_in_conv cnj enc fls imp in_num prv_imp_cnj3L prv_imp_mp)
+      hence "prv (imp (eql (Var yy) r)
+                (imp (cnj (PPf (Var yy) \<langle>\<phi>R\<rangle>) (RR (Var yy) \<langle>\<phi>R\<rangle>)) fls))"
+        using prv_eql_subst_trm_id[of yy "cnj (PPf (Var yy) \<langle>\<phi>R\<rangle>) (RR (Var yy) \<langle>\<phi>R\<rangle>)" r,simplified]
+        unfolding neg_def[symmetric]
+        by (intro prv_neg_imp_imp_trans) auto
+    }
+    thus "prv (imp (sdsj {eql (Var yy) r |r. r \<in> P})
+              (imp (cnj (PPf (Var yy) \<langle>\<phi>R\<rangle>) (RR (Var yy) \<langle>\<phi>R\<rangle>)) fls))"
+       using Var P(1) eql by (intro prv_sdsj_imp) (auto 0 0 simp: set_rev_mp)
+  next
+    let ?\<phi> = "all xx' (imp (NN \<langle>\<phi>R\<rangle> (Var xx')) (neg (PPf p (Var xx'))))"
+    have "bprv (neg ?\<phi>)"
+      using 1 11 by (intro B.prv_imp_neg_allWI[where t = "\<langle>neg \<phi>R\<rangle>"]) (auto intro: B.prv_prv_neg_imp_neg)
+    hence "prv (neg ?\<phi>)" by (auto intro: dwf_dwfd.d_dwf.bprv_prv')
+    hence 00: "prv (imp (LLq p (Var yy))
+                       (imp (imp (LLq p (Var yy)) ?\<phi>) fls))"
+      unfolding neg_def[symmetric] by (intro prv_imp_neg_imp_neg_imp) auto
+    have "prv (imp (LLq p (Var yy))
+              (imp (RR (Var yy) \<langle>\<phi>R\<rangle>) fls))"
+      unfolding neg_def[symmetric] using 00[folded neg_def]
+      by (auto simp add: RR_def2 R_def intro!: prv_imp_neg_allI[where t = p])
+    thus "prv (imp (LLq p (Var yy))
+              (imp (cnj (PPf (Var yy) \<langle>\<phi>R\<rangle>) (RR (Var yy) \<langle>\<phi>R\<rangle>)) fls))"
+      unfolding neg_def[symmetric] by (intro prv_imp_neg_imp_cnjR) auto
+  qed(auto, insert Var P(1) eql, simp_all add: set_rev_mp)
+  hence "prv (neg (exi yy (cnj (PPf (Var yy) \<langle>\<phi>R\<rangle>) (RR (Var yy) \<langle>\<phi>R\<rangle>))))"
+    unfolding neg_def[symmetric] by (intro prv_neg_neg_exi) auto
+  hence "prv (neg (PP' \<langle>\<phi>R\<rangle>))" unfolding PP'_def P'_def by simp
+  hence "prv \<phi>R" using prv_\<phi>R_eqv by (meson PP' \<phi>R enc in_num neg prv_eqv_prv_rev)
+  with `\<not> prv \<phi>R` show False using c unfolding consistent_def3 by auto
+qed
+
+theorem goedel_rosser_first:
+  assumes "consistent"
+  shows "\<not> prv \<phi>R \<and> \<not> prv (neg \<phi>R)"
+  using assms goedel_rosser_first_theEasyHalf goedel_rosser_first_theHardHalf by blast
+
+theorem goedel_rosser_first_ex:
+  assumes "consistent"
+  shows "\<exists> \<phi>. \<phi> \<in> fmla \<and> \<not> prv \<phi> \<and> \<not> prv (neg \<phi>)"
+  using assms goedel_rosser_first by (intro exI[of _ \<phi>R]) blast
+
+end \<comment> \<open>context @{locale Rosser_Form}\<close>
+
+
+section \<open>Model-Theoretic Versions\<close>
+
+subsection \<open>First model-theoretic version\<close>
+
+locale Rosser_Form_Proofs_Minimal_Truth =
+Rosser_Form_Proofs
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  eql cnj imp all exi
+  fls
+  prv bprv
+  Lq
+  dsj
+  "proof" prfOf
+  enc
+  N S
+  encPf
+  Pf
++
+Minimal_Truth_Soundness
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  dsj
+  num
+  bprv
+  isTrue
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and eql cnj imp all exi
+and fls
+and dsj
+and num
+and Lq
+and prv bprv
+and enc ("\<langle>_\<rangle>")
+and N S P
+and "proof" :: "'proof set" and prfOf encPf
+and Pf
+and isTrue
+begin
+
+lemma Fvars_PP'[simp]: "Fvars (PP' \<langle>\<phi>R\<rangle>) = {}" unfolding PP'_def
+  by (subst Fvars_subst) auto
+
+lemma Fvars_RR'[simp]: "Fvars (RR (Var yy) \<langle>\<phi>R\<rangle>) = {yy}"
+  unfolding RR_def
+  by (subst Fvars_psubst) (fastforce intro!: exI[of _ "{yy}"])+
+
+lemma isTrue_PPf_implies_\<phi>R:
+assumes "isTrue (all yy (neg (PPf (Var yy) \<langle>\<phi>R\<rangle>)))"
+(is "isTrue ?H")
+shows "isTrue \<phi>R"
+proof-
+  define F where "F \<equiv> RR (Var yy) \<langle>\<phi>R\<rangle>"
+  have [simp]: "F \<in> fmla" "Fvars F = {yy}"
+    unfolding F_def by auto
+  have [simp]: "exi yy (PPf (Var yy) \<langle>\<phi>R\<rangle>) \<in> fmla"
+    unfolding PPf_def by auto
+
+  have 1: "bprv
+     (imp (all yy (neg (PPf (Var yy) \<langle>\<phi>R\<rangle>)))
+       (neg (exi yy (PPf (Var yy) \<langle>\<phi>R\<rangle>))))"
+  (is "bprv (imp (all yy (neg ?G)) (neg (exi yy ?G)))")
+    using B.prv_all_neg_imp_neg_exi[of yy ?G] by auto
+  have 2: "bprv (imp (neg (exi yy ?G)) (neg (exi yy (cnj ?G F))))"
+    by (auto intro!: B.prv_imp_neg_rev B.prv_exi_cong B.prv_imp_cnjL)
+  have "bprv (imp (all yy (neg ?G)) (neg (exi yy (cnj ?G F))))"
+    using B.prv_prv_imp_trans[OF _ _ _  1 2] by simp
+  hence "bprv (imp ?H (neg (PP' \<langle>\<phi>R\<rangle>)))"
+    unfolding PP'_def P'_def
+    by (simp add: F_def)
+  from B.prv_prv_imp_trans[OF _ _ _  this bprv_imp_\<phi>R]
+  have "bprv (imp ?H \<phi>R)" by auto
+  from prv_imp_implies_isTrue[OF _ _ _ _ this assms, simplified]
+  show ?thesis .
+qed
+
+theorem isTrue_\<phi>R:
+  assumes "consistent"
+  shows "isTrue \<phi>R"
+proof-
+  have "\<forall> n \<in> num. bprv (neg (PPf n \<langle>\<phi>R\<rangle>))"
+    using not_prv_prv_neg_PPf[OF _ _ goedel_rosser_first_theEasyHalf[OF assms]]
+    by auto
+  hence "\<forall> n \<in> num. isTrue (neg (PPf n \<langle>\<phi>R\<rangle>))" by (auto intro: sound_isTrue)
+  hence "isTrue (all yy (neg (PPf (Var yy) \<langle>\<phi>R\<rangle>)))" by (auto intro: isTrue_all)
+  thus ?thesis using isTrue_PPf_implies_\<phi>R by auto
+qed
+
+
+theorem goedel_rosser_first_strong: "consistent \<Longrightarrow> \<not> prv \<phi>R \<and> \<not> prv (neg \<phi>R) \<and> isTrue \<phi>R"
+  using isTrue_\<phi>R goedel_rosser_first by blast
+
+theorem goedel_rosser_first_strong_ex:
+"consistent \<Longrightarrow> \<exists> \<phi>. \<phi> \<in> fmla \<and> \<not> prv \<phi> \<and> \<not> prv (neg \<phi>) \<and> isTrue \<phi>"
+  using goedel_rosser_first_strong by (intro exI[of _ \<phi>R]) blast
+
+end \<comment> \<open>context @{locale Rosser_Form_Proofs_Minimal_Truth}\<close>
+
+
+subsection \<open>Second model-theoretic version\<close>
+
+context Rosser_Form
+begin
+print_context
+end
+
+locale Rosser_Form_Minimal_Truth_Soundness_HBL1iff_Compl_Pf =
+Rosser_Form
+  var trm fmla Var
+  FvarsT substT Fvars subst
+  num
+  eql cnj imp all exi
+  fls
+  prv bprv
+  Lq
+  dsj
+  enc
+  N
+  S
+  P
++
+Minimal_Truth_Soundness_HBL1iff_Compl_Pf
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  dsj
+  num
+  enc
+  prv bprv
+  P
+  isTrue
+  Pf
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and eql cnj imp all exi
+and fls
+and dsj
+and num
+and prv bprv
+and Lq
+and enc ("\<langle>_\<rangle>")
+and N S
+and isTrue
+and P Pf
+
+
+
+locale Rosser_Form_Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf =
+Rosser_Form_Minimal_Truth_Soundness_HBL1iff_Compl_Pf
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  dsj
+  num
+  prv bprv
+  Lq
+  enc
+  N S
+  isTrue
+  P
+  Pf
++
+M : Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  dsj
+  num
+  enc
+  prv bprv
+  N
+  isTrue
+  Pf
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and eql cnj imp all exi
+and fls
+and dsj
+and num
+and prv bprv
+and Lq
+and enc ("\<langle>_\<rangle>")
+and N S P
+and isTrue
+and Pf
+
+sublocale
+  Rosser_Form_Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf <
+  recover_proofs: Rosser_Form_Proofs_Minimal_Truth
+  where prfOf = prfOf and "proof" = "proof" and encPf = encPf
+  and prv = prv and bprv = bprv
+  by standard
+
+context Rosser_Form_Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf
+begin
+thm recover_proofs.goedel_rosser_first_strong
+end
+
+(*<*)
+end
+(*>*)
+
diff --git a/thys/Goedel_Incompleteness/Abstract_Jeroslow_Encoding.thy b/thys/Goedel_Incompleteness/Abstract_Jeroslow_Encoding.thy
new file mode 100644
--- /dev/null
+++ b/thys/Goedel_Incompleteness/Abstract_Jeroslow_Encoding.thy
@@ -0,0 +1,165 @@
+chapter \<open>Jeroslow's Variant of G\"odel's Second Incompleteness Theorem\<close>
+
+(*<*)
+theory Abstract_Jeroslow_Encoding imports
+"Syntax_Independent_Logic.Deduction"
+begin
+(*>*)
+
+section \<open>Encodings and Derivability\<close>
+
+text \<open>Here we formalize some of the assumptions of Jeroslow's theorem:
+encoding, term-encoding and the First Derivability Condition.\<close>
+
+
+subsection \<open>Encoding of formulas\<close>
+
+locale Encode =
+Syntax_with_Numerals
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and num
++
+fixes
+(*************************************)
+(* Numeric formulas are assumed to be encoded as numerals: *)
+enc :: "'fmla \<Rightarrow> 'trm" ("\<langle>_\<rangle>")
+assumes
+enc[simp,intro!]: "\<And> \<phi>. \<phi> \<in> fmla \<Longrightarrow> enc \<phi> \<in> num"
+begin
+
+end \<comment> \<open>context @{locale Encode}\<close>
+
+
+subsection \<open>Encoding of computable functions\<close>
+
+text \<open>Jeroslow assumes the encodability of an abstract (unspecified) class of
+computable functions and the assumption that a particular function, @{term "sub \<phi>"} for each formula
+@{term \<phi>}, is in this collection. This is used to prove a different flavor of the diagonalization
+lemma (Jeroslow 1973). It turns out that only an encoding of unary computable functions
+is needed, so we only assume that.\<close>
+
+locale Encode_UComput =
+Encode
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  enc
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and num
+and enc ("\<langle>_\<rangle>")
++
+\<comment> \<open>Abstract (unspeficied) notion of unary "computable" function
+between numerals, which are encoded as numerals. They
+contain a special substitution-like function @{term "sub \<phi>"} for each formula @{term "\<phi>"}.\<close>
+fixes ucfunc :: "('trm \<Rightarrow> 'trm) set"
+  and encF :: "('trm \<Rightarrow> 'trm) \<Rightarrow> 'trm"
+  and sub :: "'fmla \<Rightarrow> 'trm \<Rightarrow> 'trm"
+assumes
+\<comment> \<open>NB: Due to the limitations of the type system, we define @{term "ufunc"} as a set of functions
+between terms, but we only care about their actions on numerals ...
+so we assume they send numerals to numerals:\<close>
+ucfunc[simp,intro!]: "\<And> f n. f \<in> ucfunc \<Longrightarrow> n \<in> num \<Longrightarrow> f n \<in> num"
+and
+encF[simp,intro!]: "\<And> f. f \<in> ucfunc \<Longrightarrow> encF f \<in> num"
+and
+sub[simp]: "\<And>\<phi>. \<phi> \<in> fmla \<Longrightarrow> sub \<phi> \<in> ucfunc"
+and
+\<comment> \<open>The function @{term "sub \<phi>"} takes any encoding of a function @{term "f"} and returns the encoding of
+the formula obtained by substituting for @{term "xx"} the value of @{term "f"} applied to its own encoding:\<close>
+sub_enc:
+"\<And> \<phi> f. \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {xx} \<Longrightarrow> f \<in> ucfunc \<Longrightarrow>
+    sub \<phi> (encF f) = enc (inst \<phi> (f (encF f)))"
+
+
+subsection \<open>Term-encoding of computable functons\<close>
+
+text \<open>For handling the notion of term-representation (which we introduce later),
+we assume we are given a set @{term "Ops"} of term operators and their encodings as numerals.
+We additionally assume that the term operators behave well w.r.t. free variables and
+substitution.\<close>
+
+locale TermEncode =
+Syntax_with_Numerals
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and num
++
+fixes
+Ops ::  "('trm \<Rightarrow> 'trm) set"
+and
+enc :: "('trm \<Rightarrow> 'trm) \<Rightarrow> 'trm" ("\<langle>_\<rangle>")
+assumes
+Ops[simp,intro!]: "\<And>f t. f \<in> Ops \<Longrightarrow> t \<in> trm \<Longrightarrow> f t \<in> trm"
+and
+enc[simp,intro!]: "\<And> f. f \<in> Ops \<Longrightarrow> enc f \<in> num"
+and
+Ops_FvarsT[simp]: "\<And> f t. f \<in> Ops \<Longrightarrow> t \<in> trm \<Longrightarrow> FvarsT (f t) = FvarsT t"
+and
+Ops_substT[simp]: "\<And> f t. f \<in> Ops \<Longrightarrow> t \<in> trm \<Longrightarrow> t1 \<in> trm \<Longrightarrow> x \<in> var \<Longrightarrow>
+  substT (f t) t1 x = f (substT t t1 x)"
+begin
+
+end \<comment> \<open>context @{locale TermEncode}\<close>
+
+
+subsection \<open>The first Hilbert-Bernays-Löb derivability condition\<close>
+
+locale HBL1 =
+Encode
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  enc
++
+Deduct
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  eql cnj imp all exi
+  prv
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and num
+and eql cnj imp all exi
+and prv bprv
+and enc ("\<langle>_\<rangle>")
++
+fixes P :: 'fmla
+assumes
+P[intro!,simp]: "P \<in> fmla"
+and
+Fvars_P[simp]: "Fvars P = {xx}"
+and
+HBL1: "\<And>\<phi>. \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> prv \<phi> \<Longrightarrow> prv (subst P \<langle>\<phi>\<rangle> xx)"
+begin
+
+text \<open>Predicate version of the provability formula\<close>
+definition PP where "PP \<equiv> \<lambda>t. subst P t xx"
+
+lemma PP[simp]: "\<And>t. t \<in> trm \<Longrightarrow> PP t \<in> fmla"
+  unfolding PP_def by auto
+
+lemma Fvars_PP[simp]: "\<And>t. t \<in> trm \<Longrightarrow> Fvars (PP t) = FvarsT t"
+  unfolding PP_def by auto
+
+lemma [simp]:
+"n \<in> num \<Longrightarrow> subst (PP (Var yy)) n yy = PP n"
+"n \<in> num \<Longrightarrow> subst (PP (Var xx)) n xx = PP n"
+  unfolding PP_def by auto
+
+lemma HBL1_PP:
+"\<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> prv \<phi> \<Longrightarrow> prv (PP \<langle>\<phi>\<rangle>)"
+  using HBL1 unfolding PP_def by auto
+
+end \<comment> \<open>context @{locale HBL1}\<close>
+
+(*<*)
+end
+(*>*)
\ No newline at end of file
diff --git a/thys/Goedel_Incompleteness/Abstract_Representability.thy b/thys/Goedel_Incompleteness/Abstract_Representability.thy
new file mode 100644
--- /dev/null
+++ b/thys/Goedel_Incompleteness/Abstract_Representability.thy
@@ -0,0 +1,458 @@
+chapter \<open>Representability Assumptions\<close>
+
+(*<*)
+theory Abstract_Representability imports Abstract_Encoding
+begin
+(*>*)
+
+text \<open>Here we make assumptions about various functions or relations being
+representable.\<close>
+
+
+section \<open>Representability of Negation\<close>
+
+text \<open>The negation function neg is assumed to be representable by a
+two-variable formula N.\<close>
+
+locale Repr_Neg =
+Deduct2_with_False
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  num
+  prv bprv
++
+Encode
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  enc
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and eql cnj imp all exi
+and fls
+and num
+and prv bprv
+and enc ("\<langle>_\<rangle>")
++
+fixes N :: 'fmla
+assumes
+N[simp,intro!]: "N \<in> fmla"
+and
+Fvars_N[simp]: "Fvars N = {xx,yy}"
+and
+neg_implies_prv_N:
+"\<And> \<phi>.
+  let NN = (\<lambda> t1 t2. psubst N [(t1,xx), (t2,yy)]) in
+   \<phi> \<in> fmla \<longrightarrow> Fvars \<phi> = {} \<longrightarrow> bprv (NN \<langle>\<phi>\<rangle> \<langle>neg \<phi>\<rangle>)"
+and
+N_unique:
+"\<And> \<phi>.
+  let NN = (\<lambda> t1 t2. psubst N [(t1,xx), (t2,yy)]) in
+  \<phi> \<in> fmla \<longrightarrow> Fvars \<phi> = {} \<longrightarrow>
+  bprv (all yy (all yy'
+    (imp (cnj (NN \<langle>\<phi>\<rangle> (Var yy)) (NN \<langle>\<phi>\<rangle> (Var yy')))
+         (eql (Var yy) (Var yy')))))"
+begin
+
+text \<open>NN is a notation for the predicate that takes terms and returns corresponding instances
+of N, obtained by substituting its free variables with these terms. This is very convenient
+for reasoning, and will be done for all the representing formulas we will consider.\<close>
+
+definition NN where "NN \<equiv> \<lambda> t1 t2. psubst N [(t1,xx), (t2,yy)]"
+
+lemma NN_def2: "t1 \<in> trm \<Longrightarrow> t2 \<in> trm \<Longrightarrow> yy \<notin> FvarsT t1 \<Longrightarrow>
+ NN t1 t2 = subst (subst N t1 xx) t2 yy"
+  unfolding NN_def by (rule psubst_eq_rawpsubst2[simplified]) auto
+
+lemma NN_neg:
+"\<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> bprv (NN \<langle>\<phi>\<rangle> \<langle>neg \<phi>\<rangle>)"
+  using neg_implies_prv_N unfolding Let_def NN_def by meson
+
+lemma NN_unique:
+  assumes "\<phi> \<in> fmla" "Fvars \<phi> = {}"
+  shows "bprv (all yy (all yy'
+    (imp (cnj (NN \<langle>\<phi>\<rangle> (Var yy)) (NN \<langle>\<phi>\<rangle> (Var yy')))
+         (eql (Var yy) (Var yy')))))"
+  using assms N_unique unfolding Let_def NN_def by meson
+
+lemma NN[simp,intro]:
+"t1 \<in> trm \<Longrightarrow> t2 \<in> trm \<Longrightarrow> NN t1 t2 \<in> fmla"
+unfolding NN_def by auto
+
+lemma Fvars_NN[simp]: "t1 \<in> trm \<Longrightarrow> t2 \<in> trm \<Longrightarrow> yy \<notin> FvarsT t1 \<Longrightarrow>
+Fvars (NN t1 t2) = FvarsT t1 \<union> FvarsT t2"
+by (auto simp add: NN_def2 subst2_fresh_switch)
+
+(* Here and elsewhere: hard to make into one or two uniform statements,
+given that we don't assume sufficiently powerful properties for trm substitution.
+So such lists would need to be maintained on an ad hoc basis, keeping adding instances
+when needed. *)
+lemma [simp]:
+"m \<in> num \<Longrightarrow> n \<in> num \<Longrightarrow> subst (NN m (Var yy)) n yy = NN m n"
+"m \<in> num \<Longrightarrow> n \<in> num \<Longrightarrow> subst (NN m (Var yy')) n yy = NN m (Var yy')"
+"m \<in> num \<Longrightarrow> subst (NN m (Var yy')) (Var yy) yy' = NN m (Var yy)"
+"n \<in> num \<Longrightarrow> subst (NN (Var xx) (Var yy)) n xx = NN n (Var yy)"
+"n \<in> num \<Longrightarrow> subst (NN (Var xx) (Var xx')) n xx = NN n (Var xx')"
+"m \<in> num \<Longrightarrow> n \<in> num \<Longrightarrow> subst (NN m (Var xx')) n zz = NN m (Var xx')"
+"n \<in> num \<Longrightarrow> subst (NN n (Var yy)) (Var xx') yy = NN n (Var xx')"
+"m \<in> num \<Longrightarrow> n \<in> num \<Longrightarrow> subst (NN m (Var xx')) n xx' = NN m n"
+  by (auto simp add: NN_def2 subst2_fresh_switch)
+
+lemma NN_unique2:
+assumes [simp]:"\<phi> \<in> fmla" "Fvars \<phi> = {}"
+shows
+"bprv (all yy
+     (imp (NN \<langle>\<phi>\<rangle> (Var yy))
+          (eql \<langle>neg \<phi>\<rangle> (Var yy))))"
+proof-
+  have 1: "bprv (NN \<langle>\<phi>\<rangle> \<langle>neg \<phi>\<rangle>)"
+    using NN_neg[OF assms] .
+  have 2: "bprv (all yy' (
+             imp (cnj (NN \<langle>\<phi>\<rangle> \<langle>neg \<phi>\<rangle>)
+                      (NN \<langle>\<phi>\<rangle> (Var yy')))
+                 (eql \<langle>neg \<phi>\<rangle> (Var yy'))))"
+    using B.prv_allE[of yy, OF _ _ _ NN_unique, of "\<phi>" "\<langle>neg \<phi>\<rangle>"]
+    by fastforce
+  have 31: "bprv (all yy' (
+             imp (NN \<langle>\<phi>\<rangle> \<langle>neg \<phi>\<rangle>)
+                 (imp (NN \<langle>\<phi>\<rangle> (Var yy'))
+                      (eql \<langle>neg \<phi>\<rangle> (Var yy')))))"
+    using B.prv_all_imp_cnj_rev[OF _ _ _ _ 2] by simp
+  have 32: "bprv (imp (NN \<langle>\<phi>\<rangle> \<langle>neg \<phi>\<rangle>)
+                      (all yy' (imp (NN \<langle>\<phi>\<rangle> (Var yy'))
+                                    (eql \<langle>neg \<phi>\<rangle> (Var yy')))))"
+    by (rule B.prv_all_imp[OF _ _ _ _ 31]) (auto simp: NN_def2)
+  have 33: "bprv (all yy' (imp (NN \<langle>\<phi>\<rangle> (Var yy'))
+                              (eql \<langle>neg \<phi>\<rangle> (Var yy'))))"
+    by (rule B.prv_imp_mp [OF _ _ 32 1]) auto
+  thus ?thesis using B.all_subst_rename_prv[OF _ _ _ _ 33, of yy] by simp
+qed
+
+lemma NN_neg_unique:
+assumes [simp]:"\<phi> \<in> fmla" "Fvars \<phi> = {}"
+shows
+"bprv (imp (NN \<langle>\<phi>\<rangle> (Var yy))
+           (eql \<langle>neg \<phi>\<rangle> (Var yy)))" (is "bprv ?A")
+proof-
+  have 0: "bprv (all yy ?A)"
+    using NN_unique2[of "\<phi>"] by simp
+  show ?thesis by (rule B.allE_id[OF _ _ 0]) auto
+qed
+
+lemma NN_exi_cnj:
+assumes \<phi>[simp]: "\<phi> \<in> fmla" "Fvars \<phi> = {}" and \<chi>[simp]: "\<chi> \<in> fmla"
+assumes f: "Fvars \<chi> = {yy}"
+shows "bprv (eqv (subst \<chi> \<langle>neg \<phi>\<rangle> yy)
+                 (exi yy (cnj \<chi> (NN \<langle>\<phi>\<rangle> (Var yy)))))"
+(is "bprv (eqv ?A ?B)")
+proof(intro B.prv_eqvI)
+  have yy: "yy \<in> var" by simp
+  let ?N = "NN \<langle>\<phi>\<rangle> (Var yy)"
+  have "bprv (imp (subst \<chi> \<langle>neg \<phi>\<rangle> yy) ((subst (cnj \<chi> ?N) \<langle>neg \<phi>\<rangle> yy)))" using NN_neg[OF \<phi>]
+    by (simp add: B.prv_imp_cnj B.prv_imp_refl B.prv_imp_triv)
+  thus "bprv (imp ?A ?B)"
+    by (elim B.prv_prv_imp_trans[rotated 3], intro B.prv_exi_inst) auto
+next
+  have 00: "bprv (imp (eql \<langle>neg \<phi>\<rangle> (Var yy)) (imp \<chi> (subst \<chi> \<langle>neg \<phi>\<rangle> yy)))"
+    by (rule B.prv_eql_subst_trm_id_rev) auto
+  have 11: "bprv (imp (NN \<langle>\<phi>\<rangle> (Var yy)) (imp \<chi> (subst \<chi> \<langle>neg \<phi>\<rangle> yy)))"
+    using 00 NN_neg_unique[OF \<phi>]
+    using NN num Var Variable \<phi> \<chi> eql imp subst B.prv_prv_imp_trans
+    by (metis (no_types, lifting) enc in_num neg)
+  hence "bprv (imp (cnj \<chi> (NN \<langle>\<phi>\<rangle> (Var yy))) (subst \<chi> \<langle>neg \<phi>\<rangle> yy))"
+    by (simp add: 11 B.prv_cnj_imp_monoR2 B.prv_imp_com)
+  hence 1: "bprv (all yy (imp (cnj \<chi> (NN \<langle>\<phi>\<rangle> (Var yy))) (subst \<chi> \<langle>neg \<phi>\<rangle> yy)))"
+    by (simp add: B.prv_all_gen)
+  have 2: "Fvars (subst \<chi> \<langle>neg \<phi>\<rangle> yy) = {}" using f by simp
+  show "bprv (imp ?B ?A)" using 1 2
+    by (simp add: B.prv_exi_imp)
+qed auto
+
+end \<comment> \<open>context @{locale Repr_Neg}\<close>
+
+
+section \<open>Representability of Self-Substitution\<close>
+
+text \<open>Self-substitution is the function that takes a formula @{term \<phi>}
+and returns $\phi[\langle\phi\rangle/\mathit{xx}]$ (for the fixed variable @{term xx}). This is all that
+will be needed for the diagonalization lemma.\<close>
+
+locale Repr_SelfSubst =
+Encode
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  enc
++
+Deduct2
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  eql cnj imp all exi
+  prv bprv
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and num
+and eql cnj imp all exi
+and prv bprv
+and enc ("\<langle>_\<rangle>")
++
+fixes S :: 'fmla
+assumes
+S[simp,intro!]: "S \<in> fmla"
+and
+Fvars_S[simp]: "Fvars S = {xx,yy}"
+and
+subst_implies_prv_S:
+"\<And> \<phi>.
+  let SS = (\<lambda> t1 t2. psubst S [(t1,xx), (t2,yy)]) in
+  \<phi> \<in> fmla \<longrightarrow> Fvars \<phi> = {xx} \<longrightarrow>
+  bprv (SS \<langle>\<phi>\<rangle> \<langle>subst \<phi> \<langle>\<phi>\<rangle> xx\<rangle>)"
+and
+S_unique:
+"\<And> \<phi>.
+  let SS = (\<lambda> t1 t2. psubst S [(t1,xx), (t2,yy)]) in
+  \<phi> \<in> fmla \<longrightarrow> Fvars \<phi> = {xx} \<longrightarrow>
+  bprv (all yy (all yy'
+     (imp (cnj (SS \<langle>\<phi>\<rangle> (Var yy)) (SS \<langle>\<phi>\<rangle> (Var yy')))
+          (eql (Var yy) (Var yy')))))"
+begin
+
+text \<open>SS is the instantiation combinator of S:\<close>
+definition SS where "SS \<equiv> \<lambda> t1 t2. psubst S [(t1,xx), (t2,yy)]"
+
+lemma SS_def2: "t1 \<in> trm \<Longrightarrow> t2 \<in> trm \<Longrightarrow>
+ yy \<notin> FvarsT t1 \<Longrightarrow>
+ SS t1 t2 = subst (subst S t1 xx) t2 yy"
+  unfolding SS_def by (rule psubst_eq_rawpsubst2[simplified]) auto
+
+lemma subst_implies_prv_SS:
+"\<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {xx} \<Longrightarrow> bprv (SS \<langle>\<phi>\<rangle> \<langle>subst \<phi> \<langle>\<phi>\<rangle> xx\<rangle>)"
+using subst_implies_prv_S unfolding Let_def SS_def by meson
+
+lemma SS_unique:
+"\<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {xx} \<Longrightarrow>
+ bprv (all yy (all yy'
+      (imp (cnj (SS \<langle>\<phi>\<rangle> (Var yy)) (SS \<langle>\<phi>\<rangle> (Var yy')))
+           (eql (Var yy) (Var yy')))))"
+using S_unique unfolding Let_def SS_def by meson
+
+lemma SS[simp,intro]:
+"t1 \<in> trm \<Longrightarrow> t2 \<in> trm \<Longrightarrow> SS t1 t2 \<in> fmla"
+unfolding SS_def by auto
+
+lemma Fvars_SS[simp]: "t1 \<in> trm \<Longrightarrow> t2 \<in> trm \<Longrightarrow> yy \<notin> FvarsT t1 \<Longrightarrow>
+Fvars (SS t1 t2) = FvarsT t1 \<union> FvarsT t2"
+by (auto simp add: SS_def2 subst2_fresh_switch)
+
+lemma [simp]:
+"m \<in> num \<Longrightarrow> p \<in> num \<Longrightarrow> subst (SS m (Var yy)) p yy = SS m p"
+"m \<in> num \<Longrightarrow> subst (SS m (Var yy')) (Var yy) yy' = SS m (Var yy)"
+"m \<in> num \<Longrightarrow> p \<in> num \<Longrightarrow> subst (SS m (Var yy')) p yy' = SS m p"
+"m \<in> num \<Longrightarrow> p \<in> num \<Longrightarrow> subst (SS m (Var yy')) p yy = SS m (Var yy')"
+"m \<in> num \<Longrightarrow> subst (SS (Var xx) (Var yy)) m xx = SS m (Var yy)"
+by (auto simp add: SS_def2 subst_comp_num Let_def)
+
+end \<comment> \<open>context @{locale Repr_SelfSubst}\<close>
+
+
+section \<open>Representability of Self-Soft-Substitution\<close>
+
+text \<open>The soft substitution function performs substitution logically instead of
+syntactically. In particular, its "self" version sends @{term \<phi>} to
+@{term "exi xx (cnj (eql (Var xx) (enc \<phi>)) \<phi>)"}. Representability of self-soft-substitution will be
+an alternative assumption in the diagonalization lemma.\<close>
+
+locale Repr_SelfSoftSubst =
+Encode
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  enc
++
+Deduct2
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  eql cnj imp all exi
+  prv bprv
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and num
+and eql cnj imp all exi
+and prv bprv
+and enc ("\<langle>_\<rangle>")
++
+fixes S :: 'fmla
+assumes
+S[simp,intro!]: "S \<in> fmla"
+and
+Fvars_S[simp]: "Fvars S = {xx,yy}"
+and
+softSubst_implies_prv_S:
+"\<And> \<phi>.
+  let SS = (\<lambda> t1 t2. psubst S [(t1,xx), (t2,yy)]) in
+  \<phi> \<in> fmla \<longrightarrow> Fvars \<phi> = {xx} \<longrightarrow>
+  bprv (SS \<langle>\<phi>\<rangle> \<langle>softSubst \<phi> \<langle>\<phi>\<rangle> xx\<rangle>)"
+and
+S_unique:
+"\<And> \<phi>.
+  let SS = (\<lambda> t1 t2. psubst S [(t1,xx), (t2,yy)]) in
+  \<phi> \<in> fmla \<longrightarrow> Fvars \<phi> = {xx} \<longrightarrow>
+  bprv (all yy (all yy'
+     (imp (cnj (SS \<langle>\<phi>\<rangle> (Var yy)) (SS \<langle>\<phi>\<rangle> (Var yy')))
+          (eql (Var yy) (Var yy')))))"
+begin
+
+text \<open>SS is the instantiation combinator of S:\<close>
+definition SS where "SS \<equiv> \<lambda> t1 t2. psubst S [(t1,xx), (t2,yy)]"
+
+lemma SS_def2: "t1 \<in> trm \<Longrightarrow> t2 \<in> trm \<Longrightarrow>
+ yy \<notin> FvarsT t1 \<Longrightarrow>
+ SS t1 t2 = subst (subst S t1 xx) t2 yy"
+  unfolding SS_def by (rule psubst_eq_rawpsubst2[simplified]) auto
+
+lemma softSubst_implies_prv_SS:
+"\<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {xx} \<Longrightarrow> bprv (SS \<langle>\<phi>\<rangle> \<langle>softSubst \<phi> \<langle>\<phi>\<rangle> xx\<rangle>)"
+using softSubst_implies_prv_S unfolding Let_def SS_def by meson
+
+lemma SS_unique:
+"\<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {xx} \<Longrightarrow>
+ bprv (all yy (all yy'
+     (imp (cnj (SS \<langle>\<phi>\<rangle> (Var yy)) (SS \<langle>\<phi>\<rangle> (Var yy')))
+          (eql (Var yy) (Var yy')))))"
+using S_unique unfolding Let_def SS_def by meson
+
+lemma SS[simp,intro]:
+"t1 \<in> trm \<Longrightarrow> t2 \<in> trm \<Longrightarrow> SS t1 t2 \<in> fmla"
+unfolding SS_def by auto
+
+lemma Fvars_SS[simp]: "t1 \<in> trm \<Longrightarrow> t2 \<in> trm \<Longrightarrow> yy \<notin> FvarsT t1 \<Longrightarrow>
+Fvars (SS t1 t2) = FvarsT t1 \<union> FvarsT t2"
+by (auto simp add: SS_def2 subst2_fresh_switch)
+
+lemma [simp]:
+"m \<in> num \<Longrightarrow> p \<in> num \<Longrightarrow> subst (SS m (Var yy)) p yy = SS m p"
+"m \<in> num \<Longrightarrow> subst (SS m (Var yy')) (Var yy) yy' = SS m (Var yy)"
+"m \<in> num \<Longrightarrow> p \<in> num \<Longrightarrow> subst (SS m (Var yy')) p yy' = SS m p"
+"m \<in> num \<Longrightarrow> p \<in> num \<Longrightarrow> subst (SS m (Var yy')) p yy = SS m (Var yy')"
+"m \<in> num \<Longrightarrow> subst (SS (Var xx) (Var yy)) m xx = SS m (Var yy)"
+by (auto simp add: SS_def2 subst_comp_num Let_def)
+
+end \<comment> \<open>context @{locale Repr_SelfSoftSubst}\<close>
+
+
+section \<open>Clean Representability of the "Proof-of" Relation\<close>
+
+
+text\<open>For the proof-of relation, we must assume a stronger version of
+representability, namely clean representability on the first argument, which
+is dedicated to encoding the proof component. The property asks that the
+representation predicate is provably false on numerals that do not encode
+proofs; it would hold trivially for surjective proof encodings.
+
+Cleanness is not a standard concept in the literature -- we have
+introduced it in our CADE 2019 paper~\cite{DBLP:conf/cade/0001T19}.\<close>
+
+locale CleanRepr_Proofs =
+Encode_Proofs
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  eql cnj imp all exi
+  prv bprv
+  enc
+  fls
+  dsj
+  "proof" prfOf
+  encPf
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and num
+and eql cnj imp all exi
+and prv bprv
+and enc ("\<langle>_\<rangle>")
+and fls dsj
+and "proof" :: "'proof set" and prfOf
+and encPf
++
+fixes Pf :: 'fmla
+assumes
+Pf[simp,intro!]: "Pf \<in> fmla"
+and
+Fvars_Pf[simp]: "Fvars Pf = {yy,xx}"
+and
+prfOf_Pf:
+"\<And> prf \<phi>.
+  let PPf = (\<lambda> t1 t2. psubst Pf [(t1,yy), (t2,xx)]) in
+  (prf \<in> proof \<and> \<phi> \<in> fmla \<and> Fvars \<phi> = {} \<longrightarrow>
+   prfOf prf \<phi>
+   \<longrightarrow>
+   bprv (PPf (encPf prf) \<langle>\<phi>\<rangle>))"
+and
+not_prfOf_Pf:
+"\<And> prf \<phi>.
+  let PPf = (\<lambda> t1 t2. psubst Pf [(t1,yy), (t2,xx)]) in
+  (prf \<in> proof \<and> \<phi> \<in> fmla \<and> Fvars \<phi> = {} \<longrightarrow>
+   \<not> prfOf prf \<phi>
+   \<longrightarrow>
+   bprv (neg (PPf (encPf prf) \<langle>\<phi>\<rangle>)))"
+and
+Clean_Pf_encPf:
+"\<And> p \<phi>. let PPf = (\<lambda> t1 t2. psubst Pf [(t1,yy), (t2,xx)]) in
+  p \<in> num \<and> \<phi> \<in> fmla \<and> Fvars \<phi> = {} \<longrightarrow> p \<notin> encPf ` proof \<longrightarrow> bprv (neg (PPf p \<langle>\<phi>\<rangle>))"
+begin
+
+text \<open>PPf is the instantiation combinator of Pf:\<close>
+definition PPf where "PPf \<equiv> \<lambda> t1 t2. psubst Pf [(t1,yy), (t2,xx)]"
+
+lemma prfOf_PPf:
+assumes "prf \<in> proof" "\<phi> \<in> fmla" "Fvars \<phi> = {}" "prfOf prf \<phi>"
+shows "bprv (PPf (encPf prf) \<langle>\<phi>\<rangle>)"
+  using assms prfOf_Pf unfolding PPf_def by auto
+
+lemma not_prfOf_PPf:
+assumes "prf \<in> proof" "\<phi> \<in> fmla" "Fvars \<phi> = {}" "\<not> prfOf prf \<phi>"
+shows "bprv (neg (PPf (encPf prf) \<langle>\<phi>\<rangle>))"
+  using assms not_prfOf_Pf unfolding PPf_def by auto
+
+lemma Clean_PPf_encPf:
+  assumes "\<phi> \<in> fmla" "Fvars \<phi> = {}" and "p \<in> num" "p \<notin> encPf ` proof"
+  shows "bprv (neg (PPf p \<langle>\<phi>\<rangle>))"
+using assms Clean_Pf_encPf unfolding PPf_def by auto
+
+lemma PPf[simp,intro!]: "t1 \<in> trm \<Longrightarrow> t2 \<in> trm \<Longrightarrow> xx \<notin> FvarsT t1 \<Longrightarrow> PPf t1 t2 \<in> fmla"
+  unfolding PPf_def by auto
+
+lemma PPf_def2: "t1 \<in> trm \<Longrightarrow> t2 \<in> trm \<Longrightarrow> xx \<notin> FvarsT t1 \<Longrightarrow>
+  PPf t1 t2 = subst (subst Pf t1 yy) t2 xx"
+  unfolding PPf_def by (rule psubst_eq_rawpsubst2[simplified]) auto
+
+lemma Fvars_PPf[simp]:
+"t1 \<in> trm \<Longrightarrow> t2 \<in> trm \<Longrightarrow> xx \<notin> FvarsT t1 \<Longrightarrow>
+ Fvars (PPf t1 t2) = FvarsT t1 \<union> FvarsT t2"
+by (auto simp add: PPf_def2 subst2_fresh_switch)
+
+lemma [simp]:
+"n \<in> num \<Longrightarrow> subst (PPf (Var yy) (Var xx)) n xx = PPf (Var yy) n"
+"m \<in> num \<Longrightarrow> n \<in> num \<Longrightarrow> subst (PPf (Var yy) m) n yy = PPf n m"
+"n \<in> num \<Longrightarrow> subst (PPf (Var yy) (Var xx)) n yy = PPf n (Var xx)"
+"m \<in> num \<Longrightarrow> n \<in> num \<Longrightarrow> subst (PPf m (Var xx)) n xx = PPf m n"
+"m \<in> num \<Longrightarrow> subst (PPf (Var zz) (Var xx')) m zz = PPf m (Var xx')"
+"m \<in> num \<Longrightarrow> n \<in> num \<Longrightarrow> subst (PPf m (Var xx')) n xx' = PPf m n"
+"n \<in> num \<Longrightarrow> subst (PPf (Var zz) (Var xx')) n xx' = PPf (Var zz) n"
+"m \<in> num \<Longrightarrow> n \<in> num \<Longrightarrow> subst (PPf (Var zz) n) m zz = PPf m n"
+by (auto simp add: PPf_def2 subst2_fresh_switch)
+
+lemma B_consistent_prfOf_iff_PPf:
+"B.consistent \<Longrightarrow> prf \<in> proof \<Longrightarrow> \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<longrightarrow> prfOf prf \<phi> \<longleftrightarrow> bprv (PPf (encPf prf) \<langle>\<phi>\<rangle>)"
+  unfolding B.consistent_def3 using not_prfOf_PPf[of "prf" \<phi>] prfOf_PPf[of "prf" \<phi>] by force
+
+lemma consistent_prfOf_iff_PPf:
+"consistent \<Longrightarrow> prf \<in> proof \<Longrightarrow> \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<longrightarrow> prfOf prf \<phi> \<longleftrightarrow> bprv (PPf (encPf prf) \<langle>\<phi>\<rangle>)"
+  using B_consistent_prfOf_iff_PPf[OF dwf_dwfd.consistent_B_consistent] .
+
+end \<comment> \<open>context @{locale CleanRepr_Proofs}\<close>
+
+(*<*)
+end
+(*>*)
diff --git a/thys/Goedel_Incompleteness/Abstract_Second_Goedel.thy b/thys/Goedel_Incompleteness/Abstract_Second_Goedel.thy
new file mode 100644
--- /dev/null
+++ b/thys/Goedel_Incompleteness/Abstract_Second_Goedel.thy
@@ -0,0 +1,108 @@
+chapter \<open>Abstract Formulation of Gödel's Second Incompleteness Theorem\<close>
+
+(*<*)
+theory Abstract_Second_Goedel imports Abstract_First_Goedel Derivability_Conditions
+begin
+(*>*)
+
+text \<open>We assume all three derivability conditions, and assumptions
+behind Gödel formulas:\<close>
+locale Goedel_Second_Assumptions =
+HBL1_2_3
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  eql cnj imp all exi
+  prv bprv
+  enc
+  P
++
+Goedel_Form
+  var trm fmla Var num FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  prv bprv
+  enc
+  S
+  P
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and num
+and eql cnj imp all exi
+and prv bprv
+and enc ("\<langle>_\<rangle>")
+and S
+and P
+and fls
+begin
+
+lemma P_G:
+"bprv (imp (PP \<langle>\<phi>G\<rangle>) (PP \<langle>fls\<rangle>))"
+proof-
+  have 0: "prv (imp \<phi>G (neg (PP \<langle>\<phi>G\<rangle>)))"
+  using prv_\<phi>G_eqv by (intro prv_imp_eqvEL) auto
+  have 1: "bprv (PP \<langle>imp \<phi>G (neg (PP \<langle>\<phi>G\<rangle>))\<rangle>)"
+  using HBL1_PP[OF _ _ 0] by simp
+  have 2: "bprv (imp (PP \<langle>\<phi>G\<rangle>) (PP \<langle>neg (PP \<langle>\<phi>G\<rangle>)\<rangle>))"
+  using HBL2_imp2[OF _ _  _ _ 1] by simp
+  have 3: "bprv (imp (PP \<langle>\<phi>G\<rangle>) (PP \<langle>PP \<langle>\<phi>G\<rangle>\<rangle>))"
+    using HBL3[OF \<phi>G] by simp
+  have 23: "bprv (imp (PP \<langle>\<phi>G\<rangle>)
+                      (cnj (PP \<langle>PP \<langle>\<phi>G\<rangle>\<rangle>)
+                           (PP \<langle>neg (PP \<langle>\<phi>G\<rangle>)\<rangle>)))"
+  using B.prv_imp_cnj[OF _ _ _ 3 2] by simp
+  have 4: "bprv (imp (cnj (PP \<langle>PP \<langle>\<phi>G\<rangle>\<rangle>)
+                          (PP \<langle>neg (PP \<langle>\<phi>G\<rangle>)\<rangle>))
+                     (PP \<langle>fls\<rangle>))"
+    using HBL2[of "PP \<langle>\<phi>G\<rangle>" fls] unfolding neg_def[symmetric] by simp
+  show ?thesis using B.prv_prv_imp_trans[OF _ _ _ 23 4] by simp
+qed
+
+text \<open>First the "direct", positive formulation:\<close>
+lemma goedel_second_pos:
+assumes "prv (neg (PP \<langle>fls\<rangle>))"
+shows "prv fls"
+proof-
+  note PG = bprv_prv[OF _ _ P_G, simplified]
+  have "prv (neg (PP \<langle>\<phi>G\<rangle>))"
+  using PG assms unfolding neg_def by (rule prv_prv_imp_trans[rotated 3]) auto
+  hence "prv \<phi>G" using prv_\<phi>G_eqv by (rule prv_eqv_prv_rev[rotated 2]) auto
+  thus ?thesis
+  \<comment>\<open>The only part of Goedel's first theorem that is needed:\<close>
+  using goedel_first_theEasyHalf_pos by simp
+qed
+
+text \<open>Then the more standard, counterpositive formulation:\<close>
+theorem goedel_second:
+"consistent \<Longrightarrow> \<not> prv (neg (PP \<langle>fls\<rangle>))"
+using goedel_second_pos unfolding consistent_def by auto
+
+
+text \<open>It is an immediate consequence of Gödel's Second HLB1, HLB2 that
+(assuming consistency)  @{term "prv (neg (PP \<langle>\<phi>\<rangle>))"} holds for no sentence, be it
+provable or not. The theory is omniscient about what it can prove
+(thanks to HLB1), but completely ignorant about what it cannot prove.\<close>
+
+corollary not_prv_neg_PP:
+assumes c: "consistent" and [simp]: "\<phi> \<in> fmla" "Fvars \<phi> = {}"
+shows "\<not> prv (neg (PP \<langle>\<phi>\<rangle>))"
+proof
+  assume 0: "prv (neg (PP \<langle>\<phi>\<rangle>))"
+  have "prv (imp fls \<phi>)" by simp
+  hence "bprv (PP \<langle>imp fls \<phi>\<rangle>)" by (intro HBL1_PP) auto
+  hence "bprv (imp (PP \<langle>fls\<rangle>) (PP \<langle>\<phi>\<rangle>))" by (intro HBL2_imp2) auto
+  hence "bprv (imp (neg (PP \<langle>\<phi>\<rangle>)) (neg (PP \<langle>fls\<rangle>)))" by (intro B.prv_imp_neg_rev) auto
+  from prv_imp_mp[OF _ _ bprv_prv[OF _ _ this, simplified] 0, simplified]
+  have "prv (neg (PP \<langle>fls\<rangle>))" .
+  thus False using goedel_second[OF c] by simp
+qed
+
+end \<comment> \<open>context @{locale Goedel_Second_Assumptions}\<close>
+
+(*<*)
+end
+(*>*)
+
+
+
+
diff --git a/thys/Goedel_Incompleteness/All_Abstract.thy b/thys/Goedel_Incompleteness/All_Abstract.thy
new file mode 100644
--- /dev/null
+++ b/thys/Goedel_Incompleteness/All_Abstract.thy
@@ -0,0 +1,17 @@
+(*<*)
+
+text \<open>This puts together all the theories of the abstract development\<close>
+
+theory All_Abstract
+imports
+  Abstract_First_Goedel
+  Abstract_First_Goedel_Rosser
+  Abstract_Second_Goedel
+  Jeroslow_Original
+  Jeroslow_Simplified
+  Loeb
+  Tarski
+begin
+
+end
+(*>*)
diff --git a/thys/Goedel_Incompleteness/Deduction2.thy b/thys/Goedel_Incompleteness/Deduction2.thy
new file mode 100644
--- /dev/null
+++ b/thys/Goedel_Incompleteness/Deduction2.thy
@@ -0,0 +1,280 @@
+chapter \<open>Deduction with Two Provability Relations\<close>
+(*<*)
+theory Deduction2 imports "Syntax_Independent_Logic.Deduction"
+begin
+(*>*)
+
+text \<open>We work with two provability relations:
+provability @{term prv} and basic provability @{term bprv}.\<close>
+
+section \<open>From Deduction with One Provability Relation to Two\<close>
+
+locale Deduct2 =
+Deduct
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  eql cnj imp all exi
+  prv
++
+B: Deduct
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  eql cnj imp all exi
+  bprv
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and num
+and eql cnj imp all exi
+and prv bprv
++
+assumes bprv_prv: "\<And>\<phi>. \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> bprv \<phi> \<Longrightarrow> prv \<phi>"
+begin
+
+(* Removing the sentence (empty Fvars) hypothesis from bprv_prv *)
+lemma bprv_prv':
+  assumes \<phi>: "\<phi> \<in> fmla" and b: "bprv \<phi>"
+  shows "prv \<phi>"
+proof-
+  obtain V where V: "Fvars \<phi> = V" by blast
+  have VV: "V \<subseteq> var" using Fvars V \<phi> by blast
+  have f: "finite V" using V finite_Fvars[OF \<phi>] by auto
+  thus ?thesis using \<phi> b V VV
+  proof(induction V arbitrary: \<phi> rule: finite.induct)
+    case (emptyI \<phi>)
+    then show ?case by (simp add: bprv_prv)
+  next
+    case (insertI W v \<phi>)
+    show ?case proof(cases "v \<in> W")
+      case True
+      thus ?thesis
+      using insertI.IH[OF `\<phi> \<in> fmla`] insertI.prems
+      by (simp add: insert_absorb)
+    next
+      case False
+      hence 1: "Fvars (all v \<phi>) = W"
+        using insertI.prems by auto
+      moreover have "bprv (all v \<phi>)"
+        using B.prv_all_gen insertI.prems by auto
+      ultimately have "prv (all v \<phi>)" using insertI by auto
+      thus ?thesis using allE_id insertI.prems by blast
+    qed
+  qed
+qed
+
+end \<comment> \<open>context @{locale Deduct2}\<close>
+
+
+locale Deduct2_with_False =
+Deduct_with_False
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  num
+  prv
++
+B: Deduct_with_False
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  num
+  bprv
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and eql cnj imp all exi
+and fls
+and num
+and prv bprv
++
+assumes bprv_prv: "\<And>\<phi>. \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> bprv \<phi> \<Longrightarrow> prv \<phi>"
+
+sublocale Deduct2_with_False < d_dwf: Deduct2
+  by standard (fact bprv_prv)
+
+context Deduct2_with_False begin
+
+lemma consistent_B_consistent: "consistent \<Longrightarrow> B.consistent"
+  using B.consistent_def bprv_prv consistent_def by blast
+
+end \<comment> \<open>context @{locale Deduct2_with_False}\<close>
+
+locale Deduct2_with_False_Disj =
+Deduct_with_False_Disj
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  dsj
+  num
+  prv
++
+B: Deduct_with_False_Disj
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  dsj
+  num
+  bprv
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and eql cnj imp all exi
+and fls
+and dsj
+and num
+and prv bprv
++
+assumes bprv_prv: "\<And>\<phi>. \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> bprv \<phi> \<Longrightarrow> prv \<phi>"
+
+sublocale Deduct2_with_False_Disj < dwf_dwfd: Deduct2_with_False
+  by standard (fact bprv_prv)
+
+(* Factoring in a strict-order-like relation (not actually required to be an order): *)
+locale Deduct2_with_PseudoOrder =
+Deduct2_with_False_Disj
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  dsj
+  num
+  prv bprv
++
+Syntax_PseudoOrder
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  dsj
+  num
+  Lq
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and eql cnj imp all exi
+and fls
+and dsj
+and num
+and prv bprv
+and Lq
++
+assumes
+(* We do not assume any ordering properties, but only these two axioms, Lq_num and Lq_num2,
+which (interestingly) would be satisfied by both \<le> and < within a sufficiently strong
+arithmetic such as Robinson's Q *)
+(* For each formula \<phi>(z) and numeral q, if \<phi>(p) is provable for all p
+then \<forall> z \<le> q. \<phi>(z) is provable.
+(Note that a more natural property would assume \<phi>(p) is provable for all p\<le>q,
+but we can get away with the stronger assumption (on the left of the implication). )
+*)
+Lq_num:
+"let LLq = (\<lambda> t1 t2. psubst Lq [(t1,zz), (t2,yy)]) in
+ \<forall> \<phi> \<in> fmla. \<forall> q \<in> num. Fvars \<phi> = {zz} \<and> (\<forall> p \<in> num. bprv (subst \<phi> p zz))
+    \<longrightarrow> prv (all zz (imp (LLq (Var zz) q) \<phi>))"
+and
+(* For each numeral p, there exists a finite set P such that it is provable that
+\<forall> y. (\<Or>p\<in>P. x = p) \<or> y \<le> p
+(where we write \<le> instead of Lq, but could also think of <):
+*)
+Lq_num2:
+"let LLq = (\<lambda> t1 t2. psubst Lq [(t1,zz), (t2,yy)]) in
+ \<forall> p \<in> num. \<exists> P \<subseteq> num. finite P \<and> prv (dsj (sdsj {eql (Var yy) r | r. r \<in> P}) (LLq p (Var yy)))"
+begin
+
+lemma LLq_num:
+assumes "\<phi> \<in> fmla" "q \<in> num" "Fvars \<phi> = {zz}" "\<forall> p \<in> num. bprv (subst \<phi> p zz)"
+shows "prv (all zz (imp (LLq (Var zz) q) \<phi>))"
+using assms Lq_num unfolding LLq_def by auto
+
+lemma LLq_num2:
+assumes "p \<in> num"
+shows "\<exists> P \<subseteq> num. finite P \<and> prv (dsj (sdsj {eql (Var yy) r | r. r \<in> P}) (LLq p (Var yy)))"
+using assms Lq_num2 unfolding LLq_def by auto
+
+end \<comment> \<open>context @{locale Deduct2_with_PseudoOrder}\<close>
+
+section \<open>Factoring In Explicit Proofs\<close>
+
+locale Deduct_with_Proofs =
+Deduct_with_False_Disj
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  dsj
+  num
+  prv
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and eql cnj imp all exi
+and fls
+and dsj
+and num
+and prv
++
+fixes
+"proof" :: "'proof set"
+and
+prfOf :: "'proof \<Rightarrow> 'fmla \<Rightarrow> bool"
+assumes
+\<comment> \<open>Provability means there exists a proof (only needed for sentences):\<close>
+prv_prfOf: "\<And> \<phi>. \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> prv \<phi> \<longleftrightarrow> (\<exists> prf \<in> proof. prfOf prf \<phi>)"
+
+(* We consider proof structure only for prv, not for bprv *)
+locale Deduct2_with_Proofs =
+Deduct2_with_False_Disj
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  dsj
+  num
+  prv bprv
++
+Deduct_with_Proofs
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  dsj
+  num
+  prv
+  "proof" prfOf
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and eql cnj imp all exi
+and fls
+and dsj
+and num
+and prv bprv
+and "proof" :: "'proof set" and prfOf
+
+locale Deduct2_with_Proofs_PseudoOrder =
+Deduct2_with_Proofs
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  dsj
+  num
+  prv bprv
+  "proof" prfOf
++
+Deduct2_with_PseudoOrder
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  dsj
+  num
+  prv bprv
+  Lq
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and eql cnj imp all exi
+and fls
+and dsj
+and num
+and prv bprv
+and "proof" :: "'proof set" and prfOf
+and Lq
+
+(*<*)
+end
+(*>*)
\ No newline at end of file
diff --git a/thys/Goedel_Incompleteness/Derivability_Conditions.thy b/thys/Goedel_Incompleteness/Derivability_Conditions.thy
new file mode 100644
--- /dev/null
+++ b/thys/Goedel_Incompleteness/Derivability_Conditions.thy
@@ -0,0 +1,205 @@
+chapter \<open>The Hilbert-Bernays-Löb (HBL) Derivability Conditions\<close>
+
+(*<*)
+theory Derivability_Conditions imports Abstract_Representability
+begin
+(*>*)
+
+section \<open>First Derivability Condition\<close>
+
+(* Assume the provability predicate is "very-weakly" representable,
+in that one implication of the weak representability condition holds.   *)
+locale HBL1 =
+Encode
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  enc
++
+Deduct2
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  eql cnj imp all exi
+  prv bprv
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and num
+and eql cnj imp all exi
+and prv bprv
+and enc ("\<langle>_\<rangle>")
++
+(* Very-weak represenatbility of provability, as a one-variable formula P, usually called the provability predicate: *)
+fixes P :: 'fmla
+assumes
+P[intro!,simp]: "P \<in> fmla"
+and
+Fvars_P[simp]: "Fvars P = {xx}"
+and
+HBL1: "\<And>\<phi>. \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> prv \<phi> \<Longrightarrow> bprv (subst P \<langle>\<phi>\<rangle> xx)"
+begin
+
+(* For all our (very-weak) representability assumptions, in addition to
+ the representing formulas,
+here, P, we define a corresponding instantiation combinator, here the
+predicate PP.
+If we think of P as P(xx), then PP t is the instance PP(t)  *)
+definition PP where "PP \<equiv> \<lambda>t. subst P t xx"
+
+lemma PP[simp]: "\<And>t. t \<in> trm \<Longrightarrow> PP t \<in> fmla"
+  unfolding PP_def by auto
+
+lemma Fvars_PP[simp]: "\<And>t. t \<in> trm \<Longrightarrow> Fvars (PP t) = FvarsT t"
+  unfolding PP_def by auto
+
+lemma [simp]:
+"n \<in> num \<Longrightarrow> subst (PP (Var yy)) n yy = PP n"
+"n \<in> num \<Longrightarrow> subst (PP (Var xx)) n xx = PP n"
+  unfolding PP_def by auto
+
+lemma HBL1_PP:
+"\<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> prv \<phi> \<Longrightarrow> bprv (PP \<langle>\<phi>\<rangle>)"
+  using HBL1 unfolding PP_def by auto
+
+end \<comment> \<open>context @{locale HBL1}\<close>
+
+
+section \<open>Connections between Proof Representability,
+First Derivability Condition, and Its Converse\<close>
+
+context CleanRepr_Proofs
+begin
+
+text \<open>Defining @{term P}, the internal notion of provability,
+from @{term Pf} (in its predicate form @{term PPf}), the internal notion of "proof-of".
+NB: In the technical sense of the term "represents", we have that
+@{term Pf} represents @{term pprv}, whereas @{term P} will not represent @{term prv}, but satisfy a weaker
+condition (weaker than weak representability), namely HBL1.\<close>
+
+subsection \<open>HBL1 from "proof-of" representability\<close>
+
+definition P :: "'fmla" where "P \<equiv> exi yy (PPf (Var yy) (Var xx))"
+
+lemma P[simp,intro!]: "P \<in> fmla" and Fvars_P[simp]: "Fvars P = {xx}"
+  unfolding P_def by (auto simp: PPf_def2)
+
+text \<open>We infer HBL1 from Pf representing prv:\<close>
+lemma HBL1:
+assumes \<phi>: "\<phi> \<in> fmla" "Fvars \<phi> = {}" and p\<phi>: "prv \<phi>"
+shows "bprv (subst P \<langle>\<phi>\<rangle> xx)"
+proof-
+  obtain "prf" where pf: "prf \<in> proof" and "prfOf prf \<phi>" using prv_prfOf assms by auto
+  hence 0: "bprv (PPf (encPf prf) (enc \<phi>))"
+    using prfOf_PPf \<phi> by auto
+  have 1: "subst (subst Pf (encPf prf) yy) \<langle>\<phi>\<rangle> xx = subst (subst Pf \<langle>\<phi>\<rangle> xx) (substT (encPf prf) \<langle>\<phi>\<rangle> xx) yy"
+     using assms pf by (intro subst_compose_diff) auto
+  show ?thesis using 0 unfolding P_def using assms
+    by (auto simp: PPf_def2 1 pf intro!: B.prv_exiI[of _ _ "encPf prf"])
+qed
+
+text \<open>This is used in several places, including for the hard half of
+Gödel's First and the truth of Gödel formulas (and also for the Rosser variants
+of these).\<close>
+lemma not_prv_prv_neg_PPf:
+assumes [simp]: "\<phi> \<in> fmla" "Fvars \<phi> = {}" and p: "\<not> prv \<phi>" and n[simp]: "n \<in> num"
+shows "bprv (neg (PPf n \<langle>\<phi>\<rangle>))"
+proof-
+  have "\<forall>prf\<in>proof. \<not> prfOf prf \<phi>" using prv_prfOf p by auto
+  hence "\<forall>prf\<in>proof. bprv (neg (PPf (encPf prf) \<langle>\<phi>\<rangle>))" using not_prfOf_PPf by auto
+  thus ?thesis using not_prfOf_PPf using Clean_PPf_encPf by (cases "n \<in> encPf ` proof") auto
+qed
+
+lemma consistent_not_prv_not_prv_PPf:
+assumes c: consistent
+and 0[simp]: "\<phi> \<in> fmla" "Fvars \<phi> = {}" "\<not> prv \<phi>" "n \<in> num"
+shows "\<not> bprv (PPf n \<langle>\<phi>\<rangle>)"
+  using not_prv_prv_neg_PPf[OF 0] c[THEN dwf_dwfd.consistent_B_consistent] unfolding B.consistent_def3 by auto
+
+end \<comment> \<open>context @{locale CleanRepr_Proofs}\<close>
+
+text \<open>The inference of HBL1 from "proof-of" representability, in locale form:\<close>
+sublocale CleanRepr_Proofs < wrepr: HBL1
+  where P = P
+  using HBL1 by unfold_locales auto
+
+
+subsection \<open>Sufficient condition for the converse of HBL1\<close>
+
+context CleanRepr_Proofs
+begin
+
+lemma PP_PPf:
+assumes "\<phi> \<in> fmla"
+shows "wrepr.PP \<langle>\<phi>\<rangle> = exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>)"
+  unfolding wrepr.PP_def using assms
+  by (auto simp: PPf_def2 P_def)
+
+text \<open>The converse of HLB1 condition follows from (the standard notion of)
+$\omega$-consistency for @{term bprv} and strong representability of proofs:\<close>
+lemma \<omega>consistentStd1_HBL1_rev:
+assumes oc: "B.\<omega>consistentStd1"
+and \<phi>[simp]: "\<phi> \<in> fmla" "Fvars \<phi> = {}"
+and iPP: "bprv (wrepr.PP \<langle>\<phi>\<rangle>)"
+shows "prv \<phi>"
+proof-
+  have 0: "bprv (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>))" using iPP by (simp add: PP_PPf)
+  {assume "\<not> prv \<phi>"
+   hence "\<forall>n \<in> num. bprv (neg (PPf n \<langle>\<phi>\<rangle>))" using not_prv_prv_neg_PPf by auto
+   hence "\<not> bprv (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>))"
+   using oc unfolding B.\<omega>consistentStd1_def using \<phi> by auto
+   hence False using 0 by simp
+  }
+  thus ?thesis by auto
+qed
+
+end \<comment> \<open>context @{locale CleanRepr_Proofs}\<close>
+
+
+section \<open>Second and Third Derivability Conditions\<close>
+
+text \<open>These are only needed for Gödel's Second.\<close>
+
+locale HBL1_2_3 =
+HBL1
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  eql cnj imp all exi
+  prv bprv
+  enc
+  P
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and num
+and eql cnj imp all exi
+and prv bprv
+and enc ("\<langle>_\<rangle>")
+and P
++
+assumes
+HBL2: "\<And>\<phi> \<chi>. \<phi> \<in> fmla \<Longrightarrow> \<chi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> Fvars \<chi> = {} \<Longrightarrow>
+  bprv (imp (cnj (PP \<langle>\<phi>\<rangle>) (PP \<langle>imp \<phi> \<chi>\<rangle>))
+           (PP \<langle>\<chi>\<rangle>))"
+and
+HBL3: "\<And>\<phi>. \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> bprv (imp (PP \<langle>\<phi>\<rangle>) (PP \<langle>PP \<langle>\<phi>\<rangle>\<rangle>))"
+begin
+
+text \<open>The implicational form of HBL2:\<close>
+lemma HBL2_imp:
+ "\<And>\<phi> \<chi>. \<phi> \<in> fmla \<Longrightarrow> \<chi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> Fvars \<chi> = {} \<Longrightarrow>
+  bprv (imp (PP \<langle>imp \<phi> \<chi>\<rangle>) (imp (PP \<langle>\<phi>\<rangle>) (PP \<langle>\<chi>\<rangle>)))"
+using HBL2 by (simp add: B.prv_cnj_imp B.prv_imp_com)
+
+text \<open>... and its weaker, "detached" version:\<close>
+lemma HBL2_imp2:
+assumes "\<phi> \<in> fmla" and "\<chi> \<in> fmla" "Fvars \<phi> = {}" "Fvars \<chi> = {}"
+assumes "bprv (PP \<langle>imp \<phi> \<chi>\<rangle>)"
+shows "bprv (imp (PP \<langle>\<phi>\<rangle>) (PP \<langle>\<chi>\<rangle>))"
+using assms by (meson HBL2_imp PP enc imp num B.prv_imp_mp subsetCE)
+
+end \<comment> \<open>context @{locale HBL1_2_3}\<close>
+
+(*<*)
+end
+(*>*)
+
+
diff --git a/thys/Goedel_Incompleteness/Diagonalization.thy b/thys/Goedel_Incompleteness/Diagonalization.thy
new file mode 100644
--- /dev/null
+++ b/thys/Goedel_Incompleteness/Diagonalization.thy
@@ -0,0 +1,218 @@
+chapter \<open>Diagonalization\<close>
+
+text \<open>This theory proves abstract versions of the diagonalization lemma,
+with both hard and soft substitution.\<close>
+
+
+section \<open>Alternative Diagonalization via Self-Substitution\<close>
+
+(*<*)
+theory Diagonalization imports Abstract_Representability
+begin
+(*>*)
+
+text \<open>
+Assuming representability of the diagonal instance of the substitution function,
+we prove the standard diagonalization lemma. More precisely, we show that it applies
+to any logic that
+-- embeds intuitionistic first-order logic over numerals
+-- has a countable number of formulas
+-- has formula self-substitution representable
+\<close>
+
+context Repr_SelfSubst
+begin
+
+theorem diagonalization:
+  assumes \<phi>[simp,intro!]: "\<phi> \<in> fmla" "Fvars \<phi> = {xx}"
+  shows "\<exists> \<psi>. \<psi> \<in> fmla \<and> Fvars \<psi> = {} \<and> bprv (eqv \<psi> (subst \<phi> \<langle>\<psi>\<rangle> xx))"
+proof-
+  let ?phi = "\<lambda> t. subst \<phi> t xx"
+  define \<chi> where "\<chi> \<equiv> exi yy (cnj (?phi (Var yy)) (SS (Var xx) (Var yy)))"
+  have \<chi>[simp,intro!]: "\<chi> \<in> fmla" unfolding \<chi>_def by auto
+  let ?chi = "\<lambda> t. subst \<chi> t xx"
+  define \<psi> where "\<psi> \<equiv> ?chi \<langle>\<chi>\<rangle>"
+  have \<psi>[simp,intro!]: "\<psi> \<in> fmla" unfolding \<psi>_def by auto
+  have f\<chi>[simp]: "Fvars \<chi> = {xx}" unfolding \<chi>_def by auto
+  hence Fvars_\<psi>: "Fvars \<psi> = {}" unfolding \<psi>_def by auto
+  have 1: "bprv (SS \<langle>\<chi>\<rangle> \<langle>\<psi>\<rangle>)"
+    using subst_implies_prv_SS[OF \<chi>] unfolding \<psi>_def by simp
+  have 2: "bprv (all yy' (
+             imp (cnj (SS \<langle>\<chi>\<rangle> \<langle>\<psi>\<rangle>)
+                      (SS \<langle>\<chi>\<rangle> (Var yy')))
+                 (eql \<langle>\<psi>\<rangle> (Var yy'))))"
+    using Fvars_\<psi> B.prv_allE[OF _ _ _ SS_unique, of \<chi> "\<langle>\<psi>\<rangle>"]
+    by fastforce
+  have 31: "bprv (all yy'
+                     (imp (SS \<langle>\<chi>\<rangle> \<langle>\<psi>\<rangle>)
+                          (imp (SS \<langle>\<chi>\<rangle> (Var yy'))
+                               (eql \<langle>\<psi>\<rangle> (Var yy')))))"
+    using B.prv_all_imp_cnj_rev[OF _ _ _ _ 2] by simp
+  have 32: "bprv (imp (SS \<langle>\<chi>\<rangle> \<langle>\<psi>\<rangle>)
+                      (all yy' (imp (SS \<langle>\<chi>\<rangle> (Var yy'))
+                                    (eql \<langle>\<psi>\<rangle> (Var yy')))))"
+    by (intro B.prv_all_imp[OF _ _ _ _ 31]) (auto simp: SS_def2)
+  have 33: "bprv (all yy' (imp (SS \<langle>\<chi>\<rangle> (Var yy'))
+                               (eql \<langle>\<psi>\<rangle> (Var yy'))))"
+    by (rule B.prv_imp_mp [OF _ _ 32 1]) auto
+  have 3: "bprv (all yy (imp (SS \<langle>\<chi>\<rangle> (Var yy))
+                             (eql \<langle>\<psi>\<rangle> (Var yy))))"
+    using B.all_subst_rename_prv[OF _ _ _ _ 33, of yy]
+    by fastforce
+  have 41: "bprv (imp (?phi \<langle>\<psi>\<rangle>)
+                      (cnj (?phi \<langle>\<psi>\<rangle>)
+                           (SS \<langle>\<chi>\<rangle> \<langle>\<psi>\<rangle>)))"
+    by (auto intro: in_num B.prv_imp_cnj B.prv_imp_refl B.prv_imp_triv[OF _ _ 1])
+  have [simp]: "subst (subst \<phi> \<langle>\<psi>\<rangle> xx) \<langle>\<psi>\<rangle> yy = subst \<phi> \<langle>\<psi>\<rangle> xx"
+    by (intro subst_notIn) auto
+  have [simp]: "subst (subst \<phi> (Var yy) xx) \<langle>\<psi>\<rangle> yy = subst \<phi> \<langle>\<psi>\<rangle> xx"
+    by (intro subst_subst) auto
+  have 42: "bprv (exi yy (imp (?phi \<langle>\<psi>\<rangle>)
+                              (cnj (?phi (Var yy))
+                                   (SS \<langle>\<chi>\<rangle> (Var yy)))))"
+    using 41 by (intro B.prv_exiI[of _ _ "\<langle>\<psi>\<rangle>"]) auto
+  have 4: "bprv (imp (?phi \<langle>\<psi>\<rangle>) (?chi \<langle>\<chi>\<rangle>))"
+    using B.prv_imp_exi[OF _ _ _ _ 42,simplified]
+    by (subst \<chi>_def) (auto simp add: subst_comp_num)
+  have 50: "bprv (all yy (
+          (imp (eql \<langle>\<psi>\<rangle> (Var yy))
+               (imp (?phi (Var yy))
+                    (?phi \<langle>\<psi>\<rangle>)))))"
+    using B.prv_all_eql[of yy xx \<phi> "\<langle>\<psi>\<rangle>" "Var yy"] by simp
+  have 51: "bprv (all yy (
+          (imp (SS \<langle>\<chi>\<rangle> (Var yy))
+               (imp (?phi (Var yy))
+               (?phi \<langle>\<psi>\<rangle>)))))" using B.prv_all_imp_trans[OF _ _ _ _ 3 50] by simp
+  have 52: "bprv (all yy (
+          (imp (cnj (?phi (Var yy))
+                    (SS \<langle>\<chi>\<rangle> (Var yy)))
+               (?phi \<langle>\<psi>\<rangle>))))" using B.prv_all_imp_cnj[OF _ _ _ _ 51] by simp
+  have 5: "bprv (imp (?chi \<langle>\<chi>\<rangle>) (?phi \<langle>\<psi>\<rangle>))"
+    using B.prv_exi_imp[OF _ _ _ _ 52,simplified]
+    by (subst \<chi>_def) (simp add: subst_comp_num)
+  have 6: "bprv (eqv (?chi \<langle>\<chi>\<rangle>) (?phi \<langle>\<psi>\<rangle>))"
+    using B.prv_cnjI[OF _ _ 5 4] unfolding eqv_def by simp
+  have 7: "bprv (eqv \<psi> (?phi \<langle>\<psi>\<rangle>))" using 6 unfolding \<psi>_def .
+  show ?thesis using \<psi> 7 Fvars_\<psi> by blast
+qed
+
+text \<open>Making this existential into a function.\<close>
+
+definition diag :: "'fmla \<Rightarrow> 'fmla" where
+  "diag \<phi> \<equiv> SOME \<psi>. \<psi> \<in> fmla \<and> Fvars \<psi> = {} \<and> bprv (eqv \<psi> (subst \<phi> \<langle>\<psi>\<rangle> xx))"
+
+theorem diag_everything:
+  assumes "\<phi> \<in> fmla" and "Fvars \<phi> = {xx}"
+  shows "diag \<phi> \<in> fmla \<and> Fvars (diag \<phi>) = {} \<and> bprv (eqv (diag \<phi>) (subst \<phi> \<langle>diag \<phi>\<rangle> xx))"
+  unfolding diag_def using someI_ex[OF diagonalization[OF assms]] .
+
+lemmas diag[simp] = diag_everything[THEN conjunct1]
+lemmas Fvars_diag[simp] = diag_everything[THEN conjunct2, THEN conjunct1]
+lemmas bprv_diag_eqv = diag_everything[THEN conjunct2, THEN conjunct2]
+
+end \<comment> \<open>context @{locale Repr_SelfSubst}\<close>
+
+
+section \<open>Alternative Diagonalization via Soft Self-Substitution\<close>
+
+context Repr_SelfSoftSubst
+begin
+
+theorem diagonalization:
+  assumes \<phi>[simp,intro!]: "\<phi> \<in> fmla" "Fvars \<phi> = {xx}"
+  shows "\<exists> \<psi>. \<psi> \<in> fmla \<and> Fvars \<psi> = {} \<and> bprv (eqv \<psi> (subst \<phi> \<langle>\<psi>\<rangle> xx))"
+proof-
+  let ?phi = "\<lambda> t. subst \<phi> t xx"
+  define \<chi> where "\<chi> \<equiv> exi yy (cnj (?phi (Var yy)) (SS (Var xx) (Var yy)))"
+  have \<chi>[simp,intro!]: "\<chi> \<in> fmla" unfolding \<chi>_def by auto
+  let ?chi = "\<lambda> t. softSubst \<chi> t xx"
+  define \<psi> where "\<psi> \<equiv> ?chi \<langle>\<chi>\<rangle>"
+  have \<psi>[simp,intro!]: "\<psi> \<in> fmla" unfolding \<psi>_def by auto
+  have f\<chi>[simp]: "Fvars \<chi> = {xx}" unfolding \<chi>_def by auto
+  hence Fvars_\<psi>: "Fvars \<psi> = {}" unfolding \<psi>_def by auto
+  have 1: "bprv (SS \<langle>\<chi>\<rangle> \<langle>\<psi>\<rangle>)"
+    using softSubst_implies_prv_SS[OF \<chi>] unfolding \<psi>_def by simp
+  have 2: "bprv (all yy' (
+             imp (cnj (SS \<langle>\<chi>\<rangle> \<langle>\<psi>\<rangle>)
+                      (SS \<langle>\<chi>\<rangle> (Var yy')))
+                 (eql \<langle>\<psi>\<rangle> (Var yy'))))"
+    using Fvars_\<psi> B.prv_allE[OF _ _ _ SS_unique, of \<chi> "\<langle>\<psi>\<rangle>"]
+    by fastforce
+  have 31: "bprv (all yy'
+                     (imp (SS \<langle>\<chi>\<rangle> \<langle>\<psi>\<rangle>)
+                          (imp (SS \<langle>\<chi>\<rangle> (Var yy'))
+                               (eql \<langle>\<psi>\<rangle> (Var yy')))))"
+    using B.prv_all_imp_cnj_rev[OF _ _ _ _ 2] by simp
+  have 32: "bprv (imp (SS \<langle>\<chi>\<rangle> \<langle>\<psi>\<rangle>)
+                     (all yy' (imp (SS \<langle>\<chi>\<rangle> (Var yy'))
+                                   (eql \<langle>\<psi>\<rangle> (Var yy')))))"
+    by (intro B.prv_all_imp[OF _ _ _ _ 31]) (auto simp: SS_def2)
+  have 33: "bprv (all yy' (imp (SS \<langle>\<chi>\<rangle> (Var yy'))
+                              (eql \<langle>\<psi>\<rangle> (Var yy'))))"
+    by (rule B.prv_imp_mp [OF _ _ 32 1]) auto
+  have 3: "bprv (all yy (imp (SS \<langle>\<chi>\<rangle> (Var yy))
+                            (eql \<langle>\<psi>\<rangle> (Var yy))))"
+    using B.all_subst_rename_prv[OF _ _ _ _ 33, of yy]
+    by fastforce
+  have 41: "bprv (imp (?phi \<langle>\<psi>\<rangle>)
+                     (cnj (?phi \<langle>\<psi>\<rangle>)
+                          (SS \<langle>\<chi>\<rangle> \<langle>\<psi>\<rangle>)))"
+    by (auto intro: in_num B.prv_imp_cnj B.prv_imp_refl B.prv_imp_triv[OF _ _ 1])
+  have [simp]: "subst (subst \<phi> \<langle>\<psi>\<rangle> xx) \<langle>\<psi>\<rangle> yy = subst \<phi> \<langle>\<psi>\<rangle> xx"
+    by (intro subst_notIn) auto
+  have [simp]: "subst (subst \<phi> (Var yy) xx) \<langle>\<psi>\<rangle> yy = subst \<phi> \<langle>\<psi>\<rangle> xx"
+    by (intro subst_subst) auto
+  have 42: "bprv (exi yy (imp (?phi \<langle>\<psi>\<rangle>)
+                             (cnj (?phi (Var yy))
+                                  (SS \<langle>\<chi>\<rangle> (Var yy)))))"
+    using 41 by (intro B.prv_exiI[of _ _ "\<langle>\<psi>\<rangle>"]) auto
+  have 4: "bprv (imp (?phi \<langle>\<psi>\<rangle>) (subst \<chi> \<langle>\<chi>\<rangle> xx))"
+    using B.prv_imp_exi[OF _ _ _ _ 42,simplified]
+    by (subst \<chi>_def) (auto simp add: subst_comp_num)
+  moreover have "bprv (imp (subst \<chi> \<langle>\<chi>\<rangle> xx) (?chi \<langle>\<chi>\<rangle>))" by (rule B.prv_subst_imp_softSubst) auto
+  ultimately have 4: "bprv (imp (?phi \<langle>\<psi>\<rangle>) (?chi \<langle>\<chi>\<rangle>))"
+    by (rule B.prv_prv_imp_trans[rotated -2]) auto
+  have 50: "bprv (all yy (
+          (imp (eql \<langle>\<psi>\<rangle> (Var yy))
+               (imp (?phi (Var yy))
+                    (?phi \<langle>\<psi>\<rangle>)))))"
+    using B.prv_all_eql[of yy xx \<phi> "\<langle>\<psi>\<rangle>" "Var yy"] by simp
+  have 51: "bprv (all yy (
+          (imp (SS \<langle>\<chi>\<rangle> (Var yy))
+               (imp (?phi (Var yy))
+               (?phi \<langle>\<psi>\<rangle>)))))" using B.prv_all_imp_trans[OF _ _ _ _ 3 50] by simp
+  have 52: "bprv (all yy (
+          (imp (cnj (?phi (Var yy))
+                    (SS \<langle>\<chi>\<rangle> (Var yy)))
+               (?phi \<langle>\<psi>\<rangle>))))" using B.prv_all_imp_cnj[OF _ _ _ _ 51] by simp
+  have "bprv (imp (?chi \<langle>\<chi>\<rangle>) (subst \<chi> \<langle>\<chi>\<rangle> xx))" by (rule B.prv_softSubst_imp_subst) auto
+  moreover have "bprv (imp (subst \<chi> \<langle>\<chi>\<rangle> xx) (?phi \<langle>\<psi>\<rangle>))"
+    using B.prv_exi_imp[OF _ _ _ _ 52,simplified]
+    by (subst \<chi>_def) (simp add: subst_comp_num)
+  ultimately have 5: "bprv (imp (?chi \<langle>\<chi>\<rangle>) (?phi \<langle>\<psi>\<rangle>))"
+    by (rule B.prv_prv_imp_trans[rotated -2]) auto
+  have 6: "bprv (eqv (?chi \<langle>\<chi>\<rangle>) (?phi \<langle>\<psi>\<rangle>))"
+    using B.prv_cnjI[OF _ _ 5 4] unfolding eqv_def by simp
+  have 7: "bprv (eqv \<psi> (?phi \<langle>\<psi>\<rangle>))" using 6 unfolding \<psi>_def .
+  show ?thesis using \<psi> 7 Fvars_\<psi> by blast
+qed
+
+text \<open>Making this existential into a function.\<close>
+
+definition diag :: "'fmla \<Rightarrow> 'fmla" where
+  "diag \<phi> \<equiv> SOME \<psi>. \<psi> \<in> fmla \<and> Fvars \<psi> = {} \<and> bprv (eqv \<psi> (subst \<phi> \<langle>\<psi>\<rangle> xx))"
+
+theorem diag_everything:
+  assumes "\<phi> \<in> fmla" and "Fvars \<phi> = {xx}"
+  shows "diag \<phi> \<in> fmla \<and> Fvars (diag \<phi>) = {} \<and> bprv (eqv (diag \<phi>) (subst \<phi> \<langle>diag \<phi>\<rangle> xx))"
+  unfolding diag_def using someI_ex[OF diagonalization[OF assms]] .
+
+lemmas diag[simp] = diag_everything[THEN conjunct1]
+lemmas Fvars_diag[simp] = diag_everything[THEN conjunct2, THEN conjunct1]
+lemmas prv_diag_eqv = diag_everything[THEN conjunct2, THEN conjunct2]
+
+end \<comment> \<open>context @{locale Repr_SelfSoftSubst}\<close>
+
+(*<*)
+end
+(*>*)
diff --git a/thys/Goedel_Incompleteness/Goedel_Formula.thy b/thys/Goedel_Incompleteness/Goedel_Formula.thy
new file mode 100644
--- /dev/null
+++ b/thys/Goedel_Incompleteness/Goedel_Formula.thy
@@ -0,0 +1,142 @@
+chapter \<open>Gödel Formulas\<close>
+
+(*<*)
+theory Goedel_Formula imports Diagonalization Derivability_Conditions
+begin
+(*>*)
+
+text \<open>Gödel formulas are defined by diagonalizing the negation of the provability predicate.\<close>
+
+locale Goedel_Form =
+\<comment> \<open>Assuming the @{term fls} (False) connective gives us negation:\<close>
+Deduct2_with_False
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  num
+  prv bprv
++
+Repr_SelfSubst
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  eql cnj imp all exi
+  prv bprv
+  enc
+  S
++
+HBL1
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  eql cnj imp all exi
+  prv bprv
+  enc
+  P
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var num FvarsT substT Fvars subst
+and eql cnj imp all exi
+and fls
+and prv bprv
+and enc ("\<langle>_\<rangle>")
+and S
+and P
+begin
+
+text \<open>The Gödel formula.
+NB, we speak of "the" Gödel formula because the diagonalization function makes a choice.\<close>
+definition \<phi>G :: 'fmla where "\<phi>G \<equiv> diag (neg P)"
+
+lemma \<phi>G[simp,intro!]: "\<phi>G \<in> fmla"
+and
+Fvars_\<phi>G[simp]: "Fvars \<phi>G = {}"
+  unfolding \<phi>G_def PP_def by auto
+
+lemma bprv_\<phi>G_eqv:
+"bprv (eqv \<phi>G (neg (PP \<langle>\<phi>G\<rangle>)))"
+  unfolding \<phi>G_def PP_def using bprv_diag_eqv[of "neg P"] by simp
+
+lemma prv_\<phi>G_eqv:
+"prv (eqv \<phi>G (neg (PP \<langle>\<phi>G\<rangle>)))"
+  using bprv_prv[OF _ _ bprv_\<phi>G_eqv, simplified] .
+
+end \<comment> \<open>context @{locale Goedel_Form}\<close>
+
+
+text \<open>Adding cleanly representable proofs to the assumptions
+behind Gödel formulas:\<close>
+
+locale Goedel_Form_Proofs =
+Repr_SelfSubst
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  eql cnj imp all exi
+  prv bprv
+  enc
+  S
++
+CleanRepr_Proofs
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  eql cnj imp all exi
+  prv bprv
+  enc
+  fls
+  dsj
+  "proof" prfOf
+  encPf
+  Pf
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst num
+and eql cnj imp all exi
+and fls
+and prv bprv
+and enc ("\<langle>_\<rangle>")
+and S
+and dsj
+and "proof" :: "'proof set" and prfOf encPf
+and Pf
+
+text \<open>... and extending the sublocale relationship @{locale CleanRepr_Proofs} < @{locale HBL1}:\<close>
+sublocale Goedel_Form_Proofs < Goedel_Form where P = P by standard
+
+
+context Goedel_Form_Proofs
+begin
+
+lemma bprv_\<phi>G_eqv_not_exi_PPf:
+"bprv (eqv \<phi>G (neg (exi yy (PPf (Var yy) \<langle>\<phi>G\<rangle>))))"
+proof-
+  have P: "P = exi yy Pf" using P_def by (simp add: PPf_def2)
+  hence "subst P \<langle>\<phi>G\<rangle> xx = subst (exi yy Pf) \<langle>\<phi>G\<rangle> xx" by auto
+  hence "subst P \<langle>\<phi>G\<rangle> xx = exi yy (subst Pf \<langle>\<phi>G\<rangle> xx)" by simp
+  thus ?thesis using bprv_\<phi>G_eqv by (simp add: wrepr.PP_def PPf_def2)
+qed
+
+lemma prv_\<phi>G_eqv_not_exi_PPf:
+"prv (eqv \<phi>G (neg (exi yy (PPf (Var yy) \<langle>\<phi>G\<rangle>))))"
+using bprv_prv[OF _ _ bprv_\<phi>G_eqv_not_exi_PPf, simplified] .
+
+lemma bprv_\<phi>G_eqv_all_not_PPf:
+"bprv (eqv \<phi>G (all yy (neg (PPf (Var yy) \<langle>\<phi>G\<rangle>))))"
+  by (rule B.prv_eqv_trans[OF _ _ _ bprv_\<phi>G_eqv_not_exi_PPf B.prv_neg_exi_eqv_all_neg]) auto
+
+lemma prv_\<phi>G_eqv_all_not_PPf:
+"prv (eqv \<phi>G (all yy (neg (PPf (Var yy) \<langle>\<phi>G\<rangle>))))"
+using bprv_prv[OF _ _ bprv_\<phi>G_eqv_all_not_PPf, simplified] .
+
+lemma bprv_eqv_all_not_PPf_imp_\<phi>G:
+"bprv (imp (all yy (neg (PPf (Var yy) \<langle>\<phi>G\<rangle>))) \<phi>G)"
+  using bprv_\<phi>G_eqv_all_not_PPf by (auto intro: B.prv_imp_eqvER)
+
+lemma prv_eqv_all_not_PPf_imp_\<phi>G:
+"prv (imp (all yy (neg (PPf (Var yy) \<langle>\<phi>G\<rangle>))) \<phi>G)"
+using bprv_prv[OF _ _ bprv_eqv_all_not_PPf_imp_\<phi>G, simplified] .
+
+
+end \<comment> \<open>context @{locale Goedel_Form_Proofs}\<close>
+
+
+(*<*)
+end
+(*>*)
diff --git a/thys/Goedel_Incompleteness/Jeroslow_Original.thy b/thys/Goedel_Incompleteness/Jeroslow_Original.thy
new file mode 100644
--- /dev/null
+++ b/thys/Goedel_Incompleteness/Jeroslow_Original.thy
@@ -0,0 +1,337 @@
+section \<open>A Formalization of Jeroslow's Original Argument\<close>
+
+(*<*)
+theory Jeroslow_Original imports
+"Syntax_Independent_Logic.Pseudo_Term"
+Abstract_Jeroslow_Encoding
+begin
+(*>*)
+
+subsection \<open>Preliminaries\<close>
+
+text \<open>The First Derivability Condition was stated using a formula
+with free variable @{term xx}, whereas the pseudo-term theory employs a different variable,
+inp. The distinction is of course immaterial, because we can perform
+a change of variable in the instantiation:\<close>
+
+context HBL1
+begin
+
+text \<open>Changing the variable (from @{term xx} to @{term inp}) in the provability predicate:\<close>
+definition "Pinp \<equiv> subst P (Var inp) xx"
+lemma PP_Pinp: "t \<in> trm \<Longrightarrow> PP t = instInp Pinp t"
+unfolding PP_def Pinp_def instInp_def by auto
+
+text \<open>A version of HBL1 that uses the @{term inp} variable:\<close>
+lemma HBL1_inp:
+"\<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> prv \<phi> \<Longrightarrow> prv (instInp Pinp \<langle>\<phi>\<rangle>)"
+unfolding Pinp_def instInp_def by (auto intro: HBL1)
+
+end \<comment> \<open>context @{locale HBL1 }\<close>
+
+
+subsection \<open>Jeroslow-style diagonalization\<close>
+
+locale Jeroslow_Diagonalization =
+Deduct_with_False_Disj_Rename
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  dsj
+  num
+  prv
++
+Encode
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  enc
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and eql cnj imp all exi
+and fls
+and dsj
+and num
+and prv
+and enc ("\<langle>_\<rangle>")
++
+fixes F :: "('trm \<Rightarrow> 'trm) set"
+  and encF :: "('trm \<Rightarrow> 'trm) \<Rightarrow> 'fmla"
+  and N :: "'trm \<Rightarrow> 'trm"
+  and ssap :: "'fmla \<Rightarrow> 'trm \<Rightarrow> 'trm"
+assumes
+\<comment> \<open>For the members @{term f} of @{term F}, we will only care about their action on numerals,
+and we assume that they send numerals to numerals.\<close>
+F[simp,intro!]: "\<And> f n. f \<in> F \<Longrightarrow> n \<in> num \<Longrightarrow> f n \<in> num"
+and
+encF[simp,intro!]: "\<And> f. f \<in> F \<Longrightarrow> encF f \<in> ptrm (Suc 0)"
+and
+N[simp,intro!]: "N \<in> F"
+and
+ssap[simp]: "\<And>\<phi>. \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {inp} \<Longrightarrow> ssap \<phi> \<in> F"
+and
+ReprF: "\<And>f n. f \<in> F \<Longrightarrow> n \<in> num \<Longrightarrow> prveqlPT (instInp (encF f) n) (f n)"
+and
+CapN: "\<And>\<phi>. \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> N \<langle>\<phi>\<rangle> = \<langle>neg \<phi>\<rangle>"
+and
+CapSS: \<comment> \<open>We consider formulas @{term \<psi>} of one variable, called @{term inp}:\<close>
+"\<And> \<psi> f. \<psi> \<in> fmla \<Longrightarrow> Fvars \<psi> = {inp} \<Longrightarrow> f \<in> F \<Longrightarrow>
+    ssap \<psi> \<langle>encF f\<rangle> = \<langle>instInpP \<psi> 0 (instInp (encF f) \<langle>encF f\<rangle>)\<rangle>"
+begin
+
+lemma encF_fmla[simp,intro!]: "\<And> f. f \<in> F \<Longrightarrow> encF f \<in> fmla"
+by auto
+
+lemma enc_trm: "\<phi> \<in> fmla \<Longrightarrow> \<langle>\<phi>\<rangle> \<in> trm"
+by auto
+
+definition \<tau>J :: "'fmla \<Rightarrow> 'fmla" where
+"\<tau>J \<psi> \<equiv> instInp (encF (ssap \<psi>)) (\<langle>encF (ssap \<psi>)\<rangle>)"
+
+definition \<phi>J :: "'fmla \<Rightarrow> 'fmla" where
+"\<phi>J \<psi> \<equiv> instInpP \<psi> 0 (\<tau>J \<psi>)"
+
+lemma \<tau>J[simp]:
+assumes "\<psi> \<in> fmla" and "Fvars \<psi> = {inp}"
+shows "\<tau>J \<psi> \<in> ptrm 0"
+unfolding \<tau>J_def apply(rule instInp)
+using assms by auto
+
+lemma \<tau>J_fmla[simp]:
+assumes "\<psi> \<in> fmla" and "Fvars \<psi> = {inp}"
+shows "\<tau>J \<psi> \<in> fmla"
+using \<tau>J[OF assms] unfolding ptrm_def by auto
+
+lemma FvarsT_\<tau>J[simp]:
+assumes "\<psi> \<in> fmla" and "Fvars \<psi> = {inp}"
+shows "Fvars (\<tau>J \<psi>) = {out}"
+using \<tau>J[OF assms] unfolding ptrm_def by auto
+
+lemma \<phi>J[simp]:
+assumes "\<psi> \<in> fmla" and "Fvars \<psi> = {inp}"
+shows "\<phi>J \<psi> \<in> fmla"
+unfolding \<phi>J_def using assms by (intro instInpP_fmla) auto
+
+lemma Fvars_\<phi>J[simp]:
+assumes "\<psi> \<in> fmla" and "Fvars \<psi> = {inp}"
+shows "Fvars (\<phi>J \<psi>) = {}"
+using assms unfolding \<phi>J_def by auto
+
+lemma diagonalization:
+assumes \<psi>[simp]: "\<psi> \<in> fmla" and [simp]: "Fvars \<psi> = {inp}"
+shows "prveqlPT (\<tau>J \<psi>) \<langle>instInpP \<psi> 0 (\<tau>J \<psi>)\<rangle> \<and>
+       prv (eqv (\<phi>J \<psi>) (instInp \<psi> \<langle>\<phi>J \<psi>\<rangle>))"
+proof
+  define f where "f \<equiv> ssap \<psi>"
+  have f[simp]: "f \<in> F" unfolding f_def using assms by auto
+  have ff: "f \<langle>encF f\<rangle> = \<langle>instInpP \<psi> 0 (\<tau>J \<psi>)\<rangle>"
+  using assms unfolding f_def \<tau>J_def by (intro CapSS) auto
+
+  show "prveqlPT (\<tau>J \<psi>) \<langle>instInpP \<psi> 0 (\<tau>J \<psi>)\<rangle>"
+  using ReprF[OF f, of "\<langle>encF f\<rangle>"]
+  unfolding \<tau>J_def[of \<psi>, unfolded f_def[symmetric],symmetric] ff[symmetric]
+  by auto
+  from prveqlPT_prv_instInp_eqv_instInpP[OF \<psi>, of "\<tau>J \<psi>", OF _ _ _ _ this,
+           unfolded \<phi>J_def[symmetric]]
+  show "prv (eqv (\<phi>J \<psi>) (instInp \<psi> \<langle>\<phi>J \<psi>\<rangle>))"
+  by auto
+qed
+
+end \<comment> \<open>context @{locale Jeroslow_Diagonalization}\<close>
+
+
+subsection \<open>Jeroslow's Second Incompleteness Theorem\<close>
+
+text \<open>We follow Jeroslow's pseudo-term-based development of the
+Second Incompleteness Theorem and point out the location in the proof that
+implicitly uses an unstated assumption: the fact that, for certain two provably
+equivalent formulas @{term \<phi>} and @{term \<phi>'}, it is provable that
+the provability of the encoding of @{term \<phi>'} implies
+the provability of the encoding of @{term \<phi>}. \<close>
+
+locale Jeroslow_Godel_Second =
+Jeroslow_Diagonalization
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  dsj
+  num
+  prv
+  enc
+  F encF N ssap
++
+HBL1
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  eql cnj imp all exi
+  prv prv
+  enc
+  P
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and eql cnj imp all exi
+and fls
+and dsj
+and num
+and prv
+and enc ("\<langle>_\<rangle>")
+and P
+and F encF N ssap
++
+assumes
+SHBL3: "\<And>\<tau>. \<tau> \<in> ptrm 0 \<Longrightarrow> prv (imp (instInpP Pinp 0 \<tau>) (instInp Pinp \<langle>instInpP Pinp 0 \<tau>\<rangle>))"
+begin
+
+
+text \<open>Consistency formula a la Jeroslow:\<close>
+definition jcons :: "'fmla" where
+"jcons \<equiv> all xx (neg (cnj (instInp Pinp (Var xx))
+                           (instInpP Pinp 0 (instInp (encF N) (Var (xx))))))"
+
+lemma prv_eql_subst_trm3:
+"x \<in> var \<Longrightarrow> \<phi> \<in> fmla \<Longrightarrow> t1 \<in> trm \<Longrightarrow> t2 \<in> trm \<Longrightarrow>
+prv (eql t1 t2) \<Longrightarrow> prv (subst \<phi> t1 x) \<Longrightarrow> prv (subst \<phi> t2 x)"
+using prv_eql_subst_trm2
+  by (meson subst prv_imp_mp)
+
+lemma Pinp[simp,intro!]: "Pinp \<in> fmla"
+and Fvars_Pinp[simp]: "Fvars Pinp = {inp}"
+unfolding Pinp_def by auto
+
+lemma ReprF_combineWith_CapN:
+assumes "\<phi> \<in> fmla" and "Fvars \<phi> = {}"
+shows "prveqlPT (instInp (encF N) \<langle>\<phi>\<rangle>) \<langle>neg \<phi>\<rangle>"
+using assms unfolding CapN[symmetric, OF assms] by (intro ReprF) auto
+
+theorem jeroslow_godel_second:
+assumes consistent
+\<comment> \<open>Assumption that is not stated by Jeroslow, but seems to be needed:\<close>
+assumes unstated:
+        "let \<psi> = instInpP Pinp (Suc 0) (encF N);
+             \<tau> = \<tau>J \<psi>;
+             \<phi> = instInpP (instInpP Pinp (Suc 0) (encF N)) 0 \<tau>;
+             \<phi>' = instInpP Pinp 0 (instInpP (encF N) 0 \<tau>)
+         in prv (imp (instInp Pinp \<langle>\<phi>'\<rangle>) (instInp Pinp \<langle>\<phi>\<rangle>))"
+shows "\<not> prv jcons"
+proof
+  assume *: "prv jcons"
+
+  define \<psi> where "\<psi> \<equiv> instInpP Pinp (Suc 0) (encF N)"
+  define \<tau> where "\<tau> \<equiv> \<tau>J \<psi>"
+  define \<phi> where "\<phi> \<equiv> \<phi>J \<psi>"
+  have \<psi>[simp,intro]: "\<psi> \<in> fmla" "Fvars \<psi> = {inp}"
+  unfolding \<psi>_def by auto
+  have \<tau>[simp,intro]: "\<tau> \<in> ptrm 0" "\<tau> \<in> fmla" "Fvars \<tau> = {out}"
+    unfolding \<tau>_def by auto
+  have [simp]: "\<phi> \<in> fmla" "Fvars \<phi> = {}" unfolding \<phi>_def by auto
+
+  define eN\<tau> where "eN\<tau> \<equiv> instInpP (encF N) 0 \<tau>"
+  have eN\<tau>[simp]: "eN\<tau> \<in> ptrm 0" "eN\<tau> \<in> fmla" "Fvars eN\<tau> = {out}"
+   unfolding eN\<tau>_def by auto
+  define \<phi>' where "\<phi>' \<equiv> instInpP Pinp 0 eN\<tau>"
+  have [simp]: "\<phi>' \<in> fmla" "Fvars \<phi>' = {}" unfolding \<phi>'_def by auto
+
+  have \<phi>\<phi>': "prv (imp \<phi> \<phi>')" and \<phi>'\<phi>: "prv (imp \<phi>' \<phi>)" and \<phi>e\<phi>': "prv (eqv \<phi> \<phi>')"
+   unfolding \<phi>_def \<phi>J_def \<phi>'_def eN\<tau>_def \<tau>_def[symmetric] unfolding \<psi>_def
+   using prv_instInpP_compose[of Pinp "encF N" \<tau>] by auto
+
+  from diagonalization[OF \<psi>]
+  have "prveqlPT \<tau> \<langle>instInpP \<psi> 0 \<tau>\<rangle>" and **: "prv (eqv \<phi> (instInp \<psi> \<langle>\<phi>\<rangle>))"
+  unfolding \<tau>_def[symmetric] \<phi>_def[symmetric] by auto
+  have "**1": "prv (imp \<phi> (instInp \<psi> \<langle>\<phi>\<rangle>))" "prv (imp (instInp \<psi> \<langle>\<phi>\<rangle>) \<phi>)"
+   using prv_imp_eqvEL[OF _ _ **] prv_imp_eqvER[OF _ _ **] by auto
+
+  from SHBL3[OF eN\<tau>(1)]
+  have "prv (imp (instInpP Pinp 0 eN\<tau>) (instInp Pinp \<langle>instInpP Pinp 0 eN\<tau>\<rangle>))" .
+  hence "prv (imp \<phi>' (instInp Pinp \<langle>\<phi>'\<rangle>))" unfolding \<phi>'_def .
+  from prv_prv_imp_trans[OF _ _ _ \<phi>\<phi>' this]
+  have 0: "prv (imp \<phi> (instInp Pinp \<langle>\<phi>'\<rangle>))" by auto
+
+  note unr = unstated[unfolded Let_def
+    \<phi>_def[unfolded \<phi>J_def \<tau>_def[symmetric], symmetric] \<psi>_def[symmetric]
+      \<tau>_def[symmetric] eN\<tau>_def[symmetric] \<phi>'_def[symmetric] \<phi>J_def]
+
+  have 1: "prv (imp \<phi> (instInp Pinp \<langle>\<phi>\<rangle>))"
+  apply(nrule r: nprv_prvI)
+  apply(nrule r: nprv_impI)
+  apply(nrule r: nprv_addLemmaE[OF unr])
+  apply(nrule r: nprv_addImpLemmaE[OF 0])
+  apply(nrule r: nprv_clear3_3)
+  by (simp add: nprv_clear2_2 prv_nprv1I unr)
+
+  have 2: "prv (imp \<phi> (cnj (instInp Pinp \<langle>\<phi>\<rangle>)
+                           (instInp \<psi> \<langle>\<phi>\<rangle>)))"
+  apply(nrule r: nprv_prvI)
+  apply(nrule r: nprv_impI)
+  apply(nrule r: nprv_cnjI)
+  subgoal apply(nrule r: nprv_addImpLemmaE[OF 1]) .
+  subgoal apply(nrule r: nprv_addImpLemmaE[OF "**1"(1)]) . .
+
+  define z where "z \<equiv> Variable (Suc (Suc 0))"
+  have z_facts[simp]: "z \<in> var" "z \<noteq> xx" "z \<notin> Fvars Pinp"
+    "out \<noteq> z \<and> z \<noteq> out" "inp \<noteq> z \<and> z \<noteq> inp"
+   unfolding z_def by auto
+
+  have 30: "subst (instInpP Pinp 0 (instInp (encF N) (Var xx))) \<langle>\<phi>\<rangle> xx =
+            instInpP Pinp 0 (instInp (encF N) \<langle>\<phi>\<rangle>)"
+  unfolding z_def[symmetric] instInp_def instInpP_def Let_def
+  by (variousSubsts4 auto
+        s1: subst_compose_diff s2: subst_subst
+        s3: subst_notIn[of _ _ xx] s4: subst_compose_diff)
+  have 31: "subst (instInp Pinp (Var xx)) \<langle>\<phi>\<rangle> xx =
+            instInp Pinp \<langle>\<phi>\<rangle>" unfolding instInp_def by auto
+  have [simp]: "instInp (instInpP Pinp (Suc 0) (encF N)) \<langle>\<phi>\<rangle> =
+           instInpP Pinp 0 (instInp (encF N) \<langle>\<phi>\<rangle>)"
+  by (auto simp: instInp_instInpP \<psi>_def)
+
+  have 3: "prv (neg (cnj (instInp Pinp \<langle>\<phi>\<rangle>)
+                         (instInp \<psi> \<langle>\<phi>\<rangle>)))"
+  apply(nrule r: nprv_prvI)
+  apply(nrule r: nprv_addLemmaE[OF *, unfolded jcons_def])
+  apply(rule nprv_allE0[of _ _ _ "\<langle>\<phi>\<rangle>"], auto)
+  unfolding 30 31
+  apply(nrule r: nprv_clear2_2)
+  apply(nrule r: nprv_negI)
+  apply(nrule r: nprv_negE0)
+  apply(nrule r: nprv_clear2_2)
+  apply(nrule r: nprv_cnjE0)
+  apply(nrule r: nprv_clear3_3)
+  apply(nrule r: nprv_cnjI)
+  apply(nrule r: nprv_clear2_1)
+  unfolding \<psi>_def
+  apply(nrule r: nprv_hyp) .
+
+  have ***: "prv (neg \<phi>)"
+  apply(nrule r: nprv_prvI)
+  apply(nrule r: nprv_negI)
+  apply(nrule r: nprv_addImpLemmaE[OF 2])
+  apply(nrule r: nprv_addLemmaE[OF 3])
+  apply(nrule r: nprv_negE0) .
+
+  have 4: "prv (instInp Pinp \<langle>neg \<phi>\<rangle>)" using HBL1_inp[OF _ _ ***] by auto
+
+  have 5: "prveqlPT (instInp (encF N) \<langle>\<phi>\<rangle>) \<langle>neg \<phi>\<rangle>"
+    using ReprF_combineWith_CapN[of \<phi>] by auto
+
+  have [simp]: "instInp (encF N) \<langle>\<phi>\<rangle> \<in> ptrm 0" using instInp by auto
+
+  have 6: "prv (instInpP Pinp 0 (instInp (encF N) \<langle>\<phi>\<rangle>))"
+  apply(nrule r: nprv_prvI)
+  apply(nrule r: nprv_addLemmaE[OF 4])
+  apply(nrule r: prveqlPT_nprv_instInpP_instInp[OF _ _ _ _ _ 5]) .
+
+  note lem = "**1"(2)[unfolded \<psi>_def]
+  have "prv \<phi>"
+  apply(nrule r: nprv_prvI)
+  apply(nrule r: nprv_addLemmaE[OF 6])
+  apply(nrule r: nprv_addImpLemmaE[OF lem]) .
+
+  from this *** `consistent` show False unfolding consistent_def3 by auto
+qed
+
+end \<comment> \<open>context @{locale Jeroslow_Godel_Second}\<close>
+
+(*<*)
+end
+(*>*)
diff --git a/thys/Goedel_Incompleteness/Jeroslow_Simplified.thy b/thys/Goedel_Incompleteness/Jeroslow_Simplified.thy
new file mode 100644
--- /dev/null
+++ b/thys/Goedel_Incompleteness/Jeroslow_Simplified.thy
@@ -0,0 +1,380 @@
+section \<open>A Simplification of Jeroslow's Original Argument\<close>
+
+(*<*)
+theory Jeroslow_Simplified imports Abstract_Jeroslow_Encoding
+begin
+(*>*)
+
+text \<open>This is the simplified version of Jeroslow's Second Incompleteness Theorem
+reported in our CADE 2019 paper~\cite{DBLP:conf/cade/0001T19}.
+The simplification consists of replacing pseudo-terms with plain terms
+and representability with (what we call in the paper) term-representability.
+This simplified version does not incur the complications of the original.\<close>
+
+
+subsection \<open>Jeroslow-style term-based diagonalization\<close>
+
+locale Jeroslow_Diagonalization =
+Deduct_with_False
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  num
+  prv
++
+Encode
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  enc
++
+TermEncode
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  Ops tenc
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and eql cnj imp all exi
+and fls
+and num
+and prv
+and enc ("\<langle>_\<rangle>")
+and Ops and tenc
++
+fixes F :: "('trm \<Rightarrow> 'trm) set"
+  and encF :: "('trm \<Rightarrow> 'trm) \<Rightarrow> ('trm \<Rightarrow> 'trm)"
+  and N :: "'trm \<Rightarrow> 'trm"
+  and ssap :: "'fmla \<Rightarrow> 'trm \<Rightarrow> 'trm"
+assumes
+F[simp,intro!]: "\<And> f n. f \<in> F \<Longrightarrow> n \<in> num \<Longrightarrow> f n \<in> num"
+and
+encF[simp,intro!]: "\<And> f. f \<in> F \<Longrightarrow> encF f \<in> Ops"
+and
+N[simp,intro!]: "N \<in> F"
+and
+ssap[simp]: "\<And>\<phi>. \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {xx} \<Longrightarrow> ssap \<phi> \<in> F"
+and
+ReprF: "\<And>f n. f \<in> F \<Longrightarrow> n \<in> num \<Longrightarrow> prv (eql (encF f n) (f n))"
+and
+CapN: "\<And>\<phi>. \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> N \<langle>\<phi>\<rangle> = \<langle>neg \<phi>\<rangle>"
+and
+CapSS:
+"\<And> \<psi> f. \<psi> \<in> fmla \<Longrightarrow> Fvars \<psi> = {xx} \<Longrightarrow> f \<in> F \<Longrightarrow>
+    ssap \<psi> (tenc (encF f)) = \<langle>inst \<psi> (encF f (tenc (encF f)))\<rangle>"
+begin
+
+definition tJ :: "'fmla \<Rightarrow> 'trm" where
+"tJ \<psi> \<equiv> encF (ssap \<psi>) (tenc (encF (ssap \<psi>)))"
+
+definition \<phi>J :: "'fmla \<Rightarrow> 'fmla" where
+"\<phi>J \<psi> \<equiv> subst \<psi> (tJ \<psi>) xx"
+
+lemma tJ[simp]:
+assumes "\<psi> \<in> fmla" and "Fvars \<psi> = {xx}"
+shows "tJ \<psi> \<in> trm"
+using assms tJ_def by auto
+
+lemma FvarsT_tJ[simp]:
+assumes "\<psi> \<in> fmla" and "Fvars \<psi> = {xx}"
+shows "FvarsT (tJ \<psi>) = {}"
+using assms tJ_def by auto
+
+lemma \<phi>J[simp]:
+assumes "\<psi> \<in> fmla" and "Fvars \<psi> = {xx}"
+shows "\<phi>J \<psi> \<in> fmla"
+using assms \<phi>J_def by auto
+
+lemma Fvars_\<phi>J[simp]:
+assumes "\<psi> \<in> fmla" and "Fvars \<psi> = {xx}"
+shows "Fvars (\<phi>J \<psi>) = {}"
+using assms \<phi>J_def by auto
+
+lemma diagonalization:
+assumes "\<psi> \<in> fmla" and "Fvars \<psi> = {xx}"
+shows "prv (eql (tJ \<psi>) \<langle>inst \<psi> (tJ \<psi>)\<rangle>) \<and>
+       prv (eqv (\<phi>J \<psi>) (inst \<psi> \<langle>\<phi>J \<psi>\<rangle>))"
+proof
+  define fJ where "fJ \<equiv> ssap \<psi>"
+  have fJ[simp]: "fJ \<in> F" unfolding fJ_def using assms by auto
+  have "fJ (tenc (encF fJ)) = \<langle>inst \<psi> (tJ \<psi>)\<rangle>"
+   by (simp add: CapSS assms fJ_def tJ_def)
+  thus **: "prv (eql (tJ \<psi>) \<langle>inst \<psi> (tJ \<psi>)\<rangle>)"
+   using ReprF fJ fJ_def tJ_def by fastforce
+  show "prv (eqv (\<phi>J \<psi>) (inst \<psi> \<langle>\<phi>J \<psi>\<rangle>))"
+   using assms prv_eql_subst_trm_eqv[OF xx _  _ _ **, of "\<psi>"]
+   by (auto simp: \<phi>J_def inst_def)
+qed
+
+end \<comment> \<open>context @{locale Jeroslow_Diagonalization}\<close>
+
+
+subsection \<open>Term-based version of Jeroslow's Second Incompleteness Theorem\<close>
+
+locale Jeroslow_Godel_Second =
+Jeroslow_Diagonalization
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  num
+  prv
+  enc
+  Ops tenc
+  F encF N ssap
++
+HBL1
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  eql cnj imp all exi
+  prv prv
+  enc
+  P
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and eql cnj imp all exi
+and fls
+and num
+and prv
+and enc ("\<langle>_\<rangle>")
+and Ops and tenc
+and P
+and F encF N ssap
++
+assumes
+SHBL3: "\<And>t. t \<in> trm \<Longrightarrow> FvarsT t = {} \<Longrightarrow> prv (imp (PP t) (PP \<langle>PP t\<rangle>))"
+begin
+
+text \<open>Consistency formula a la Jeroslow:\<close>
+definition jcons :: "'fmla" where
+"jcons \<equiv> all xx (neg (cnj (PP (Var xx)) (PP (encF N (Var (xx))))))"
+
+lemma prv_eql_subst_trm3:
+"x \<in> var \<Longrightarrow> \<phi> \<in> fmla \<Longrightarrow> t1 \<in> trm \<Longrightarrow> t2 \<in> trm \<Longrightarrow>
+prv (eql t1 t2) \<Longrightarrow> prv (subst \<phi> t1 x) \<Longrightarrow> prv (subst \<phi> t2 x)"
+using prv_eql_subst_trm2
+  by (meson subst prv_imp_mp)
+
+lemma prv_eql_neg_encF_N:
+assumes "\<phi> \<in> fmla" and "Fvars \<phi> = {}"
+shows "prv (eql \<langle>neg \<phi>\<rangle> (encF N \<langle>\<phi>\<rangle>))"
+  unfolding CapN[symmetric, OF assms]
+  by (rule prv_prv_eql_sym) (auto simp: assms intro: ReprF)
+
+lemma prv_imp_neg_encF_N_aux:
+assumes "\<phi> \<in> fmla" and "Fvars \<phi> = {}"
+shows "prv (imp (PP \<langle>neg \<phi>\<rangle>) (PP (encF N \<langle>\<phi>\<rangle>)))"
+using assms prv_eql_subst_trm2[OF _ _ _ _ prv_eql_neg_encF_N[OF assms],
+  of xx "PP (Var xx)"]
+  unfolding PP_def by auto
+
+lemma prv_cnj_neg_encF_N_aux:
+assumes "\<phi> \<in> fmla" and "Fvars \<phi> = {}" "\<chi> \<in> fmla" "Fvars \<chi> = {}"
+and "prv (neg (cnj \<chi> (PP \<langle>neg \<phi>\<rangle>)))"
+shows"prv (neg (cnj \<chi> (PP (encF N \<langle>\<phi>\<rangle>))))"
+using assms prv_eql_subst_trm3[OF _ _ _ _ prv_eql_neg_encF_N,
+  of xx "neg (cnj \<chi> (PP (Var xx)))"]
+  unfolding PP_def by auto
+
+theorem jeroslow_godel_second:
+assumes consistent
+shows "\<not> prv jcons"
+proof
+  assume *: "prv jcons"
+  define \<psi> where "\<psi> \<equiv> PP (encF N (Var xx))"
+  define t where "t \<equiv> tJ \<psi>"
+  have \<psi>[simp,intro]: "\<psi> \<in> fmla" "Fvars \<psi> = {xx}"
+  and t[simp,intro]: "t \<in> trm" "FvarsT t = {}"
+    unfolding \<psi>_def t_def by auto
+
+  have sPP[simp]: "subst (PP (encF N (Var xx))) \<langle>PP (encF N t)\<rangle> xx =
+             PP (encF N \<langle>PP (encF N t)\<rangle>)"
+    unfolding PP_def by (subst subst_compose_eq_or) auto
+  have sPP2[simp]: "subst (PP (encF N (Var xx))) t xx = PP (encF N t)"
+    unfolding PP_def by (subst subst_compose_eq_or) auto
+  have 00: "PP (encF N t) = inst \<psi> t" unfolding \<psi>_def inst_def PP_def
+    by (subst subst_compose_eq_or) auto
+
+  define \<phi> where "\<phi> \<equiv> \<phi>J \<psi>"
+  have [simp]: "\<phi> \<in> fmla" "Fvars \<phi> = {}" unfolding \<phi>_def by auto
+  have **: "prv (eql t \<langle>\<phi>\<rangle>)"
+    unfolding 00 \<phi>_def
+    using \<phi>J_def diagonalization inst_def t_def by auto
+  have \<phi>: "\<phi> = PP (encF N t)" unfolding \<phi>_def \<phi>J_def t_def \<psi>_def
+    using sPP2 \<psi>_def t_def by blast
+  have 1: "prv (imp \<phi> (PP \<langle>\<phi>\<rangle>))" using SHBL3[of "encF N t"]
+    using 00 \<phi>J_def \<phi>_def \<psi>_def inst_def t_def by auto
+  have eqv_\<phi>: "prv (eqv \<phi> (PP (encF N \<langle>\<phi>\<rangle>)))"  using diagonalization
+    by (metis "00" sPP \<phi>J_def \<phi>_def \<psi> \<psi>_def diagonalization inst_def t_def)
+  have 2: "prv (imp \<phi> (PP (encF N \<langle>\<phi>\<rangle>)))"
+   using prv_cnjEL[OF _ _ eqv_\<phi>[unfolded eqv_def]] by auto
+  have "prv (imp (PP (encF N \<langle>\<phi>\<rangle>)) \<phi>)"
+   using prv_cnjER[OF _ _ eqv_\<phi>[unfolded eqv_def]] by auto
+  from  prv_prv_imp_trans[OF _ _ _ prv_imp_neg_encF_N_aux this]
+  have 22: "prv (imp (PP \<langle>neg \<phi>\<rangle>) \<phi>)" by auto
+  have 3: "prv (imp \<phi> (cnj (PP \<langle>\<phi>\<rangle>) (PP (encF N \<langle>\<phi>\<rangle>))))"
+    by (rule prv_imp_cnj[OF _ _ _ 1 2]) (auto simp: \<phi>_def)
+  have 4: "prv (neg (cnj (PP \<langle>\<phi>\<rangle>) (PP (encF N \<langle>\<phi>\<rangle>))))"
+     using prv_allE[OF _ _ _ *[unfolded jcons_def], of "\<langle>\<phi>\<rangle>"]
+  by (simp add: \<phi> \<psi>_def)
+  have 5: "prv (neg \<phi>)"
+    unfolding neg_def
+    by (rule prv_prv_imp_trans[OF _ _ _ 3 4[unfolded neg_def]]) auto
+  hence "prv (PP \<langle>neg \<phi>\<rangle>)" using
+      HBL1_PP[OF _ _ 5] by auto
+  hence "prv \<phi>" using prv_imp_mp[OF _ _ 22] by auto
+  with 5 assms show False unfolding consistent_def3 by auto
+qed
+
+
+subsection \<open>A variant of the Second Incompleteness Theorem\<close>
+
+text \<open>This variant (also discussed in our CADE 2019 paper~\cite{DBLP:conf/cade/0001T19}) strengthens
+the conclusion of the theorem to the standard formulation
+of "does not prove its own consistency" at the expense of two
+additional derivability-like conditions, HBL4 and WHBL2.\<close>
+
+theorem jeroslow_godel_second_standardCon:
+assumes consistent
+and HBL4: "\<And>\<phi>1 \<phi>2. {\<phi>1,\<phi>2} \<subseteq> fmla \<Longrightarrow> Fvars \<phi>1 = {} \<Longrightarrow> Fvars \<phi>2 = {} \<Longrightarrow>
+   prv (imp (cnj (PP \<langle>\<phi>1\<rangle>) (PP \<langle>\<phi>2\<rangle>)) (PP \<langle>cnj \<phi>1 \<phi>2\<rangle>))"
+and WHBL2: "\<And>\<phi>1 \<phi>2. {\<phi>1,\<phi>2} \<subseteq> fmla \<Longrightarrow> Fvars \<phi>1 = {} \<Longrightarrow> Fvars \<phi>2 = {} \<Longrightarrow>
+   prv (imp \<phi>1 \<phi>2) \<Longrightarrow> prv (imp (PP \<langle>\<phi>1\<rangle>) (PP \<langle>\<phi>2\<rangle>))"
+shows "\<not> prv (neg (PP \<langle>fls\<rangle>))"
+proof
+  assume *:  "prv (neg (PP \<langle>fls\<rangle>))"
+  define \<psi> where "\<psi> \<equiv> PP (encF N (Var xx))"
+  define t where "t \<equiv> tJ \<psi>"
+  have \<psi>[simp,intro]: "\<psi> \<in> fmla" "Fvars \<psi> = {xx}"
+  and t[simp,intro]: "t \<in> trm" "FvarsT t = {}"
+    unfolding \<psi>_def t_def by auto
+
+  have [simp]: "subst (PP (encF N (Var xx))) \<langle>PP (encF N t)\<rangle> xx =
+             PP (encF N \<langle>PP (encF N t)\<rangle>)"
+    unfolding PP_def by (subst subst_compose_eq_or) auto
+  have [simp]: "subst (PP (encF N (Var xx))) t xx = PP (encF N t)"
+    unfolding PP_def by (subst subst_compose_eq_or) auto
+  have 00: "PP (encF N t) = inst \<psi> t" unfolding \<psi>_def inst_def PP_def
+    by (subst subst_compose_eq_or) auto
+
+  define \<phi> where "\<phi> = PP (encF N t)"
+  have [simp]: "\<phi> \<in> fmla" "Fvars \<phi> = {}" unfolding \<phi>_def by auto
+  have **: "prv (eql t \<langle>PP (encF N t)\<rangle>)"
+    unfolding 00 by (simp add: diagonalization t_def)
+  have 1: "prv (imp \<phi> (PP \<langle>\<phi>\<rangle>))" using SHBL3[of "encF N t"]
+    by (auto simp: \<phi>_def)
+  have 2: "prv (imp \<phi> (PP (encF N \<langle>\<phi>\<rangle>)))"
+   using prv_eql_subst_trm2[OF xx _  _ _ **, of "PP (encF N (Var xx))"]
+   by (auto simp: \<phi>_def)
+  have "prv (imp (PP (encF N \<langle>\<phi>\<rangle>)) \<phi>)"
+   using prv_eql_subst_trm_rev2[OF xx _  _ _ **, of "PP (encF N (Var xx))"]
+   by (auto simp: \<phi>_def)
+  from prv_prv_imp_trans[OF _ _ _ prv_imp_neg_encF_N_aux this]
+  have 22: "prv (imp (PP \<langle>neg \<phi>\<rangle>) \<phi>)" by auto
+  have 3: "prv (imp \<phi> (cnj (PP \<langle>\<phi>\<rangle>) (PP (encF N \<langle>\<phi>\<rangle>))))"
+    by (rule prv_imp_cnj[OF _ _ _ 1 2]) (auto simp: \<phi>_def)
+
+  \<comment> \<open>This is the modification from the proof of @{thm jeroslow_godel_second}:\<close>
+  have 41: "prv (imp (cnj (PP \<langle>\<phi>\<rangle>) (PP \<langle>neg \<phi>\<rangle>)) (PP \<langle>cnj \<phi> (neg \<phi>)\<rangle>))"
+  using HBL4[of \<phi> "neg \<phi>"] by auto
+  have "prv (imp (cnj \<phi> (neg \<phi>)) (fls))"
+    by (simp add: prv_cnj_imp_monoR2 prv_imp_neg_fls)
+  from WHBL2[OF _ _ _ this]
+  have 42: "prv (imp (PP \<langle>cnj \<phi> (neg \<phi>)\<rangle>) (PP \<langle>fls\<rangle>))" by auto
+  from prv_prv_imp_trans[OF _ _ _ 41 42]
+  have "prv (imp (cnj (PP \<langle>\<phi>\<rangle>) (PP \<langle>neg \<phi>\<rangle>)) (PP \<langle>fls\<rangle>))" by auto
+  from prv_prv_imp_trans[OF _ _ _ this *[unfolded neg_def]]
+  have "prv (neg (cnj (PP \<langle>\<phi>\<rangle>) (PP \<langle>neg \<phi>\<rangle>)))"
+  unfolding neg_def by auto
+  from prv_cnj_neg_encF_N_aux[OF _ _ _ _ this]
+  have 4: "prv (neg (cnj (PP \<langle>\<phi>\<rangle>) (PP (encF N \<langle>\<phi>\<rangle>))))" by auto
+  \<comment> \<open>End modification\<close>
+
+  have 5: "prv (neg \<phi>)"
+    unfolding neg_def
+    by (rule prv_prv_imp_trans[OF _ _ _ 3 4[unfolded neg_def]]) auto
+  hence "prv (PP \<langle>neg \<phi>\<rangle>)" using HBL1_PP[OF _ _ 5] by auto
+  hence "prv \<phi>" using prv_imp_mp[OF _ _ 22] by auto
+  with 5 assms show False unfolding consistent_def3 by auto
+qed
+
+text \<open>Next we perform a formal analysis of some connection between the
+above theorems' hypotheses.\<close>
+
+definition noContr :: bool where
+"noContr \<equiv> \<forall> \<phi> \<in> fmla. Fvars \<phi> = {} \<longrightarrow> prv (neg (cnj (PP \<langle>\<phi>\<rangle>) (PP \<langle>neg \<phi>\<rangle>)))"
+
+lemma jcons_noContr:
+assumes j: "prv jcons"
+shows "noContr"
+unfolding noContr_def proof safe
+  fix \<phi> assume \<phi>[simp]: "\<phi> \<in> fmla" "Fvars \<phi> = {}"
+  have [simp]: "subst (PP (encF N (Var xx))) \<langle>\<phi>\<rangle> xx =
+               PP (encF N \<langle>\<phi>\<rangle>)"
+  unfolding PP_def by (simp add: subst_compose_same)
+  note j = allE_id[OF _ _ j[unfolded jcons_def], simplified]
+  have 0: "prv (neg (cnj (PP \<langle>\<phi>\<rangle>)
+                         (PP (encF N \<langle>\<phi>\<rangle>))))"
+  (is "prv (neg (cnj (PP \<langle>\<phi>\<rangle>) ?j))")
+    using prv_subst[OF _ _ _ j, of xx "\<langle>\<phi>\<rangle>"] by simp
+  have 1: "prv (imp (PP \<langle>neg \<phi>\<rangle>) ?j)"
+  using prv_eql_neg_encF_N[of \<phi>, simplified]
+  using prv_imp_neg_encF_N_aux by auto
+  have 2: "prv (imp (cnj (PP \<langle>\<phi>\<rangle>) (PP \<langle>neg \<phi>\<rangle>))
+                    (cnj (PP \<langle>\<phi>\<rangle>) ?j))"
+  using 0 1 by (simp add:  prv_cnj_mono prv_imp_refl)
+
+  have "prv (imp (cnj (PP \<langle>\<phi>\<rangle>) (PP \<langle>neg \<phi>\<rangle>))
+                 (cnj (PP \<langle>\<phi>\<rangle>) ?j))"
+    by (simp add: 2 prv_cnj_mono prv_imp_refl)
+  thus "prv (neg (cnj (PP \<langle>\<phi>\<rangle>) (PP \<langle>neg \<phi>\<rangle>)))" using 0
+    unfolding neg_def
+    by (elim prv_prv_imp_trans[rotated 3]) auto
+qed
+
+text \<open>@{term noContr} is still stronger than the standard notion of proving own consistency:\<close>
+
+lemma noContr_implies_neg_PP_fls:
+ assumes "noContr"
+ shows "prv (neg (PP \<langle>fls\<rangle>))"
+proof-
+  have "prv (neg (cnj (PP \<langle>fls\<rangle>) (PP \<langle>neg fls\<rangle>)))"
+    using assms unfolding noContr_def by auto
+  thus ?thesis
+  using Fvars_tru enc in_num tru_def PP PP_def fls imp HBL1 neg_def
+       prv_cnj_imp prv_fls prv_imp_com prv_imp_mp
+  by (metis Encode.enc HBL1_axioms HBL1_def)
+qed
+
+corollary jcons_implies_neg_PP_fls:
+assumes "prv jcons"
+shows "prv (neg (PP \<langle>fls\<rangle>))"
+by (simp add: assms noContr_implies_neg_PP_fls jcons_noContr)
+
+text \<open>However, unlike @{term jcons}, which seems to be quite a bit stronger,
+@{term noContr} is equivalent to the standard notion under a slightly
+stronger assumption than our WWHBL2, namely, a binary version of that:\<close>
+
+lemma neg_PP_fls_implies_noContr:
+ assumes WWHBL22:
+"\<And>\<phi> \<chi> \<psi>. \<phi> \<in> fmla \<Longrightarrow> \<chi> \<in> fmla \<Longrightarrow> \<psi> \<in> fmla \<Longrightarrow>
+   Fvars \<phi> = {} \<Longrightarrow> Fvars \<chi> = {} \<Longrightarrow> Fvars \<psi> = {} \<Longrightarrow>
+   prv (imp \<phi> (imp \<chi> \<psi>)) \<Longrightarrow> prv (imp (PP \<langle>\<phi>\<rangle>) (imp (PP \<langle>\<chi>\<rangle>) (PP \<langle>\<psi>\<rangle>)))"
+ assumes p: "prv (neg (PP \<langle>fls\<rangle>))"
+ shows "noContr"
+unfolding noContr_def proof safe
+  fix \<phi> assume \<phi>[simp]: "\<phi> \<in> fmla" "Fvars \<phi> = {}"
+  have 0: "prv (imp \<phi> (imp (neg \<phi>) fls))"
+    by (simp add: prv_imp_neg_fls)
+  have 1: "prv (imp (PP \<langle>\<phi>\<rangle>) (imp (PP \<langle>neg \<phi>\<rangle>) (PP \<langle>fls\<rangle>)))"
+    using WWHBL22[OF _ _ _ _ _ _ 0] by auto
+  show "prv (neg (cnj (PP \<langle>\<phi>\<rangle>) (PP \<langle>neg \<phi>\<rangle>)))" using 1 p
+    unfolding neg_def
+    by (elim prv_cnj_imp_monoR2[rotated 3, OF prv_prv_imp_trans[rotated 3]])
+      (auto intro!: prv_imp_monoL)
+qed
+
+end \<comment> \<open>context @{locale Jeroslow_Godel_Second}\<close>
+
+(*<*)
+end
+(*>*)
diff --git a/thys/Goedel_Incompleteness/Loeb.thy b/thys/Goedel_Incompleteness/Loeb.thy
new file mode 100644
--- /dev/null
+++ b/thys/Goedel_Incompleteness/Loeb.thy
@@ -0,0 +1,121 @@
+chapter \<open>Löb's Theorem\<close>
+
+(*<*)
+theory Loeb imports Loeb_Formula Derivability_Conditions
+begin
+(*>*)
+
+text \<open>We have set up the formalization of Gödel's first (easy half) and Gödel's second
+so that the following generalizations, leading to Löb's theorem, are trivial
+modifications of these, replacing negation with "implies @{term \<phi>}" in all proofs.\<close>
+
+locale Loeb_Assumptions =
+HBL1_2_3
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  eql cnj imp all exi
+  prv bprv
+  enc
+  P
++
+Loeb_Form
+  var trm fmla Var num FvarsT substT Fvars subst
+  eql cnj imp all exi
+  prv bprv
+  enc
+  S
+  P
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var num FvarsT substT Fvars subst
+and eql cnj imp all exi
+and prv bprv
+and enc ("\<langle>_\<rangle>")
+and S
+and P
+begin
+
+text \<open>Generalization of $\mathit{goedel\_first\_theEasyHalf\_pos}$, replacing @{term fls} with a sentence @{term \<phi>}:\<close>
+lemma loeb_aux_prv:
+assumes \<phi>[simp]: "\<phi> \<in> fmla" "Fvars \<phi> = {}" and p: "prv (\<phi>L \<phi>)"
+shows "prv \<phi>"
+proof-
+  have "prv (imp (PP \<langle>\<phi>L \<phi>\<rangle>) \<phi>)" using assms prv_eqv_prv[OF _ _ p prv_\<phi>L_eqv] by auto
+  moreover have "bprv (PP \<langle>\<phi>L \<phi>\<rangle>)" using HBL1[OF \<phi>L[OF \<phi>] _ p] unfolding PP_def by simp
+  from bprv_prv[OF _ _ this, simplified] have "prv (PP \<langle>\<phi>L \<phi>\<rangle>)" .
+  ultimately show ?thesis using PP \<phi>L by (meson assms enc in_num prv_imp_mp)
+qed
+
+lemma loeb_aux_bprv:
+assumes \<phi>[simp]: "\<phi> \<in> fmla" "Fvars \<phi> = {}" and p: "bprv (\<phi>L \<phi>)"
+shows "bprv \<phi>"
+proof-
+  note pp = bprv_prv[OF _ _ p, simplified]
+  have "bprv (imp (PP \<langle>\<phi>L \<phi>\<rangle>) \<phi>)" using assms B.prv_eqv_prv[OF _ _ p bprv_\<phi>L_eqv] by auto
+  moreover have "bprv (PP \<langle>\<phi>L \<phi>\<rangle>)" using HBL1[OF \<phi>L[OF \<phi>] _ pp] unfolding PP_def by simp
+  ultimately show ?thesis using PP \<phi>L by (meson assms enc in_num B.prv_imp_mp)
+qed
+
+text \<open>Generalization of $\mathit{P\_G}$, the main lemma used for Gödel's second:\<close>
+lemma P_L:
+assumes \<phi>[simp]: "\<phi> \<in> fmla" "Fvars \<phi> = {}"
+shows "bprv (imp (PP \<langle>\<phi>L \<phi>\<rangle>) (PP \<langle>\<phi>\<rangle>))"
+proof-
+  have 0: "prv (imp (\<phi>L \<phi>) (imp (PP \<langle>\<phi>L \<phi>\<rangle>) \<phi>))"
+    using prv_\<phi>L_eqv by (intro prv_imp_eqvEL) auto
+  have 1: "bprv (PP \<langle>imp (\<phi>L \<phi>) (imp (PP \<langle>\<phi>L \<phi>\<rangle>) \<phi>)\<rangle>)"
+    using HBL1_PP[OF _ _ 0] by simp
+  have 2: "bprv (imp (PP \<langle>\<phi>L \<phi>\<rangle>) (PP \<langle>imp (PP \<langle>\<phi>L \<phi>\<rangle>) \<phi>\<rangle>))"
+  using HBL2_imp2[OF _ _ _ _ 1] by simp
+  have 3: "bprv (imp (PP \<langle>\<phi>L \<phi>\<rangle>) (PP \<langle>PP \<langle>\<phi>L \<phi>\<rangle>\<rangle>))"
+    using HBL3[OF \<phi>L[OF \<phi>] _] by simp
+  have 23: "bprv (imp (PP \<langle>\<phi>L \<phi>\<rangle>)
+                      (cnj (PP \<langle>PP \<langle>\<phi>L \<phi>\<rangle>\<rangle>)
+                           (PP \<langle>imp (PP \<langle>\<phi>L \<phi>\<rangle>) \<phi>\<rangle>)))"
+  using B.prv_imp_cnj[OF _ _ _ 3 2] by simp
+  have 4: "bprv (imp (cnj (PP \<langle>PP \<langle>\<phi>L \<phi>\<rangle>\<rangle>)
+                          (PP \<langle>imp (PP \<langle>\<phi>L \<phi>\<rangle>) \<phi>\<rangle>))
+                    (PP \<langle>\<phi>\<rangle>))"
+    using HBL2[of "PP \<langle>\<phi>L \<phi>\<rangle>" \<phi>] by simp
+  show ?thesis using B.prv_prv_imp_trans[OF _ _ _ 23 4] by simp
+qed
+
+text \<open>Löb's theorem generalizes the positive formulation Gödel's Second
+($\mathit{goedel\_second}$). In our two-provability-relation framework, we get two variants of Löb's theorem.
+A stronger variant, assuming @{term prv} and proving @{term bprv}, seems impossible.\<close>
+
+theorem loeb_bprv:
+assumes \<phi>[simp]: "\<phi> \<in> fmla" "Fvars \<phi> = {}" and p: "bprv (imp (PP \<langle>\<phi>\<rangle>) \<phi>)"
+shows "bprv \<phi>"
+proof-
+  have "bprv (imp (PP \<langle>\<phi>L \<phi>\<rangle>) \<phi>)"
+    by (rule B.prv_prv_imp_trans[OF _ _ _ P_L p]) auto
+  hence "bprv (\<phi>L \<phi>)"
+    by (rule B.prv_eqv_prv_rev[OF _ _ _ bprv_\<phi>L_eqv, rotated 2]) auto
+  thus ?thesis using loeb_aux_bprv[OF \<phi>] by simp
+qed
+
+theorem loeb_prv:
+assumes \<phi>[simp]: "\<phi> \<in> fmla" "Fvars \<phi> = {}" and p: "prv (imp (PP \<langle>\<phi>\<rangle>) \<phi>)"
+shows "prv \<phi>"
+proof-
+  note PL = bprv_prv[OF _ _ P_L, simplified]
+  have "prv (imp (PP \<langle>\<phi>L \<phi>\<rangle>) \<phi>)"
+    by (rule prv_prv_imp_trans[OF _ _ _ PL p]) auto
+  hence "prv (\<phi>L \<phi>)"
+    by (rule prv_eqv_prv_rev[OF _ _ _ prv_\<phi>L_eqv, rotated 2]) auto
+  thus ?thesis using loeb_aux_prv[OF \<phi>] by simp
+qed
+
+text \<open>We could have of course inferred $\mathit{goedel\_first\_theEasyHalf\_pos}$
+and $\mathit{goedel\_second}$ from these more general versions, but we leave the original
+arguments as they are more instructive.\<close>
+
+end \<comment> \<open>context @{locale Loeb_Assumptions}\<close>
+
+(*<*)
+end
+(*>*)
+
+
+
diff --git a/thys/Goedel_Incompleteness/Loeb_Formula.thy b/thys/Goedel_Incompleteness/Loeb_Formula.thy
new file mode 100644
--- /dev/null
+++ b/thys/Goedel_Incompleteness/Loeb_Formula.thy
@@ -0,0 +1,63 @@
+chapter \<open>Löb  Formulas\<close>
+
+(*<*)
+theory Loeb_Formula imports Diagonalization Derivability_Conditions
+begin
+(*>*)
+
+text \<open>The Löb formula, parameterized by a sentence @{term \<phi>}, is defined by diagonalizing @{term "imp P \<phi>"}.\<close>
+
+
+locale Loeb_Form =
+Deduct2
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  eql cnj imp all exi
+  prv bprv
++
+Repr_SelfSubst
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  eql cnj imp all exi
+  prv bprv
+  enc
+  S
++
+HBL1
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  eql cnj imp all exi
+  prv bprv
+  enc
+  P
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var num FvarsT substT Fvars subst
+and eql cnj imp all exi
+and prv bprv
+and enc ("\<langle>_\<rangle>")
+and S
+and P
+begin
+
+text \<open>The Löb formula associated to a formula @{term \<phi>}:\<close>
+definition \<phi>L :: "'fmla \<Rightarrow> 'fmla" where "\<phi>L \<phi> \<equiv> diag (imp P \<phi>)"
+
+lemma \<phi>L[simp,intro]: "\<And>\<phi>. \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> \<phi>L \<phi> \<in> fmla"
+and
+Fvars_\<phi>L[simp]: "\<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> Fvars (\<phi>L \<phi>) = {}"
+  unfolding \<phi>L_def PP_def by auto
+
+lemma bprv_\<phi>L_eqv:
+"\<phi> \<in> fmla \<Longrightarrow> Fvars \<phi>  = {} \<Longrightarrow> bprv (eqv (\<phi>L \<phi>) (imp (PP \<langle>\<phi>L \<phi>\<rangle>) \<phi>))"
+  unfolding \<phi>L_def PP_def using bprv_diag_eqv[of "imp P \<phi>"] by auto
+
+lemma prv_\<phi>L_eqv:
+"\<phi> \<in> fmla \<Longrightarrow> Fvars \<phi>  = {} \<Longrightarrow> prv (eqv (\<phi>L \<phi>) (imp (PP \<langle>\<phi>L \<phi>\<rangle>) \<phi>))"
+  using bprv_prv[OF _ _ bprv_\<phi>L_eqv, simplified] by auto
+
+end \<comment> \<open>context @{locale Loeb_Form}\<close>
+
+(*<*)
+end
+(*>*)
diff --git a/thys/Goedel_Incompleteness/ROOT b/thys/Goedel_Incompleteness/ROOT
new file mode 100644
--- /dev/null
+++ b/thys/Goedel_Incompleteness/ROOT
@@ -0,0 +1,10 @@
+chapter AFP
+
+session Goedel_Incompleteness (AFP) = Syntax_Independent_Logic +
+  description \<open>The Abstract Incompleteness Theorems\<close>
+  options [timeout = 600]
+  theories
+    All_Abstract
+  document_files
+    "root.tex"
+    "root.bib"
diff --git a/thys/Goedel_Incompleteness/Rosser_Formula.thy b/thys/Goedel_Incompleteness/Rosser_Formula.thy
new file mode 100644
--- /dev/null
+++ b/thys/Goedel_Incompleteness/Rosser_Formula.thy
@@ -0,0 +1,183 @@
+chapter \<open>Rosser Formulas\<close>
+
+text \<open>The Rosser formula is a modification of the Gödel formula that
+is undecidable assuming consistency only (not $\omega$-consistency).\<close>
+
+(*<*)
+theory Rosser_Formula
+  imports Diagonalization Goedel_Formula
+begin
+(*>*)
+
+locale Rosser_Form =
+Deduct2_with_PseudoOrder
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  dsj
+  num
+  prv bprv
+  Lq
+  +
+Repr_Neg
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  num
+  prv bprv
+  enc
+  N
+  +
+Repr_SelfSubst
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  eql cnj imp all exi
+  prv bprv
+  enc
+  S
+  +
+HBL1
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  eql cnj imp all exi
+  prv bprv
+  enc
+  P
+  for
+    var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+    and Var FvarsT substT Fvars subst
+    and num
+    and eql cnj imp all exi
+    and fls
+    and prv bprv
+    and Lq
+    and dsj
+    and enc ("\<langle>_\<rangle>")
+    and N S P
+
+
+locale Rosser_Form_Proofs =
+Deduct2_with_PseudoOrder
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  dsj
+  num
+  prv bprv
+  Lq
+  +
+Repr_Neg
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  num
+  prv bprv
+  enc
+  N
+  +
+Repr_SelfSubst
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  eql cnj imp all exi
+  prv bprv
+  enc
+  S
+  +
+CleanRepr_Proofs
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  eql cnj imp all exi
+  prv bprv
+  enc
+  fls
+  dsj
+  "proof" prfOf
+  encPf
+  Pf
+  for
+    var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+    and Var FvarsT substT Fvars subst
+    and num
+    and eql cnj imp all exi
+    and fls
+    and prv bprv
+    and Lq
+    and dsj and "proof" :: "'proof set" and prfOf
+    and enc ("\<langle>_\<rangle>")
+    and N
+    and S
+    and encPf Pf
+
+context Rosser_Form_Proofs
+begin
+
+definition R where "R = all zz (imp (LLq (Var zz) (Var yy))
+                                     (all xx' (imp (NN (Var xx) (Var xx'))
+                                                   (neg (PPf (Var zz) (Var xx'))))))"
+
+definition RR where "RR t1 t2 = psubst R [(t1,yy), (t2,xx)]"
+
+lemma R[simp,intro!]: "R \<in> fmla" unfolding R_def by auto
+
+lemma RR_def2:
+  "t1 \<in> trm \<Longrightarrow> t2 \<in> trm \<Longrightarrow> xx \<notin> FvarsT t1 \<Longrightarrow> RR t1 t2 = subst (subst R t1 yy) t2 xx"
+  unfolding RR_def by (rule psubst_eq_rawpsubst2[simplified]) auto
+
+definition P' where "P' = exi yy (cnj (PPf (Var yy) (Var xx)) (RR (Var yy) (Var xx)))"
+
+definition PP' where "PP' t = subst P' t xx"
+
+lemma Fvars_R[simp]: "Fvars R = {xx,yy}" unfolding R_def by auto
+
+lemma [simp]: "Fvars (RR (Var yy) (Var xx)) = {yy,xx}" by (auto simp: RR_def2)
+
+lemma P'[simp,intro!]: "P' \<in> fmla" unfolding P'_def by (auto simp: PPf_def2 RR_def2)
+
+lemma Fvars_P'[simp]: "Fvars P' = {xx}" unfolding P'_def by (auto simp: PPf_def2 RR_def2)
+
+lemma PP'[simp,intro!]: "t \<in> trm \<Longrightarrow> PP' t \<in> fmla"
+  unfolding PP'_def by auto
+
+lemma RR[simp,intro]: "t1 \<in> trm \<Longrightarrow> t2 \<in> trm \<Longrightarrow> RR t1 t2 \<in> fmla"
+  by (auto simp: RR_def)
+
+lemma RR_simps[simp]:
+   "n \<in> num \<Longrightarrow> subst (RR (Var yy) (Var xx)) n xx = RR (Var yy) n"
+   "m \<in> num \<Longrightarrow> n \<in> num \<Longrightarrow> subst (RR (Var yy) m) n yy = RR n m"
+  by (simp add: RR_def2 subst2_fresh_switch)+
+
+
+text \<open>The Rosser modification of the Gödel formula\<close>
+definition \<phi>R :: 'fmla where "\<phi>R \<equiv> diag (neg P')"
+
+lemma \<phi>R[simp,intro!]: "\<phi>R \<in> fmla" and Fvars_\<phi>R[simp]: "Fvars \<phi>R = {}"
+  unfolding \<phi>R_def wrepr.PP_def by auto
+
+lemma bprv_\<phi>R_eqv:
+  "bprv (eqv \<phi>R (neg (PP' \<langle>\<phi>R\<rangle>)))"
+  unfolding \<phi>R_def PP'_def using bprv_diag_eqv[of "neg P'"] by simp
+
+lemma bprv_imp_\<phi>R:
+  "bprv (imp (neg (PP' \<langle>\<phi>R\<rangle>)) \<phi>R)"
+  by (rule B.prv_imp_eqvER) (auto intro: bprv_\<phi>R_eqv)
+
+lemma prv_\<phi>R_eqv:
+  "prv (eqv \<phi>R (neg (PP' \<langle>\<phi>R\<rangle>)))"
+  using dwf_dwfd.d_dwf.bprv_prv'[OF _ bprv_\<phi>R_eqv, simplified] .
+
+lemma prv_imp_\<phi>R:
+  "prv (imp (neg (PP' \<langle>\<phi>R\<rangle>)) \<phi>R)"
+  by (rule prv_imp_eqvER) (auto intro: prv_\<phi>R_eqv)
+
+end \<comment> \<open>context @{locale Rosser_Form}\<close>
+
+
+sublocale Rosser_Form_Proofs < Rosser_Form where P = P
+  by standard
+
+sublocale Rosser_Form_Proofs < Goedel_Form where P = P
+  by standard
+
+(*<*)
+end
+(*>*)
diff --git a/thys/Goedel_Incompleteness/Standard_Model_More.thy b/thys/Goedel_Incompleteness/Standard_Model_More.thy
new file mode 100644
--- /dev/null
+++ b/thys/Goedel_Incompleteness/Standard_Model_More.thy
@@ -0,0 +1,469 @@
+chapter \<open>Standard Models with Two Provability Relations\<close>
+
+(*<*)
+(* Abstract notion of standard model and truth  *)
+theory Standard_Model_More
+imports Derivability_Conditions "Syntax_Independent_Logic.Standard_Model"
+begin
+(*>*)
+
+locale Minimal_Truth_Soundness_Proof_Repr =
+CleanRepr_Proofs
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  eql cnj imp all exi
+  prv bprv
+  enc
+  fls
+  dsj
+  "proof" prfOf
+  encPf
+  Pf
++ \<comment> \<open>The label "B" stands for "basic", as a reminder that soundness
+refers to the basic provability relation:\<close>
+B: Minimal_Truth_Soundness
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  dsj
+  num
+  bprv
+  isTrue
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and eql cnj imp all exi
+and fls
+and dsj
+and num
+and prv bprv
+and isTrue
+and enc ("\<langle>_\<rangle>")
+and "proof" :: "'proof set" and prfOf
+and encPf Pf
+begin
+
+lemmas prfOf_iff_PPf = B_consistent_prfOf_iff_PPf[OF B.consistent]
+
+text \<open>The provability predicate is decided by basic provability on encodings:\<close>
+lemma isTrue_prv_PPf_prf_or_neg:
+"prf \<in> proof \<Longrightarrow> \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow>
+    bprv (PPf (encPf prf) \<langle>\<phi>\<rangle>) \<or> bprv (neg (PPf (encPf prf) \<langle>\<phi>\<rangle>))"
+  using not_prfOf_PPf prfOf_PPf by blast
+
+text \<open>... hence that predicate is complete w.r.t. truth:\<close>
+lemma isTrue_PPf_Implies_bprv_PPf:
+"prf \<in> proof \<Longrightarrow> \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow>
+   isTrue (PPf (encPf prf) \<langle>\<phi>\<rangle>) \<Longrightarrow> bprv (PPf (encPf prf) \<langle>\<phi>\<rangle>)"
+  by (metis FvarsT_num Fvars_PPf Fvars_fls PPf
+Un_empty empty_iff enc encPf fls in_num isTrue_prv_PPf_prf_or_neg
+neg_def B.not_isTrue_fls B.prv_imp_implies_isTrue)
+
+text \<open>... and thanks cleanness we can replace encoded proofs
+with arbitrary numerals in the completeness property:\<close>
+lemma isTrue_implies_bprv_PPf:
+assumes [simp]: "n \<in> num" "\<phi> \<in> fmla" "Fvars \<phi> = {}"
+and iT: "isTrue (PPf n \<langle>\<phi>\<rangle>)"
+shows "bprv (PPf n \<langle>\<phi>\<rangle>)"
+proof(cases "n \<in> encPf ` proof")
+  case True
+  thus ?thesis
+    using iT isTrue_PPf_Implies_bprv_PPf by auto
+next
+  case False
+  hence "bprv (neg (PPf n \<langle>\<phi>\<rangle>))" by (simp add: Clean_PPf_encPf)
+  hence "isTrue (neg (PPf n \<langle>\<phi>\<rangle>))" by (intro B.sound_isTrue) auto
+  hence False using iT by (intro B.isTrue_neg_excl) auto
+  thus ?thesis by auto
+qed
+
+text \<open>... in fact, by @{locale Minimal_Truth_Soundness} we even have an iff:\<close>
+lemma isTrue_iff_bprv_PPf:
+"\<And> n \<phi>. n \<in> num \<Longrightarrow> \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> isTrue (PPf n \<langle>\<phi>\<rangle>) \<longleftrightarrow> bprv (PPf n \<langle>\<phi>\<rangle>)"
+using isTrue_implies_bprv_PPf
+using exists_no_Fvars B.not_isTrue_fls B.sound_isTrue by auto
+
+text \<open>Truth of the provability representation implies provability (TIP):\<close>
+lemma TIP:
+assumes \<phi>[simp]: "\<phi> \<in> fmla" "Fvars \<phi> = {}"
+and iPP: "isTrue (wrepr.PP \<langle>\<phi>\<rangle>)"
+shows "prv \<phi>"
+proof-
+  have "isTrue (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>))" using iPP unfolding PP_PPf[OF \<phi>(1)] .
+  from B.isTrue_exi[OF _ _ _ this]
+  obtain n where n[simp]: "n \<in> num" and "isTrue (PPf n \<langle>\<phi>\<rangle>)" by auto
+  hence pP: "bprv (PPf n \<langle>\<phi>\<rangle>)" using isTrue_implies_bprv_PPf by auto
+  hence "\<not> bprv (neg (PPf n \<langle>\<phi>\<rangle>))"
+  using B.prv_neg_excl[of "PPf n \<langle>\<phi>\<rangle>"] by auto
+  then obtain "prf" where "prf"[simp]: "prf \<in> proof" and nn: "n = encPf prf"
+  using assms n Clean_PPf_encPf \<phi>(1) by blast
+  have "prfOf prf \<phi>" using pP unfolding nn using prfOf_iff_PPf by auto
+  thus ?thesis using prv_prfOf by auto
+qed
+
+text \<open>The reverse HBL1 -- now without the $\omega$-consistency assumption which holds here
+thanks to our truth-in-standard-model assumption:\<close>
+
+lemmas HBL1_rev = \<omega>consistentStd1_HBL1_rev[OF B.\<omega>consistentStd1]
+text \<open>Note that the above would also follow by @{locale Minimal_Truth_Soundness} from TIP:\<close>
+lemma TIP_implies_HBL1_rev:
+assumes TIP: "\<forall>\<phi>. \<phi> \<in> fmla \<and> Fvars \<phi> = {} \<and> isTrue (wrepr.PP \<langle>\<phi>\<rangle>) \<longrightarrow> prv \<phi>"
+shows "\<forall>\<phi>. \<phi> \<in> fmla \<and> Fvars \<phi> = {} \<and> bprv (wrepr.PP \<langle>\<phi>\<rangle>) \<longrightarrow> prv \<phi>"
+using B.sound_isTrue[of "wrepr.PP \<langle>_\<rangle>"] TIP by auto
+
+end \<comment> \<open>context @{locale Minimal_Truth_Soundness_Proof_Repr}\<close>
+
+
+section \<open>Proof recovery from $\mathit{HBL1\_iff}$\<close>
+
+locale Minimal_Truth_Soundness_HBL1iff_Compl_Pf =
+HBL1
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  eql cnj imp all exi
+  prv bprv
+  enc
+  P
++
+B : Minimal_Truth_Soundness
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  dsj
+  num
+  bprv
+  isTrue
++
+Deduct_with_False_Disj
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  dsj
+  num
+  prv
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and eql cnj imp all exi
+and fls
+and dsj
+and num
+and enc ("\<langle>_\<rangle>")
+and prv bprv
+and P
+and isTrue
++
+fixes Pf :: 'fmla
+assumes
+\<comment> \<open>@{term Pf} is a formula with free variables @{term xx} @{term yy}:\<close>
+Pf[simp,intro!]: "Pf \<in> fmla"
+and
+Fvars_Pf[simp]: "Fvars Pf = {yy,xx}"
+and
+\<comment> \<open>@{term P} relates to @{term Pf} internally (inside basic provability)
+just like a @{term prv} and a @{term prfOf} would relate---via an existential:\<close>
+P_Pf:
+"\<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow>
+ let PPf = (\<lambda> t1 t2. psubst Pf [(t1,yy), (t2,xx)]) in
+ bprv (eqv (subst P \<langle>\<phi>\<rangle> xx) (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>)))"
+assumes
+\<comment> \<open>We assume both $\mathit{HBL1}$ and $\mathit{HBL1\_rev}$, i.e., an iff version:\<close>
+HBL1_iff: "\<And> \<phi>. \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> bprv (PP \<langle>\<phi>\<rangle>) \<longleftrightarrow> prv \<phi>"
+and
+Compl_Pf:
+"\<And> n \<phi>. n \<in> num \<Longrightarrow> \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow>
+ let PPf = (\<lambda> t1 t2. psubst Pf [(t1,yy), (t2,xx)]) in
+ isTrue (PPf n \<langle>\<phi>\<rangle>) \<longrightarrow> bprv (PPf n \<langle>\<phi>\<rangle>)"
+begin
+
+definition PPf where "PPf \<equiv> \<lambda> t1 t2. psubst Pf [(t1,yy), (t2,xx)]"
+
+lemma PP_deff: "PP t = subst P t xx" using PP_def by auto
+
+lemma PP_PPf_eqv:
+  "\<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> bprv (eqv (PP \<langle>\<phi>\<rangle>) (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>)))"
+  using PP_deff PPf_def P_Pf by auto
+
+(*  *)
+
+lemma PPf[simp,intro!]: "t1 \<in> trm \<Longrightarrow> t2 \<in> trm \<Longrightarrow> xx \<notin> FvarsT t1 \<Longrightarrow> PPf t1 t2 \<in> fmla"
+  unfolding PPf_def by auto
+
+lemma PPf_def2: "t1 \<in> trm \<Longrightarrow> t2 \<in> trm \<Longrightarrow> xx \<notin> FvarsT t1 \<Longrightarrow>
+  PPf t1 t2 = subst (subst Pf t1 yy) t2 xx"
+  unfolding PPf_def by (rule psubst_eq_rawpsubst2[simplified]) auto
+
+lemma Fvars_PPf[simp]:
+  "t1 \<in> trm \<Longrightarrow> t2 \<in> trm \<Longrightarrow> xx \<notin> FvarsT t1 \<Longrightarrow> Fvars (PPf t1 t2) = FvarsT t1 \<union> FvarsT t2"
+  by (auto simp add: PPf_def2 subst2_fresh_switch)
+
+lemma [simp]:
+"n \<in> num \<Longrightarrow> subst (PPf (Var yy) (Var xx)) n xx = PPf (Var yy) n"
+"m \<in> num \<Longrightarrow> n \<in> num \<Longrightarrow> subst (PPf (Var yy) m) n yy = PPf n m"
+"n \<in> num \<Longrightarrow> subst (PPf (Var yy) (Var xx)) n yy = PPf n (Var xx)"
+"m \<in> num \<Longrightarrow> n \<in> num \<Longrightarrow> subst (PPf m (Var xx)) n xx = PPf m n"
+"m \<in> num \<Longrightarrow> subst (PPf (Var zz) (Var xx')) m zz = PPf m (Var xx')"
+"m \<in> num \<Longrightarrow> n \<in> num \<Longrightarrow> subst (PPf m (Var xx')) n xx' = PPf m n"
+"n \<in> num \<Longrightarrow> subst (PPf (Var zz) (Var xx')) n xx' = PPf (Var zz) n"
+"m \<in> num \<Longrightarrow> n \<in> num \<Longrightarrow> subst (PPf (Var zz) n) m zz = PPf m n"
+  by (auto simp: PPf_def2 subst2_fresh_switch)
+
+(* *)
+
+lemma PP_PPf:
+assumes "\<phi> \<in> fmla" "Fvars \<phi> = {}" shows "bprv (PP \<langle>\<phi>\<rangle>) \<longleftrightarrow> bprv (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>))"
+  using assms PP_PPf_eqv[OF assms] B.prv_eqv_sym[OF _ _ PP_PPf_eqv[OF assms]]
+  by (auto intro!: B.prv_eqv_prv[of "PP \<langle>\<phi>\<rangle>" "exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>)"]
+    B.prv_eqv_prv[of "exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>)" "PP \<langle>\<phi>\<rangle>"])
+
+lemma isTrue_implies_bprv_PPf:
+"\<And> n \<phi>. n \<in> num \<Longrightarrow> \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow>
+ isTrue (PPf n \<langle>\<phi>\<rangle>) \<Longrightarrow> bprv (PPf n \<langle>\<phi>\<rangle>)"
+  using Compl_Pf by(simp add: PPf_def)
+
+lemma isTrue_iff_bprv_PPf:
+"\<And> n \<phi>. n \<in> num \<Longrightarrow> \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> isTrue (PPf n \<langle>\<phi>\<rangle>) \<longleftrightarrow> bprv (PPf n \<langle>\<phi>\<rangle>)"
+using isTrue_implies_bprv_PPf
+  using exists_no_Fvars B.not_isTrue_fls B.sound_isTrue by auto
+
+text \<open>Preparing to instantiate this "proof recovery" alternative into our
+mainstream locale hierarchy, which assumes proofs.
+We define the "missing" proofs to be numerals, we encode them as the identity,
+and we "copy" @{term prfOf} from the corresponding predicate one-level-up, @{term PPf}:\<close>
+
+definition "proof" :: "'trm set" where [simp]: "proof = num"
+definition prfOf :: "'trm \<Rightarrow> 'fmla \<Rightarrow> bool" where
+  "prfOf n \<phi> \<equiv> bprv (PPf n \<langle>\<phi>\<rangle>)"
+definition encPf :: "'trm \<Rightarrow> 'trm" where [simp]: "encPf \<equiv> id"
+(*  *)
+
+lemma prv_exi_PPf_iff_isTrue:
+assumes [simp]: "\<phi> \<in> fmla" "Fvars \<phi> = {}"
+shows "bprv (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>)) \<longleftrightarrow> isTrue (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>))" (is "?L \<longleftrightarrow> ?R")
+proof
+  assume ?L thus ?R by (intro B.sound_isTrue) auto
+next
+  assume ?R
+  obtain n where n[simp]: "n \<in> num" and i: "isTrue (PPf n \<langle>\<phi>\<rangle>)" using B.isTrue_exi[OF _ _ _ `?R`] by auto
+  hence "bprv (PPf n \<langle>\<phi>\<rangle>)" by (auto simp: isTrue_iff_bprv_PPf)
+  thus ?L by (intro B.prv_exiI[of _ _ n]) auto
+qed
+
+lemma isTrue_exi_iff:
+assumes [simp]: "\<phi> \<in> fmla" "Fvars \<phi> = {}"
+shows "isTrue (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>)) \<longleftrightarrow> (\<exists>n\<in>num. isTrue (PPf n \<langle>\<phi>\<rangle>))" (is "?L \<longleftrightarrow> ?R")
+proof
+  assume ?L thus ?R using B.isTrue_exi[OF _ _ _ `?L`] by auto
+next
+  assume ?R
+  then obtain n where n[simp]: "n \<in> num" and i: "isTrue (PPf n \<langle>\<phi>\<rangle>)" by auto
+  hence "bprv (PPf n \<langle>\<phi>\<rangle>)" by (auto simp: isTrue_iff_bprv_PPf)
+  hence "bprv (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>))" by (intro B.prv_exiI[of _ _ n]) auto
+  thus ?L by (intro B.sound_isTrue) auto
+qed
+
+lemma prv_prfOf:
+assumes "\<phi> \<in> fmla" "Fvars \<phi> = {}"
+shows "prv \<phi> \<longleftrightarrow> (\<exists>n\<in>num. prfOf n \<phi>)"
+proof-
+  have "prv \<phi> \<longleftrightarrow> bprv (PP \<langle>\<phi>\<rangle>)" using HBL1_iff[OF assms] by simp
+  also have "\<dots> \<longleftrightarrow> bprv (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>))" unfolding PP_PPf[OF assms] ..
+  also have "\<dots> \<longleftrightarrow> isTrue (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>))" using prv_exi_PPf_iff_isTrue[OF assms] .
+  also have "\<dots> \<longleftrightarrow> (\<exists>n\<in>num. isTrue (PPf n \<langle>\<phi>\<rangle>))" using isTrue_exi_iff[OF assms] .
+  also have "\<dots> \<longleftrightarrow> (\<exists>n\<in>num. bprv (PPf n \<langle>\<phi>\<rangle>))" using isTrue_iff_bprv_PPf[OF _ assms] by auto
+  also have "\<dots> \<longleftrightarrow> (\<exists>n\<in>num. prfOf n \<phi>)" unfolding prfOf_def ..
+  finally show ?thesis .
+qed
+
+lemma prfOf_prv_Pf:
+assumes "n \<in> num" and "\<phi> \<in> fmla" "Fvars \<phi> = {}" and "prfOf n \<phi>"
+shows "bprv (psubst Pf [(n, yy), (\<langle>\<phi>\<rangle>, xx)])"
+using assms unfolding prfOf_def by (auto simp: PPf_def2 psubst_eq_rawpsubst2)
+
+lemma isTrue_exi_iff_PP:
+assumes [simp]: "\<phi> \<in> fmla" "Fvars \<phi> = {}"
+shows "isTrue (PP \<langle>\<phi>\<rangle>) \<longleftrightarrow> (\<exists>n\<in>num. isTrue (PPf n \<langle>\<phi>\<rangle>))"
+proof-
+  have "bprv (eqv (PP \<langle>\<phi>\<rangle>) (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>)))"
+    using PP_PPf_eqv by auto
+  hence "bprv (imp (PP \<langle>\<phi>\<rangle>) (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>)))"
+  and "bprv (imp (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>)) (PP \<langle>\<phi>\<rangle>))"
+  by (simp_all add: B.prv_imp_eqvEL B.prv_imp_eqvER)
+  thus ?thesis unfolding isTrue_exi_iff[OF assms, symmetric]
+    by (intro iffI) (rule B.prv_imp_implies_isTrue; simp)+
+qed
+
+lemma bprv_compl_isTrue_PP_enc:
+assumes 1: "\<phi> \<in> fmla" "Fvars \<phi> = {}" and 2: "isTrue (PP \<langle>\<phi>\<rangle>)"
+shows "bprv (PP \<langle>\<phi>\<rangle>)"
+proof-
+  obtain n where nn: "n \<in> num" and i: "isTrue (PPf n \<langle>\<phi>\<rangle>)"
+   using 2 unfolding isTrue_exi_iff_PP[OF 1] ..
+  hence "bprv (PPf n \<langle>\<phi>\<rangle>)"
+    using i using nn assms isTrue_iff_bprv_PPf by blast
+  hence "bprv (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>))"
+  using 2 assms isTrue_exi_iff isTrue_exi_iff_PP prv_exi_PPf_iff_isTrue by auto
+  thus ?thesis using PP_PPf 1 by blast
+qed
+
+lemma TIP:
+assumes 1: "\<phi> \<in> fmla" "Fvars \<phi> = {}" and 2: "isTrue (PP \<langle>\<phi>\<rangle>)"
+shows "prv \<phi>"
+using bprv_compl_isTrue_PP_enc[OF assms] HBL1_iff assms by blast
+
+
+end \<comment> \<open>context @{locale Minimal_Truth_Soundness_HBL1iff_Compl_Pf}\<close>
+
+
+locale Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf =
+Minimal_Truth_Soundness_HBL1iff_Compl_Pf
++
+assumes
+Compl_NegPf:
+"\<And> n \<phi>. n \<in> num \<Longrightarrow> \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow>
+ let PPf = (\<lambda> t1 t2. psubst Pf [(t1,yy), (t2,xx)]) in
+ isTrue (B.neg (PPf n \<langle>\<phi>\<rangle>)) \<longrightarrow> bprv (B.neg (PPf n \<langle>\<phi>\<rangle>))"
+begin
+
+lemma isTrue_implies_prv_neg_PPf:
+"\<And> n \<phi>. n \<in> num \<Longrightarrow> \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow>
+ isTrue (B.neg (PPf n \<langle>\<phi>\<rangle>)) \<Longrightarrow> bprv (B.neg (PPf n \<langle>\<phi>\<rangle>))"
+  using Compl_NegPf by(simp add: PPf_def)
+
+lemma isTrue_iff_prv_neg_PPf:
+"\<And> n \<phi>. n \<in> num \<Longrightarrow> \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> isTrue (B.neg (PPf n \<langle>\<phi>\<rangle>)) \<longleftrightarrow> bprv (B.neg (PPf n \<langle>\<phi>\<rangle>))"
+using isTrue_implies_prv_neg_PPf
+  using exists_no_Fvars B.not_isTrue_fls B.sound_isTrue by auto
+
+lemma prv_PPf_decide:
+assumes [simp]: "n \<in> num" "\<phi> \<in> fmla" "Fvars \<phi> = {}"
+and np: "\<not> bprv (PPf n \<langle>\<phi>\<rangle>)"
+shows "bprv (B.neg (PPf n \<langle>\<phi>\<rangle>))"
+proof-
+  have "\<not> isTrue (PPf n \<langle>\<phi>\<rangle>)" using assms by (auto simp: isTrue_iff_bprv_PPf)
+  hence "isTrue (B.neg (PPf n \<langle>\<phi>\<rangle>))" using B.isTrue_neg[of "PPf n \<langle>\<phi>\<rangle>"] by auto
+  thus ?thesis by (auto simp: isTrue_iff_prv_neg_PPf)
+qed
+
+lemma not_prfOf_prv_neg_Pf:
+assumes n\<phi>: "n \<in> num" "\<phi> \<in> fmla" "Fvars \<phi> = {}" and "\<not> prfOf n \<phi>"
+shows "bprv (B.neg (psubst Pf [(n, yy), (\<langle>\<phi>\<rangle>, xx)]))"
+  using assms prv_PPf_decide[OF n\<phi>] by (auto simp: prfOf_def PPf_def2 psubst_eq_rawpsubst2)
+
+end \<comment> \<open>context @{locale Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf}\<close>
+
+sublocale Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf <
+   repr: CleanRepr_Proofs
+(* added label to avoid duplicated constant P, which is assumed
+in Minimal_Truth_Soundness_HBL1iff_Compl_Pf but defined in CleanRepr_Proofs
+(they are of course extensionally equal).
+*)
+  where "proof" = "proof" and prfOf = prfOf and encPf = encPf
+  by standard (auto simp: bprv_prv prv_prfOf prfOf_prv_Pf not_prfOf_prv_neg_Pf)
+
+(* Lemma 6 ("proof recovery") from the JAR paper: *)
+sublocale Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf <
+  min_truth: Minimal_Truth_Soundness_Proof_Repr
+where "proof" = "proof" and prfOf = prfOf and encPf = encPf
+  by standard
+
+
+
+(* FOR THE CLASSICAL REASONING VERSION *)
+
+locale Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf =
+HBL1
+  var trm fmla Var FvarsT substT Fvars subst
+  num
+  eql cnj imp all exi
+  prv bprv
+  enc
+  P
++
+B: Minimal_Truth_Soundness
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  dsj
+  num
+  bprv
+  isTrue
++
+Deduct_with_False_Disj
+  var trm fmla Var FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  dsj
+  num
+  prv
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var FvarsT substT Fvars subst
+and eql cnj imp all exi
+and fls
+and dsj
+and num
+and enc ("\<langle>_\<rangle>")
+and prv bprv
+and P
+and isTrue
++
+fixes Pf :: 'fmla
+assumes
+(* Pf is a formula with free variables xx yy  *)
+Pf[simp,intro!]: "Pf \<in> fmla"
+and
+Fvars_Pf[simp]: "Fvars Pf = {yy,xx}"
+and
+(* P relates to Pf internally just like a prv and a proofOf would
+relate: via an existential *)
+P_Pf:
+"\<phi> \<in> fmla \<Longrightarrow>
+ let PPf = (\<lambda> t1 t2. psubst Pf [(t1,yy), (t2,xx)]) in
+ bprv (eqv (subst P \<langle>\<phi>\<rangle> xx) (exi yy (PPf (Var yy) \<langle>\<phi>\<rangle>)))"
+assumes
+(* We assume, in addition to HBL1, the strong form of HBL1_rev: *)
+HBL1_rev_prv: "\<And> \<phi>. \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> prv (PP \<langle>\<phi>\<rangle>) \<Longrightarrow> prv \<phi>"
+and
+Compl_Pf:
+"\<And> n \<phi>. n \<in> num \<Longrightarrow> \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow>
+ let PPf = (\<lambda> t1 t2. psubst Pf [(t1,yy), (t2,xx)]) in
+ isTrue (PPf n \<langle>\<phi>\<rangle>) \<longrightarrow> bprv (PPf n \<langle>\<phi>\<rangle>)"
+begin
+
+lemma HBL1_rev:
+  assumes f: "\<phi> \<in> fmla" and fv: "Fvars \<phi> = {}" and bp: "bprv (PP \<langle>\<phi>\<rangle>)"
+  shows "prv \<phi>"
+  using assms by (auto intro!: HBL1_rev_prv bprv_prv[OF _ _ bp])
+
+lemma HBL1_iff: "\<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> bprv (PP \<langle>\<phi>\<rangle>) \<longleftrightarrow> prv \<phi>"
+  using HBL1 HBL1_rev unfolding PP_def by auto
+
+lemma HBL1_iff_prv: "\<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> prv (PP \<langle>\<phi>\<rangle>) \<longleftrightarrow> prv \<phi>"
+  by (intro iffI bprv_prv[OF _ _ HBL1_PP], elim HBL1_rev_prv[rotated -1]) auto
+
+end \<comment> \<open>context @{locale Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf}\<close>
+
+sublocale Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf <
+  mts_prv_mts: Minimal_Truth_Soundness_HBL1iff_Compl_Pf where Pf = Pf
+  using P_Pf HBL1_rev HBL1_PP Compl_Pf
+  by unfold_locales auto
+
+locale Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf_Classical =
+Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf
++
+assumes
+\<comment> \<open>NB: we don't really need to assume classical reasoning (double negation) all throughout,
+but only for the provability predicate:\<close>
+classical_P: "\<And> \<phi>. \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> let PP = (\<lambda>t. subst P t xx) in
+  prv (B.neg (B.neg (PP \<langle>\<phi>\<rangle>))) \<Longrightarrow> prv (PP \<langle>\<phi>\<rangle>)"
+begin
+
+lemma classical_PP: "\<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> prv (B.neg (B.neg (PP \<langle>\<phi>\<rangle>))) \<Longrightarrow> prv (PP \<langle>\<phi>\<rangle>)"
+  using classical_P unfolding PP_def by auto
+
+end \<comment> \<open>context @{locale Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf_Classical}\<close>
+
+(*<*)
+end
+(*>*)
diff --git a/thys/Goedel_Incompleteness/Tarski.thy b/thys/Goedel_Incompleteness/Tarski.thy
new file mode 100644
--- /dev/null
+++ b/thys/Goedel_Incompleteness/Tarski.thy
@@ -0,0 +1,97 @@
+chapter \<open>Abstract Formulation of Tarski's Theorems\<close>
+
+text \<open>We prove Tarski's proof-theoretic and semantic theorems about the
+non-definability and respectively non-expressiveness (in the standard model) of truth\<close>
+
+(*<*)
+theory Tarski
+  imports Goedel_Formula Standard_Model_More
+begin
+(*>*)
+
+section \<open>Non-Definability of Truth\<close>
+
+context Goedel_Form
+begin
+
+context
+  fixes T :: 'fmla
+  assumes T[simp,intro!]: "T \<in> fmla"
+  and Fvars_T[simp]: "Fvars T = {xx}"
+  and prv_T: "\<And>\<phi>. \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> prv (eqv (subst T \<langle>\<phi>\<rangle> xx) \<phi>)"
+begin
+
+definition \<phi>T :: 'fmla where "\<phi>T \<equiv> diag (neg T)"
+
+lemma \<phi>T[simp,intro!]: "\<phi>T \<in> fmla" and
+Fvars_\<phi>T[simp]: "Fvars \<phi>T = {}"
+  unfolding \<phi>T_def PP_def by auto
+
+lemma bprv_\<phi>T_eqv:
+"bprv (eqv \<phi>T (neg (subst T \<langle>\<phi>T\<rangle> xx)))"
+  unfolding \<phi>T_def using bprv_diag_eqv[of "neg T"] by simp
+
+lemma prv_\<phi>T_eqv:
+"prv (eqv \<phi>T (neg (subst T \<langle>\<phi>T\<rangle> xx)))"
+  using d_dwf.bprv_prv'[OF _ bprv_\<phi>T_eqv, simplified] .
+
+lemma \<phi>T_prv_fls: "prv fls"
+using prv_eqv_eqv_neg_prv_fls2[OF _ _ prv_T[OF \<phi>T Fvars_\<phi>T] prv_\<phi>T_eqv] by auto
+
+end \<comment> \<open>context\<close>
+
+theorem Tarski_proof_theoretic:
+assumes "T \<in> fmla" "Fvars T = {xx}"
+and "\<And>\<phi>. \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> prv (eqv (subst T \<langle>\<phi>\<rangle> xx) \<phi>)"
+shows "\<not> consistent"
+using \<phi>T_prv_fls[OF assms] consistent_def by auto
+
+end \<comment> \<open>context @{locale Goedel_Form}\<close>
+
+
+section \<open>Non-Expressiveness of Truth\<close>
+
+text \<open>This follows as a corollary of the syntactic version, after taking prv
+to be isTrue on sentences.Indeed, this is a virtue of our abstract treatment
+of provability: We don't work with a particular predicate, but with any predicate
+that is closed under some rules --- which could as well be a semantic notion of truth (for sentences).\<close>
+
+locale Goedel_Form_prv_eq_isTrue =
+Goedel_Form
+  var trm fmla Var num FvarsT substT Fvars subst
+  eql cnj imp all exi
+  fls
+  prv bprv
+  enc
+  P
+  S
+for
+var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
+and Var num FvarsT substT Fvars subst
+and eql cnj imp all exi
+and fls
+and prv bprv
+and enc ("\<langle>_\<rangle>")
+and S
+and P
++
+fixes isTrue :: "'fmla \<Rightarrow> bool"
+assumes prv_eq_isTrue: "\<And> \<phi>. \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> prv \<phi> = isTrue \<phi>"
+begin
+
+theorem Tarski_semantic:
+assumes 0: "T \<in> fmla" "Fvars T = {xx}"
+and 1: "\<And>\<phi>. \<phi> \<in> fmla \<Longrightarrow> Fvars \<phi> = {} \<Longrightarrow> isTrue (eqv (subst T \<langle>\<phi>\<rangle> xx) \<phi>)"
+shows "\<not> consistent"
+using assms prv_eq_isTrue[of "eqv (subst T \<langle>_\<rangle> xx) _"]
+  by (intro Tarski_proof_theoretic[OF 0]) auto
+
+text \<open>NB: To instantiate the semantic version of Tarski's theorem for a truth predicate
+isTruth on sentences, one needs to extend it to a predicate "prv" on formulas and verify
+that "prv" satisfies the rules of intuitionistic logic.\<close>
+
+end \<comment> \<open>context @{locale Goedel_Form_prv_eq_isTrue}\<close>
+
+(*<*)
+end
+(*>*)
diff --git a/thys/Goedel_Incompleteness/document/root.bib b/thys/Goedel_Incompleteness/document/root.bib
new file mode 100644
--- /dev/null
+++ b/thys/Goedel_Incompleteness/document/root.bib
@@ -0,0 +1,14 @@
+@inproceedings{DBLP:conf/cade/0001T19,
+  author    = {Andrei Popescu and
+               Dmitriy Traytel},
+  editor    = {Pascal Fontaine},
+  title     = {A Formally Verified Abstract Account of {G}{\"{o}}del's Incompleteness
+               Theorems},
+  booktitle = {{CADE} 27},
+  series    = {LNCS},
+  volume    = {11716},
+  pages     = {442--461},
+  publisher = {Springer},
+  year      = {2019},
+  doi       = {10.1007/978-3-030-29436-6\_26},
+}
\ No newline at end of file
diff --git a/thys/Goedel_Incompleteness/document/root.tex b/thys/Goedel_Incompleteness/document/root.tex
new file mode 100644
--- /dev/null
+++ b/thys/Goedel_Incompleteness/document/root.tex
@@ -0,0 +1,53 @@
+\documentclass[10pt,a4paper]{report}
+\usepackage{isabelle,isabellesym}
+
+\usepackage{a4wide}
+\usepackage[english]{babel}
+\usepackage{eufrak}
+\usepackage{amssymb}
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{literal}
+
+
+\begin{document}
+
+\title{An Abstract Formalization of G\"odel's Incompleteness Theorems}
+\author{Andrei Popescu \and Dmitriy Traytel}
+
+\maketitle
+
+\begin{abstract} We present an abstract formalization of G\"odel's incompleteness theorems.
+We analyze sufficient conditions for the theorems' applicability to a partially specified logic.
+Our abstract perspective enables a comparison between alternative approaches from the literature.
+These include Rosser's variation of the first theorem, Jeroslow's variation of the second theorem,
+and the Swierczkowski–Paulson semantics-based approach. This AFP entry is the main entry point to the results
+described in our CADE-27 paper~\cite{DBLP:conf/cade/0001T19}.
+
+\looseness=-1
+As part of our abstract formalization's validation, we instantiate our locales twice in the separate
+AFP entries \href{https://www.isa-afp.org/entries/Goedel_HFSet_Semantic.html}{Goedel\_HFSet\_Semantic} and
+\href{https://www.isa-afp.org/entries/Goedel_HFSet_Semanticless.html}{Goedel\_HFSet\_Semanticless}.
+\end{abstract}
+
+\tableofcontents
+
+% sane default for proof documents
+\parindent 0pt\parskip 0.5ex
+
+% generated text of all theories
+\input{session}
+
+\bibliographystyle{abbrv}
+\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
diff --git a/thys/ROOTS b/thys/ROOTS
--- a/thys/ROOTS
+++ b/thys/ROOTS
@@ -1,557 +1,558 @@
 ADS_Functor
 AODV
 AVL-Trees
 AWN
 Abortable_Linearizable_Modules
 Abs_Int_ITP2012
 Abstract-Hoare-Logics
 Abstract-Rewriting
 Abstract_Completeness
 Abstract_Soundness
 Adaptive_State_Counting
 Affine_Arithmetic
 Aggregation_Algebras
 Akra_Bazzi
 Algebraic_Numbers
 Algebraic_VCs
 Allen_Calculus
 Amicable_Numbers
 Amortized_Complexity
 AnselmGod
 Applicative_Lifting
 Approximation_Algorithms
 Architectural_Design_Patterns
 Aristotles_Assertoric_Syllogistic
 Arith_Prog_Rel_Primes
 ArrowImpossibilityGS
 Attack_Trees
 Auto2_HOL
 Auto2_Imperative_HOL
 AutoFocus-Stream
 Automated_Stateful_Protocol_Verification
 Automatic_Refinement
 AxiomaticCategoryTheory
 BDD
 BNF_CC
 BNF_Operations
 Banach_Steinhaus
 Bell_Numbers_Spivey
 Berlekamp_Zassenhaus
 Bernoulli
 Bertrands_Postulate
 Bicategory
 BinarySearchTree
 Binding_Syntax_Theory
 Binomial-Heaps
 Binomial-Queues
 BirdKMP
 Bondy
 Boolean_Expression_Checkers
 Bounded_Deducibility_Security
 Buchi_Complementation
 Budan_Fourier
 Buffons_Needle
 Buildings
 BytecodeLogicJmlTypes
 C2KA_DistributedSystems
 CAVA_Automata
 CAVA_LTL_Modelchecker
 CCS
 CISC-Kernel
 CRDT
 CYK
 CakeML
 CakeML_Codegen
 Call_Arity
 Card_Equiv_Relations
 Card_Multisets
 Card_Number_Partitions
 Card_Partitions
 Cartan_FP
 Case_Labeling
 Catalan_Numbers
 Category
 Category2
 Category3
 Cauchy
 Cayley_Hamilton
 Certification_Monads
 Chandy_Lamport
 Chord_Segments
 Circus
 Clean
 ClockSynchInst
 Closest_Pair_Points
 CofGroups
 Coinductive
 Coinductive_Languages
 Collections
 Comparison_Sort_Lower_Bound
 Compiling-Exceptions-Correctly
 Complete_Non_Orders
 Completeness
 Complex_Geometry
 Complx
 ComponentDependencies
 ConcurrentGC
 ConcurrentIMP
 Concurrent_Ref_Alg
 Concurrent_Revisions
 Consensus_Refined
 Constructive_Cryptography
 Constructor_Funs
 Containers
 CoreC++
 Core_DOM
 Count_Complex_Roots
 CryptHOL
 CryptoBasedCompositionalProperties
 DFS_Framework
 DPT-SAT-Solver
 DataRefinementIBP
 Datatype_Order_Generator
 Decl_Sem_Fun_PL
 Decreasing-Diagrams
 Decreasing-Diagrams-II
 Deep_Learning
 Density_Compiler
 Dependent_SIFUM_Refinement
 Dependent_SIFUM_Type_Systems
 Depth-First-Search
 Derangements
 Deriving
 Descartes_Sign_Rule
 Dict_Construction
 Differential_Dynamic_Logic
 Differential_Game_Logic
 Dijkstra_Shortest_Path
 Diophantine_Eqns_Lin_Hom
 Dirichlet_L
 Dirichlet_Series
 DiscretePricing
 Discrete_Summation
 DiskPaxos
 DynamicArchitectures
 Dynamic_Tables
 EFSM_Inference
 E_Transcendental
 Echelon_Form
 EdmondsKarp_Maxflow
 Efficient-Mergesort
 Elliptic_Curves_Group_Law
 Encodability_Process_Calculi
 Epistemic_Logic
 Ergodic_Theory
 Error_Function
 Euler_MacLaurin
 Euler_Partition
 Example-Submission
 Extended_Finite_State_Machines
 FFT
 FLP
 FOL-Fitting
 FOL_Harrison
 FOL_Seq_Calc1
 Factored_Transition_System_Bounding
 Falling_Factorial_Sum
 Farkas
 FeatherweightJava
 Featherweight_OCL
 Fermat3_4
 FileRefinement
 FinFun
 Finger-Trees
 Finite_Automata_HF
 First_Order_Terms
 First_Welfare_Theorem
 Fishburn_Impossibility
 Fisher_Yates
 Flow_Networks
 Floyd_Warshall
 Flyspeck-Tame
 FocusStreamsCaseStudies
 Forcing
 Formal_SSA
 Formula_Derivatives
 Fourier
 Free-Boolean-Algebra
 Free-Groups
 FunWithFunctions
 FunWithTilings
 Functional-Automata
 Functional_Ordered_Resolution_Prover
 Furstenberg_Topology
 GPU_Kernel_PL
 Gabow_SCC
 Game_Based_Crypto
 Gauss-Jordan-Elim-Fun
 Gauss_Jordan
 Gauss_Sums
 Gaussian_Integers
 GenClock
 General-Triangle
 Generalized_Counting_Sort
 Generic_Deriving
 Generic_Join
 GewirthPGCProof
 Girth_Chromatic
 GoedelGod
+Goedel_Incompleteness
 Goodstein_Lambda
 GraphMarkingIBP
 Graph_Saturation
 Graph_Theory
 Green
 Groebner_Bases
 Groebner_Macaulay
 Gromov_Hyperbolicity
 Group-Ring-Module
 HOL-CSP
 HOLCF-Prelude
 HRB-Slicing
 Heard_Of
 Hello_World
 HereditarilyFinite
 Hermite
 Hidden_Markov_Models
 Higher_Order_Terms
 Hoare_Time
 HotelKeyCards
 Huffman
 Hybrid_Logic
 Hybrid_Multi_Lane_Spatial_Logic
 Hybrid_Systems_VCs
 HyperCTL
 IEEE_Floating_Point
 IMAP-CRDT
 IMO2019
 IMP2
 IMP2_Binary_Heap
 IP_Addresses
 Imperative_Insertion_Sort
 Impossible_Geometry
 Incompleteness
 Incredible_Proof_Machine
 Inductive_Confidentiality
 Inductive_Inference
 InfPathElimination
 InformationFlowSlicing
 InformationFlowSlicing_Inter
 Integration
 Interval_Arithmetic_Word32
 Iptables_Semantics
 Irrational_Series_Erdos_Straus
 Irrationality_J_Hancl
 Isabelle_C
 Isabelle_Meta_Model
 Jacobson_Basic_Algebra
 Jinja
 JinjaThreads
 JiveDataStoreModel
 Jordan_Hoelder
 Jordan_Normal_Form
 KAD
 KAT_and_DRA
 KBPs
 KD_Tree
 Key_Agreement_Strong_Adversaries
 Kleene_Algebra
 Knot_Theory
 Knuth_Bendix_Order
 Knuth_Morris_Pratt
 Koenigsberg_Friendship
 Kruskal
 Kuratowski_Closure_Complement
 LLL_Basis_Reduction
 LLL_Factorization
 LOFT
 LTL
 LTL_Master_Theorem
 LTL_Normal_Form
 LTL_to_DRA
 LTL_to_GBA
 Lam-ml-Normalization
 LambdaAuth
 LambdaMu
 Lambda_Free_EPO
 Lambda_Free_KBOs
 Lambda_Free_RPOs
 Lambert_W
 Landau_Symbols
 Laplace_Transform
 Latin_Square
 LatticeProperties
 Launchbury
 Lazy-Lists-II
 Lazy_Case
 Lehmer
 Lifting_Definition_Option
 LightweightJava
 LinearQuantifierElim
 Linear_Inequalities
 Linear_Programming
 Linear_Recurrences
 Liouville_Numbers
 List-Index
 List-Infinite
 List_Interleaving
 List_Inversions
 List_Update
 LocalLexing
 Localization_Ring
 Locally-Nameless-Sigma
 Lowe_Ontological_Argument
 Lower_Semicontinuous
 Lp
 Lucas_Theorem
 MFMC_Countable
 MFODL_Monitor_Optimized
 MFOTL_Monitor
 MSO_Regex_Equivalence
 Markov_Models
 Marriage
 Mason_Stothers
 Matrices_for_ODEs
 Matrix
 Matrix_Tensor
 Matroids
 Max-Card-Matching
 Median_Of_Medians_Selection
 Menger
 Mersenne_Primes
 MiniML
 Minimal_SSA
 Minkowskis_Theorem
 Minsky_Machines
 Modal_Logics_for_NTS
 Modular_Assembly_Kit_Security
 Monad_Memo_DP
 Monad_Normalisation
 MonoBoolTranAlgebra
 MonoidalCategory
 Monomorphic_Monad
 MuchAdoAboutTwo
 Multi_Party_Computation
 Multirelations
 Myhill-Nerode
 Name_Carrying_Type_Inference
 Nash_Williams
 Nat-Interval-Logic
 Native_Word
 Nested_Multisets_Ordinals
 Network_Security_Policy_Verification
 Neumann_Morgenstern_Utility
 No_FTL_observers
 Nominal2
 Noninterference_CSP
 Noninterference_Concurrent_Composition
 Noninterference_Generic_Unwinding
 Noninterference_Inductive_Unwinding
 Noninterference_Ipurge_Unwinding
 Noninterference_Sequential_Composition
 NormByEval
 Nullstellensatz
 Octonions
 OpSets
 Open_Induction
 Optics
 Optimal_BST
 Orbit_Stabiliser
 Order_Lattice_Props
 Ordered_Resolution_Prover
 Ordinal
 Ordinal_Partitions
 Ordinals_and_Cardinals
 Ordinary_Differential_Equations
 PAC_Checker
 PCF
 PLM
 POPLmark-deBruijn
 PSemigroupsConvolution
 Pairing_Heap
 Paraconsistency
 Parity_Game
 Partial_Function_MR
 Partial_Order_Reduction
 Password_Authentication_Protocol
 Pell
 Perfect-Number-Thm
 Perron_Frobenius
 Pi_Calculus
 Pi_Transcendental
 Planarity_Certificates
 Poincare_Bendixson
 Poincare_Disc
 Polynomial_Factorization
 Polynomial_Interpolation
 Polynomials
 Pop_Refinement
 Posix-Lexing
 Possibilistic_Noninterference
 Power_Sum_Polynomials
 Pratt_Certificate
 Presburger-Automata
 Prim_Dijkstra_Simple
 Prime_Distribution_Elementary
 Prime_Harmonic_Series
 Prime_Number_Theorem
 Priority_Queue_Braun
 Priority_Search_Trees
 Probabilistic_Noninterference
 Probabilistic_Prime_Tests
 Probabilistic_System_Zoo
 Probabilistic_Timed_Automata
 Probabilistic_While
 Program-Conflict-Analysis
 Projective_Geometry
 Promela
 Proof_Strategy_Language
 PropResPI
 Propositional_Proof_Systems
 Prpu_Maxflow
 PseudoHoops
 Psi_Calculi
 Ptolemys_Theorem
 QHLProver
 QR_Decomposition
 Quantales
 Quaternions
 Quick_Sort_Cost
 RIPEMD-160-SPARK
 ROBDD
 RSAPSS
 Ramsey-Infinite
 Random_BSTs
 Random_Graph_Subgraph_Threshold
 Randomised_BSTs
 Randomised_Social_Choice
 Rank_Nullity_Theorem
 Real_Impl
 Recursion-Addition
 Recursion-Theory-I
 Refine_Imperative_HOL
 Refine_Monadic
 RefinementReactive
 Regex_Equivalence
 Regular-Sets
 Regular_Algebras
 Relation_Algebra
 Relational-Incorrectness-Logic
 Relational_Disjoint_Set_Forests
 Relational_Paths
 Rep_Fin_Groups
 Residuated_Lattices
 Resolution_FOL
 Rewriting_Z
 Ribbon_Proofs
 Robbins-Conjecture
 Root_Balanced_Tree
 Routing
 Roy_Floyd_Warshall
 SATSolverVerification
 SDS_Impossibility
 SIFPL
 SIFUM_Type_Systems
 SPARCv8
 Safe_Distance
 Safe_OCL
 Saturation_Framework
 Secondary_Sylow
 Security_Protocol_Refinement
 Selection_Heap_Sort
 SenSocialChoice
 Separata
 Separation_Algebra
 Separation_Logic_Imperative_HOL
 SequentInvertibility
 Shivers-CFA
 ShortestPath
 Show
 Sigma_Commit_Crypto
 Signature_Groebner
 Simpl
 Simple_Firewall
 Simplex
 Skew_Heap
 Skip_Lists
 Slicing
 Sliding_Window_Algorithm
 Smith_Normal_Form
 Smooth_Manifolds
 Sort_Encodings
 Source_Coding_Theorem
 Special_Function_Bounds
 Splay_Tree
 Sqrt_Babylonian
 Stable_Matching
 Statecharts
 Stateful_Protocol_Composition_and_Typing
 Stellar_Quorums
 Stern_Brocot
 Stewart_Apollonius
 Stirling_Formula
 Stochastic_Matrices
 Stone_Algebras
 Stone_Kleene_Relation_Algebras
 Stone_Relation_Algebras
 Store_Buffer_Reduction
 Stream-Fusion
 Stream_Fusion_Code
 Strong_Security
 Sturm_Sequences
 Sturm_Tarski
 Stuttering_Equivalence
 Subresultants
 Subset_Boolean_Algebras
 SumSquares
 SuperCalc
 Surprise_Paradox
 Symmetric_Polynomials
 Syntax_Independent_Logic
 Szpilrajn
 TESL_Language
 TLA
 Tail_Recursive_Functions
 Tarskis_Geometry
 Taylor_Models
 Timed_Automata
 Topology
 TortoiseHare
 Transcendence_Series_Hancl_Rucki
 Transformer_Semantics
 Transition_Systems_and_Automata
 Transitive-Closure
 Transitive-Closure-II
 Treaps
 Tree-Automata
 Tree_Decomposition
 Triangle
 Trie
 Twelvefold_Way
 Tycon
 Types_Tableaus_and_Goedels_God
 UPF
 UPF_Firewall
 UTP
 Universal_Turing_Machine
 UpDown_Scheme
 Valuation
 VectorSpace
 VeriComp
 Verified-Prover
 VerifyThis2018
 VerifyThis2019
 Vickrey_Clarke_Groves
 VolpanoSmith
 WHATandWHERE_Security
 WOOT_Strong_Eventual_Consistency
 WebAssembly
 Weight_Balanced_Trees
 Well_Quasi_Orders
 Winding_Number_Eval
 Word_Lib
 WorkerWrapper
 XML
 ZFC_in_HOL
 Zeta_3_Irrational
 Zeta_Function
 pGCL