chapter ‹The Hilbert-Bernays-Löb (HBL) Derivability Conditions› (*<*) theory Derivability_Conditions imports Abstract_Representability begin (*>*) section ‹First Derivability Condition› (* 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 ("⟨_⟩") + (* Very-weak represenatbility of provability, as a one-variable formula P, usually called the provability predicate: *) fixes P :: 'fmla assumes P[intro!,simp]: "P ∈ fmla" and Fvars_P[simp]: "Fvars P = {xx}" and HBL1: "⋀φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹ prv φ ⟹ bprv (subst P ⟨φ⟩ 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 ≡ λt. subst P t xx" lemma PP[simp]: "⋀t. t ∈ trm ⟹ PP t ∈ fmla" unfolding PP_def by auto lemma Fvars_PP[simp]: "⋀t. t ∈ trm ⟹ Fvars (PP t) = FvarsT t" unfolding PP_def by auto lemma [simp]: "n ∈ num ⟹ subst (PP (Var yy)) n yy = PP n" "n ∈ num ⟹ subst (PP (Var xx)) n xx = PP n" unfolding PP_def by auto lemma HBL1_PP: "φ ∈ fmla ⟹ Fvars φ = {} ⟹ prv φ ⟹ bprv (PP ⟨φ⟩)" using HBL1 unfolding PP_def by auto end ― ‹context @{locale HBL1}› section ‹Connections between Proof Representability, First Derivability Condition, and Its Converse› context CleanRepr_Proofs begin text ‹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.› subsection ‹HBL1 from "proof-of" representability› definition P :: "'fmla" where "P ≡ exi yy (PPf (Var yy) (Var xx))" lemma P[simp,intro!]: "P ∈ fmla" and Fvars_P[simp]: "Fvars P = {xx}" unfolding P_def by (auto simp: PPf_def2) text ‹We infer HBL1 from Pf representing prv:› lemma HBL1: assumes φ: "φ ∈ fmla" "Fvars φ = {}" and pφ: "prv φ" shows "bprv (subst P ⟨φ⟩ xx)" proof- obtain "prf" where pf: "prf ∈ proof" and "prfOf prf φ" using prv_prfOf assms by auto hence 0: "bprv (PPf (encPf prf) (enc φ))" using prfOf_PPf φ by auto have 1: "subst (subst Pf (encPf prf) yy) ⟨φ⟩ xx = subst (subst Pf ⟨φ⟩ xx) (substT (encPf prf) ⟨φ⟩ 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 ‹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).› lemma not_prv_prv_neg_PPf: assumes [simp]: "φ ∈ fmla" "Fvars φ = {}" and p: "¬ prv φ" and n[simp]: "n ∈ num" shows "bprv (neg (PPf n ⟨φ⟩))" proof- have "∀prf∈proof. ¬ prfOf prf φ" using prv_prfOf p by auto hence "∀prf∈proof. bprv (neg (PPf (encPf prf) ⟨φ⟩))" using not_prfOf_PPf by auto thus ?thesis using not_prfOf_PPf using Clean_PPf_encPf by (cases "n ∈ encPf ` proof") auto qed lemma consistent_not_prv_not_prv_PPf: assumes c: consistent and 0[simp]: "φ ∈ fmla" "Fvars φ = {}" "¬ prv φ" "n ∈ num" shows "¬ bprv (PPf n ⟨φ⟩)" using not_prv_prv_neg_PPf[OF 0] c[THEN dwf_dwfd.consistent_B_consistent] unfolding B.consistent_def3 by auto end ― ‹context @{locale CleanRepr_Proofs}› text ‹The inference of HBL1 from "proof-of" representability, in locale form:› sublocale CleanRepr_Proofs < wrepr: HBL1 where P = P using HBL1 by unfold_locales auto subsection ‹Sufficient condition for the converse of HBL1› context CleanRepr_Proofs begin lemma PP_PPf: assumes "φ ∈ fmla" shows "wrepr.PP ⟨φ⟩ = exi yy (PPf (Var yy) ⟨φ⟩)" unfolding wrepr.PP_def using assms by (auto simp: PPf_def2 P_def) text ‹The converse of HLB1 condition follows from (the standard notion of) $\omega$-consistency for @{term bprv} and strong representability of proofs:› lemma ωconsistentStd1_HBL1_rev: assumes oc: "B.ωconsistentStd1" and φ[simp]: "φ ∈ fmla" "Fvars φ = {}" and iPP: "bprv (wrepr.PP ⟨φ⟩)" shows "prv φ" proof- have 0: "bprv (exi yy (PPf (Var yy) ⟨φ⟩))" using iPP by (simp add: PP_PPf) {assume "¬ prv φ" hence "∀n ∈ num. bprv (neg (PPf n ⟨φ⟩))" using not_prv_prv_neg_PPf by auto hence "¬ bprv (exi yy (PPf (Var yy) ⟨φ⟩))" using oc unfolding B.ωconsistentStd1_def using φ by auto hence False using 0 by simp } thus ?thesis by auto qed end ― ‹context @{locale CleanRepr_Proofs}› section ‹Second and Third Derivability Conditions› text ‹These are only needed for Gödel's Second.› 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 ("⟨_⟩") and P + assumes HBL2: "⋀φ χ. φ ∈ fmla ⟹ χ ∈ fmla ⟹ Fvars φ = {} ⟹ Fvars χ = {} ⟹ bprv (imp (cnj (PP ⟨φ⟩) (PP ⟨imp φ χ⟩)) (PP ⟨χ⟩))" and HBL3: "⋀φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹ bprv (imp (PP ⟨φ⟩) (PP ⟨PP ⟨φ⟩⟩))" begin text ‹The implicational form of HBL2:› lemma HBL2_imp: "⋀φ χ. φ ∈ fmla ⟹ χ ∈ fmla ⟹ Fvars φ = {} ⟹ Fvars χ = {} ⟹ bprv (imp (PP ⟨imp φ χ⟩) (imp (PP ⟨φ⟩) (PP ⟨χ⟩)))" using HBL2 by (simp add: B.prv_cnj_imp B.prv_imp_com) text ‹... and its weaker, "detached" version:› lemma HBL2_imp2: assumes "φ ∈ fmla" and "χ ∈ fmla" "Fvars φ = {}" "Fvars χ = {}" assumes "bprv (PP ⟨imp φ χ⟩)" shows "bprv (imp (PP ⟨φ⟩) (PP ⟨χ⟩))" using assms by (meson HBL2_imp PP enc imp num B.prv_imp_mp subsetCE) end ― ‹context @{locale HBL1_2_3}› (*<*) end (*>*)