# 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"

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

```