Theory Goedel_II

chapter‹Gödel's Second Incompleteness Theorem›

theory Goedel_II
imports Goedel_I Quote 

text‹The connection between @{term Quote} and @{term HR} (for interest only).›

lemma Quote_q_Eats [intro]:
  "Quote y y'  Quote z z'  Quote (y  z) (q_Eats y' z')"
  by (auto simp: Quote_def SeqQuote_def intro: BuildSeq2_combine)

lemma Quote_q_Succ [intro]:  "Quote y y'  Quote (succ y) (q_Succ y')"
  by (auto simp: succ_def q_Succ_def)

lemma HR_imp_eq_H: "HR x z  z = HF xe"
  apply (clarsimp simp: SeqHR_def HR_def)
  apply (erule BuildSeq2_induct, auto simp add: q_defs WR_iff_eq_W [where e=e])

lemma HR_Ord_D: "HR x y  Ord x  WR x y"
  by (metis HF_Ord HR_imp_eq_H WR_iff_eq_W)

lemma WR_Quote: "WR (ord_of i) y  Quote (ord_of i) y"
  by (induct i arbitrary: y) (auto simp: Quote_0 WR0_iff WR_succ_iff q_Succ_def [symmetric])

lemma [simp]: "0,0,0, x, y = q_Eats x y"
  by (simp add: q_Eats_def)

lemma HR_imp_Quote: "coding_hf x  HR x y  Quote x y"
  apply (induct x arbitrary: y rule: coding_hf.induct, auto simp: WR_Quote HR_Ord_D)
  apply (auto dest!: HR_imp_eq_H [where e= e0])
  by (metis hpair_def' Quote_0 HR_H Quote_q_Eats)

interpretation qp0: quote_perm 0 "{}" "make_F {} 0"
  proof unfold_locales qed auto

lemma MonPon_PfP_implies_PfP:
  "{}  α IMP β; ground_fm α; ground_fm β  {PfP «α»}  PfP «β»"
  using qp0.quote_all_MonPon_PfP_ssubst
  by auto (metis Assume PfP_implies_ModPon_PfP_quot proved_iff_proved_PfP thin0)

lemma PfP_quot_contra: "ground_fm α  {}  PfP «α» IMP PfP «Neg α» IMP PfP «Fls»"
  using qp0.quote_all_Contra_PfP_ssubst 
  by (auto simp: qp0.quote_all_Contra_PfP_ssubst ground_fm_aux_def)

text‹Gödel's second incompleteness theorem: Our theory cannot prove its own consistency.›
theorem Goedel_II: "¬ {}  Neg (PfP «Fls»)"
proof -
  obtain δ where diag: "{}  δ IFF Neg (PfP «δ»)"  "¬ {}  δ" and gnd:  "ground_fm δ"
    by (metis Goedel_I)
  have "{PfP «δ»}  PfP «PfP «δ»»"
    by (auto simp: Provability ground_fm_aux_def supp_conv_fresh)
  moreover have "{PfP «δ»}  PfP «Neg (PfP «δ»)»"
  proof (rule MonPon_PfP_implies_PfP [OF _ gnd])
    show "{}  δ IMP Neg (PfP «δ»)"
      by (metis Conj_E2 Iff_def Iff_sym diag(1))
    show "ground_fm (Neg (PfP «δ»))"
      by (auto simp: ground_fm_aux_def supp_conv_fresh) 
  moreover have "ground_fm (PfP «δ»)"
    by (auto simp: ground_fm_aux_def supp_conv_fresh)
  ultimately have "{PfP «δ»}  PfP «Fls»" using PfP_quot_contra  
    by (metis (no_types) anti_deduction cut2)
  thus "¬ {}  Neg (PfP «Fls»)"
    by (metis Iff_MP2_same Neg_mono cut1 diag)