Theory Abstract_First_Goedel_Rosser

chapter ‹Abstract Formulations of Gödel-Rosser's First Incompleteness Theorem›

(*<*)
theory Abstract_First_Goedel_Rosser
  imports Rosser_Formula Standard_Model_More
begin
(*>*)

text ‹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.›

section ‹Proof-Theoretic Versions›

context Rosser_Form_Proofs
begin

lemma NN_neg_unique_xx':
  assumes [simp]:"φ ∈ fmla" "Fvars φ = {}"
  shows
    "bprv (imp (NN ⟨φ⟩ (Var xx'))
          (eql ⟨neg φ⟩ (Var xx')))"
  using B.prv_subst[of yy _ "Var xx'", OF _ _ _ NN_neg_unique[OF assms]] by fastforce

lemma NN_imp_xx':
  assumes [simp]: "φ ∈ fmla" "Fvars φ = {}" "χ ∈ fmla"
  shows "bprv (imp (subst χ ⟨neg φ⟩ xx')
                   (all xx' (imp (NN ⟨φ⟩ (Var xx')) χ)))"
proof-
  have 2: "bprv (imp (eql ⟨neg φ⟩ (Var xx')) (imp (subst χ ⟨neg φ⟩ xx') χ))"
    using B.prv_eql_subst_trm[of xx' χ "⟨neg φ⟩" "Var xx'", simplified] .
  have 1: "bprv (imp (subst χ ⟨neg φ⟩ xx') (imp (eql ⟨neg φ⟩ (Var xx')) χ))"
    by (simp add: "2" B.prv_imp_com)
  have 0: "bprv (imp (subst χ ⟨neg φ⟩ xx') (imp (NN ⟨φ⟩ (Var xx')) χ))"
    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 "¬ prv φR"
proof
  assume 0: "prv φR"
  then obtain "prf" where [simp]: "prf ∈ proof" and "prfOf prf φR" using prv_prfOf by auto
  hence 00: "bprv (PPf (encPf prf) ⟨φR⟩)" using prfOf_PPf by auto
  from dwf_dwfd.d_dwf.bprv_prv'[OF _ 00, simplified] have b00: "prv (PPf (encPf prf) ⟨φR⟩)" .
  have "¬ prv (neg φR)" using 0 c unfolding consistent_def3 by auto
  hence "∀ prf ∈ proof.  ¬ prfOf prf (neg φR)" using 00 prv_prfOf by auto
  hence "bprv (neg (PPf p ⟨neg φR⟩))" if "p ∈ num" for p using not_prfOf_PPf Clean_PPf_encPf that
    by (cases "p ∈ encPf ` proof") auto
  hence 1: "prv (all zz (imp (LLq (Var zz) (encPf prf)) (neg (PPf (Var zz) ⟨neg φR⟩))))"
    (* here use locale assumption about the order-like relation: *)
    by (intro LLq_num) auto
  have 11: "prv (RR (encPf prf) ⟨φR⟩)"
    using NN_imp_xx'[of φ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) ⟨φR⟩) (RR (encPf prf) ⟨φR⟩))"
    by (rule prv_cnjI[OF _ _ b00 11]) auto
  have "prv ((PP' ⟨φR⟩))" unfolding PP'_def P'_def
     using 3 by (auto intro: prv_exiI[of _ _ "encPf prf"])
  moreover have "prv (neg (PP' ⟨φR⟩))"
    using prv_eqv_prv[OF _ _ 0 prv_φR_eqv] by auto
  ultimately show False using c unfolding consistent_def3 by auto
qed

lemma goedel_rosser_first_theHardHalf:
  assumes c: "consistent"
  shows "¬ prv (neg φR)"
proof
  assume 0: "prv (neg φR)"
  then obtain "prf" where [simp,intro!]: "prf ∈ proof" and pr: "prfOf prf (neg φR)" using prv_prfOf by auto
  define p where p: "p = encPf prf"
  have [simp,intro!]: "p ∈ num" unfolding p by auto
  have 11: "bprv (PPf p ⟨neg φR⟩)" using pr prfOf_PPf unfolding p by auto
  have 1: "bprv (NN ⟨φR⟩ ⟨neg φR⟩)" using NN_neg by simp

  have "¬ prv φR" using 0 c unfolding consistent_def3 by auto
  from not_prv_prv_neg_PPf[OF _ _ this]
  have b2: "∀ r ∈ num. bprv (neg (PPf r ⟨φR⟩))" by auto
  hence 2: "∀ r ∈ num. prv (neg (PPf r ⟨φR⟩))"
    by (auto intro: dwf_dwfd.d_dwf.bprv_prv')

  obtain P where P[simp,intro!]: "P ⊆num" "finite P"
    and 3: "prv (dsj (sdsj {eql (Var yy) r |r. r ∈ 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) ⟨φR⟩) (RR (Var yy) ⟨φR⟩)) fls)"
  proof(rule prv_dsj_cases[OF _ _ _ 3])
    {fix r assume r: "r ∈ P" hence rn[simp]: "r ∈ num" using P(1) by blast
      have "prv (imp (cnj (PPf r ⟨φR⟩) (RR r ⟨φR⟩)) fls)"
        using 2 unfolding neg_def
        by (metis FvarsT_num PPf RR rn φ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) ⟨φR⟩) (RR (Var yy) ⟨φR⟩)) fls))"
        using prv_eql_subst_trm_id[of yy "cnj (PPf (Var yy) ⟨φR⟩) (RR (Var yy) ⟨φR⟩)" r,simplified]
        unfolding neg_def[symmetric]
        by (intro prv_neg_imp_imp_trans) auto
    }
    thus "prv (imp (sdsj {eql (Var yy) r |r. r ∈ P})
              (imp (cnj (PPf (Var yy) ⟨φR⟩) (RR (Var yy) ⟨φR⟩)) fls))"
       using Var P(1) eql by (intro prv_sdsj_imp) (auto 0 0 simp: set_rev_mp)
  next
    let ?φ = "all xx' (imp (NN ⟨φR⟩ (Var xx')) (neg (PPf p (Var xx'))))"
    have "bprv (neg ?φ)"
      using 1 11 by (intro B.prv_imp_neg_allWI[where t = "⟨neg φR⟩"]) (auto intro: B.prv_prv_neg_imp_neg)
    hence "prv (neg ?φ)" by (auto intro: dwf_dwfd.d_dwf.bprv_prv')
    hence 00: "prv (imp (LLq p (Var yy))
                       (imp (imp (LLq p (Var yy)) ?φ) 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) ⟨φR⟩) 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) ⟨φR⟩) (RR (Var yy) ⟨φR⟩)) 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) ⟨φR⟩) (RR (Var yy) ⟨φR⟩))))"
    unfolding neg_def[symmetric] by (intro prv_neg_neg_exi) auto
  hence "prv (neg (PP' ⟨φR⟩))" unfolding PP'_def P'_def by simp
  hence "prv φR" using prv_φR_eqv by (meson PP' φR enc in_num neg prv_eqv_prv_rev)
  with ‹¬ prv φR› show False using c unfolding consistent_def3 by auto
qed

theorem goedel_rosser_first:
  assumes "consistent"
  shows "¬ prv φR ∧ ¬ prv (neg φR)"
  using assms goedel_rosser_first_theEasyHalf goedel_rosser_first_theHardHalf by blast

theorem goedel_rosser_first_ex:
  assumes "consistent"
  shows "∃ φ. φ ∈ fmla ∧ ¬ prv φ ∧ ¬ prv (neg φ)"
  using assms goedel_rosser_first by (intro exI[of _ φR]) blast

end ― ‹context @{locale Rosser_Form}›


section ‹Model-Theoretic Versions›

subsection ‹First model-theoretic version›

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 (‹⟨_⟩›)
and N S P
and "proof" :: "'proof set" and prfOf encPf
and Pf
and isTrue
begin

lemma Fvars_PP'[simp]: "Fvars (PP' ⟨φR⟩) = {}" unfolding PP'_def
  by (subst Fvars_subst) auto

