Theory Goedel_II

chapter‹Gödel's Second Incompleteness Theorem›

theory Goedel_II
imports Goedel_I Quote 
begin

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 x⟧e"
  apply (clarsimp simp: SeqHR_def HR_def)
  apply (erule BuildSeq2_induct, auto simp add: q_defs WR_iff_eq_W [where e=e])
  done

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) 
  qed
  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)
qed

end