Theory Derivability_Conditions

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
(*>*)