lemma Fvars_RR'[simp]: "Fvars (RR (Var yy) ⟨φR⟩) = {yy}"
  unfolding RR_def
  by (subst Fvars_psubst) (fastforce intro!: exI[of _ "{yy}"])+

lemma isTrue_PPf_implies_φR:
assumes "isTrue (all yy (neg (PPf (Var yy) ⟨φR⟩)))"
(is "isTrue ?H")
shows "isTrue φR"
proof-
  define F where "F ≡ RR (Var yy) ⟨φR⟩"
  have [simp]: "F ∈ fmla" "Fvars F = {yy}"
    unfolding F_def by auto
  have [simp]: "exi yy (PPf (Var yy) ⟨φR⟩) ∈ fmla"
    unfolding PPf_def by auto

  have 1: "bprv
     (imp (all yy (neg (PPf (Var yy) ⟨φR⟩)))
       (neg (exi yy (PPf (Var yy) ⟨φR⟩))))"
  (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' ⟨φR⟩)))"
    unfolding PP'_def P'_def
    by (simp add: F_def)
  from B.prv_prv_imp_trans[OF _ _ _  this bprv_imp_φR]
  have "bprv (imp ?H φR)" by auto
  from prv_imp_implies_isTrue[OF _ _ _ _ this assms, simplified]
  show ?thesis .
qed

theorem isTrue_φR:
  assumes "consistent"
  shows "isTrue φR"
proof-
  have "∀ n ∈ num. bprv (neg (PPf n ⟨φR⟩))"
    using not_prv_prv_neg_PPf[OF _ _ goedel_rosser_first_theEasyHalf[OF assms]]
    by auto
  hence "∀ n ∈ num. isTrue (neg (PPf n ⟨φR⟩))" by (auto intro: sound_isTrue)
  hence "isTrue (all yy (neg (PPf (Var yy) ⟨φR⟩)))" by (auto intro: isTrue_all)
  thus ?thesis using isTrue_PPf_implies_φR by auto
qed


theorem goedel_rosser_first_strong: "consistent ⟹ ¬ prv φR ∧ ¬ prv (neg φR) ∧ isTrue φR"
  using isTrue_φR goedel_rosser_first by blast

theorem goedel_rosser_first_strong_ex:
"consistent ⟹ ∃ φ. φ ∈ fmla ∧ ¬ prv φ ∧ ¬ prv (neg φ) ∧ isTrue φ"
  using goedel_rosser_first_strong by (intro exI[of _ φR]) blast

end ― ‹context @{locale Rosser_Form_Proofs_Minimal_Truth}›


subsection ‹Second model-theoretic version›

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 (‹⟨_⟩›)
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 (‹⟨_⟩›)
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
(*>*)