Theory Standard_Model_More

chapter ‹Standard Models with Two Provability Relations›

(*<*)
(* Abstract notion of standard model and truth  *)
theory Standard_Model_More
imports Derivability_Conditions "Syntax_Independent_Logic.Standard_Model"
begin
(*>*)

locale Minimal_Truth_Soundness_Proof_Repr =
CleanRepr_Proofs
  var trm fmla Var FvarsT substT Fvars subst
  num
  eql cnj imp all exi
  prv bprv
  enc
  fls
  dsj
  "proof" prfOf
  encPf
  Pf
+ ― ‹The label "B" stands for "basic", as a reminder that soundness
refers to the basic provability relation:›
B: Minimal_Truth_Soundness
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  dsj
  num
  bprv
  isTrue
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and eql cnj imp all exi
and fls
and dsj
and num
and prv bprv
and isTrue
and enc ("⟨_⟩")
and "proof" :: "'proof set" and prfOf
and encPf Pf
begin

lemmas prfOf_iff_PPf = B_consistent_prfOf_iff_PPf[OF B.consistent]

text ‹The provability predicate is decided by basic provability on encodings:›
lemma isTrue_prv_PPf_prf_or_neg:
"prf ∈ proof ⟹ φ ∈ fmla ⟹ Fvars φ = {} ⟹
    bprv (PPf (encPf prf) ⟨φ⟩) ∨ bprv (neg (PPf (encPf prf) ⟨φ⟩))"
  using not_prfOf_PPf prfOf_PPf by blast

text ‹... hence that predicate is complete w.r.t. truth:›
lemma isTrue_PPf_Implies_bprv_PPf:
"prf ∈ proof ⟹ φ ∈ fmla ⟹ Fvars φ = {} ⟹
   isTrue (PPf (encPf prf) ⟨φ⟩) ⟹ bprv (PPf (encPf prf) ⟨φ⟩)"
  by (metis FvarsT_num Fvars_PPf Fvars_fls PPf
Un_empty empty_iff enc encPf fls in_num isTrue_prv_PPf_prf_or_neg
neg_def B.not_isTrue_fls B.prv_imp_implies_isTrue)

text ‹... and thanks cleanness we can replace encoded proofs
with arbitrary numerals in the completeness property:›
lemma isTrue_implies_bprv_PPf:
assumes [simp]: "n ∈ num" "φ ∈ fmla" "Fvars φ = {}"
and iT: "isTrue (PPf n ⟨φ⟩)"
shows "bprv (PPf n ⟨φ⟩)"
proof(cases "n ∈ encPf ` proof")
  case True
  thus ?thesis
    using iT isTrue_PPf_Implies_bprv_PPf by auto
next
  case False
  hence "bprv (neg (PPf n ⟨φ⟩))" by (simp add: Clean_PPf_encPf)
  hence "isTrue (neg (PPf n ⟨φ⟩))" by (intro B.sound_isTrue) auto
  hence False using iT by (intro B.isTrue_neg_excl) auto
  thus ?thesis by auto
qed

text ‹... in fact, by @{locale Minimal_Truth_Soundness} we even have an iff:›
lemma isTrue_iff_bprv_PPf:
"⋀ n φ. n ∈ num ⟹ φ ∈ fmla ⟹ Fvars φ = {} ⟹ isTrue (PPf n ⟨φ⟩) ⟷ bprv (PPf n ⟨φ⟩)"
using isTrue_implies_bprv_PPf
using exists_no_Fvars B.not_isTrue_fls B.sound_isTrue by auto

text ‹Truth of the provability representation implies provability (TIP):›
lemma TIP:
assumes φ[simp]: "φ ∈ fmla" "Fvars φ = {}"
and iPP: "isTrue (wrepr.PP ⟨φ⟩)"
shows "prv φ"
proof-
  have "isTrue (exi yy (PPf (Var yy) ⟨φ⟩))" using iPP unfolding PP_PPf[OF φ(1)] .
  from B.isTrue_exi[OF _ _ _ this]
  obtain n where n[simp]: "n ∈ num" and "isTrue (PPf n ⟨φ⟩)" by auto
  hence pP: "bprv (PPf n ⟨φ⟩)" using isTrue_implies_bprv_PPf by auto
  hence "¬ bprv (neg (PPf n ⟨φ⟩))"
  using B.prv_neg_excl[of "PPf n ⟨φ⟩"] by auto
  then obtain "prf" where "prf"[simp]: "prf ∈ proof" and nn: "n = encPf prf"
  using assms n Clean_PPf_encPf φ(1) by blast
  have "prfOf prf φ" using pP unfolding nn using prfOf_iff_PPf by auto
  thus ?thesis using prv_prfOf by auto
qed

text ‹The reverse HBL1 -- now without the $\omega$-consistency assumption which holds here
thanks to our truth-in-standard-model assumption:›

lemmas HBL1_rev = ωconsistentStd1_HBL1_rev[OF B.ωconsistentStd1]
text ‹Note that the above would also follow by @{locale Minimal_Truth_Soundness} from TIP:›
lemma TIP_implies_HBL1_rev:
assumes TIP: "∀φ. φ ∈ fmla ∧ Fvars φ = {} ∧ isTrue (wrepr.PP ⟨φ⟩) ⟶ prv φ"
shows "∀φ. φ ∈ fmla ∧ Fvars φ = {} ∧ bprv (wrepr.PP ⟨φ⟩) ⟶ prv φ"
using B.sound_isTrue[of "wrepr.PP ⟨_⟩"] TIP by auto

end ― ‹context @{locale Minimal_Truth_Soundness_Proof_Repr}›


section ‹Proof recovery from $\mathit{HBL1\_iff}$›

locale Minimal_Truth_Soundness_HBL1iff_Compl_Pf =
HBL1
  var trm fmla Var FvarsT substT Fvars subst
  num
  eql cnj imp all exi
  prv bprv
  enc
  P
+
B : Minimal_Truth_Soundness
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  dsj
  num
  bprv
  isTrue
+
Deduct_with_False_Disj
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  dsj
  num
  prv
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and eql cnj imp all exi
and fls
and dsj
and num
and enc ("⟨_⟩")
and prv bprv
and P
and isTrue
+
fixes Pf :: 'fmla
assumes
― ‹@{term Pf} is a formula with free variables @{term xx} @{term yy}:›
Pf[simp,intro!]: "Pf ∈ fmla"
and
Fvars_Pf[simp]: "Fvars Pf = {yy,xx}"
and
― ‹@{term P} relates to @{term Pf} internally (inside basic provability)
just like a @{term prv} and a @{term prfOf} would relate---via an existential:›
P_Pf:
"φ ∈ fmla ⟹ Fvars φ = {} ⟹
 let PPf = (λ t1 t2. psubst Pf [(t1,yy), (t2,xx)]) in
 bprv (eqv (subst P ⟨φ⟩ xx) (exi yy (PPf (Var yy) ⟨φ⟩)))"
assumes
― ‹We assume both $\mathit{HBL1}$ and $\mathit{HBL1\_rev}$, i.e., an iff version:›
HBL1_iff: "⋀ φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹ bprv (PP ⟨φ⟩) ⟷ prv φ"
and
Compl_Pf:
"⋀ n φ. n ∈ num ⟹ φ ∈ fmla ⟹ Fvars φ = {} ⟹
 let PPf = (λ t1 t2. psubst Pf [(t1,yy), (t2,xx)]) in
 isTrue (PPf n ⟨φ⟩) ⟶ bprv (PPf n ⟨φ⟩)"
begin

definition PPf where "PPf ≡ λ t1 t2. psubst Pf [(t1,yy), (t2,xx)]"

lemma PP_deff: "PP t = subst P t xx" using PP_def by auto

lemma PP_PPf_eqv:
  "φ ∈ fmla ⟹ Fvars φ = {} ⟹ bprv (eqv (PP ⟨φ⟩) (exi yy (PPf (Var yy) ⟨φ⟩)))"
  using PP_deff PPf_def P_Pf by auto

(*  *)

lemma PPf[simp,intro!]: "t1 ∈ trm ⟹ t2 ∈ trm ⟹ xx ∉ FvarsT t1 ⟹ PPf t1 t2 ∈ fmla"
  unfolding PPf_def by auto

lemma PPf_def2: "t1 ∈ trm ⟹ t2 ∈ trm ⟹ xx ∉ FvarsT t1 ⟹
  PPf t1 t2 = subst (subst Pf t1 yy) t2 xx"
  unfolding PPf_def by (rule psubst_eq_rawpsubst2[simplified]) auto

lemma Fvars_PPf[simp]:
  "t1 ∈ trm ⟹ t2 ∈ trm ⟹ xx ∉ FvarsT t1 ⟹ Fvars (PPf t1 t2) = FvarsT t1 ∪ FvarsT t2"
  by (auto simp add: PPf_def2 subst2_fresh_switch)

lemma [simp]:
"n ∈ num ⟹ subst (PPf (Var yy) (Var xx)) n xx = PPf (Var yy) n"
"m ∈ num ⟹ n ∈ num ⟹ subst (PPf (Var yy) m) n yy = PPf n m"
"n ∈ num ⟹ subst (PPf (Var yy) (Var xx)) n yy = PPf n (Var xx)"
"m ∈ num ⟹ n ∈ num ⟹ subst (PPf m (Var xx)) n xx = PPf m n"
"m ∈ num ⟹ subst (PPf (Var zz) (Var xx')) m zz = PPf m (Var xx')"
"m ∈ num ⟹ n ∈ num ⟹ subst (PPf m (Var xx')) n xx' = PPf m n"
"n ∈ num ⟹ subst (PPf (Var zz) (Var xx')) n xx' = PPf (Var zz) n"
"m ∈ num ⟹ n ∈ num ⟹ subst (PPf (Var zz) n) m zz = PPf m n"
  by (auto simp: PPf_def2 subst2_fresh_switch)

(* *)

lemma PP_PPf:
assumes "φ ∈ fmla" "Fvars φ = {}" shows "bprv (PP ⟨φ⟩) ⟷ bprv (exi yy (PPf (Var yy) ⟨φ⟩))"
  using assms PP_PPf_eqv[OF assms] B.prv_eqv_sym[OF _ _ PP_PPf_eqv[OF assms]]
  by (auto intro!: B.prv_eqv_prv[of "PP ⟨φ⟩" "exi yy (PPf (Var yy) ⟨φ⟩)"]
    B.prv_eqv_prv[of "exi yy (PPf (Var yy) ⟨φ⟩)" "PP ⟨φ⟩"])

lemma isTrue_implies_bprv_PPf:
"⋀ n φ. n ∈ num ⟹ φ ∈ fmla ⟹ Fvars φ = {} ⟹
 isTrue (PPf n ⟨φ⟩) ⟹ bprv (PPf n ⟨φ⟩)"
  using Compl_Pf by(simp add: PPf_def)

lemma isTrue_iff_bprv_PPf:
"⋀ n φ. n ∈ num ⟹ φ ∈ fmla ⟹ Fvars φ = {} ⟹ isTrue (PPf n ⟨φ⟩) ⟷ bprv (PPf n ⟨φ⟩)"
using isTrue_implies_bprv_PPf
  using exists_no_Fvars B.not_isTrue_fls B.sound_isTrue by auto

text ‹Preparing to instantiate this "proof recovery" alternative into our
mainstream locale hierarchy, which assumes proofs.
We define the "missing" proofs to be numerals, we encode them as the identity,
and we "copy" @{term prfOf} from the corresponding predicate one-level-up, @{term PPf}:›

definition "proof" :: "'trm set" where [simp]: "proof = num"
definition prfOf :: "'trm ⇒ 'fmla ⇒ bool" where
  "prfOf n φ ≡ bprv (PPf n ⟨φ⟩)"
definition encPf :: "'trm ⇒ 'trm" where [simp]: "encPf ≡ id"
(*  *)

lemma prv_exi_PPf_iff_isTrue:
assumes [simp]: "φ ∈ fmla" "Fvars φ = {}"
shows "bprv (exi yy (PPf (Var yy) ⟨φ⟩)) ⟷ isTrue (exi yy (PPf (Var yy) ⟨φ⟩))" (is "?L ⟷ ?R")
proof
  assume ?L thus ?R by (intro B.sound_isTrue) auto
next
  assume ?R
  obtain n where n[simp]: "n ∈ num" and i: "isTrue (PPf n ⟨φ⟩)" using B.isTrue_exi[OF _ _ _ ‹?R›] by auto
  hence "bprv (PPf n ⟨φ⟩)" by (auto simp: isTrue_iff_bprv_PPf)
  thus ?L by (intro B.prv_exiI[of _ _ n]) auto
qed

lemma isTrue_exi_iff:
assumes [simp]: "φ ∈ fmla" "Fvars φ = {}"
shows "isTrue (exi yy (PPf (Var yy) ⟨φ⟩)) ⟷ (∃n∈num. isTrue (PPf n ⟨φ⟩))" (is "?L ⟷ ?R")
proof
  assume ?L thus ?R using B.isTrue_exi[OF _ _ _ ‹?L›] by auto
next
  assume ?R
  then obtain n where n[simp]: "n ∈ num" and i: "isTrue (PPf n ⟨φ⟩)" by auto
  hence "bprv (PPf n ⟨φ⟩)" by (auto simp: isTrue_iff_bprv_PPf)
  hence "bprv (exi yy (PPf (Var yy) ⟨φ⟩))" by (intro B.prv_exiI[of _ _ n]) auto
  thus ?L by (intro B.sound_isTrue) auto
qed

lemma prv_prfOf:
assumes "φ ∈ fmla" "Fvars φ = {}"
shows "prv φ ⟷ (∃n∈num. prfOf n φ)"
proof-
  have "prv φ ⟷ bprv (PP ⟨φ⟩)" using HBL1_iff[OF assms] by simp
  also have "… ⟷ bprv (exi yy (PPf (Var yy) ⟨φ⟩))" unfolding PP_PPf[OF assms] ..
  also have "… ⟷ isTrue (exi yy (PPf (Var yy) ⟨φ⟩))" using prv_exi_PPf_iff_isTrue[OF assms] .
  also have "… ⟷ (∃n∈num. isTrue (PPf n ⟨φ⟩))" using isTrue_exi_iff[OF assms] .
  also have "… ⟷ (∃n∈num. bprv (PPf n ⟨φ⟩))" using isTrue_iff_bprv_PPf[OF _ assms] by auto
  also have "… ⟷ (∃n∈num. prfOf n φ)" unfolding prfOf_def ..
  finally show ?thesis .
qed

lemma prfOf_prv_Pf:
assumes "n ∈ num" and "φ ∈ fmla" "Fvars φ = {}" and "prfOf n φ"
shows "bprv (psubst Pf [(n, yy), (⟨φ⟩, xx)])"
using assms unfolding prfOf_def by (auto simp: PPf_def2 psubst_eq_rawpsubst2)

lemma isTrue_exi_iff_PP:
assumes [simp]: "φ ∈ fmla" "Fvars φ = {}"
shows "isTrue (PP ⟨φ⟩) ⟷ (∃n∈num. isTrue (PPf n ⟨φ⟩))"
proof-
  have "bprv (eqv (PP ⟨φ⟩) (exi yy (PPf (Var yy) ⟨φ⟩)))"
    using PP_PPf_eqv by auto
  hence "bprv (imp (PP ⟨φ⟩) (exi yy (PPf (Var yy) ⟨φ⟩)))"
  and "bprv (imp (exi yy (PPf (Var yy) ⟨φ⟩)) (PP ⟨φ⟩))"
  by (simp_all add: B.prv_imp_eqvEL B.prv_imp_eqvER)
  thus ?thesis unfolding isTrue_exi_iff[OF assms, symmetric]
    by (intro iffI) (rule B.prv_imp_implies_isTrue; simp)+
qed

lemma bprv_compl_isTrue_PP_enc:
assumes 1: "φ ∈ fmla" "Fvars φ = {}" and 2: "isTrue (PP ⟨φ⟩)"
shows "bprv (PP ⟨φ⟩)"
proof-
  obtain n where nn: "n ∈ num" and i: "isTrue (PPf n ⟨φ⟩)"
   using 2 unfolding isTrue_exi_iff_PP[OF 1] ..
  hence "bprv (PPf n ⟨φ⟩)"
    using i using nn assms isTrue_iff_bprv_PPf by blast
  hence "bprv (exi yy (PPf (Var yy) ⟨φ⟩))"
  using 2 assms isTrue_exi_iff isTrue_exi_iff_PP prv_exi_PPf_iff_isTrue by auto
  thus ?thesis using PP_PPf 1 by blast
qed

lemma TIP:
assumes 1: "φ ∈ fmla" "Fvars φ = {}" and 2: "isTrue (PP ⟨φ⟩)"
shows "prv φ"
using bprv_compl_isTrue_PP_enc[OF assms] HBL1_iff assms by blast


end ― ‹context @{locale Minimal_Truth_Soundness_HBL1iff_Compl_Pf}›


locale Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf =
Minimal_Truth_Soundness_HBL1iff_Compl_Pf
+
assumes
Compl_NegPf:
"⋀ n φ. n ∈ num ⟹ φ ∈ fmla ⟹ Fvars φ = {} ⟹
 let PPf = (λ t1 t2. psubst Pf [(t1,yy), (t2,xx)]) in
 isTrue (B.neg (PPf n ⟨φ⟩)) ⟶ bprv (B.neg (PPf n ⟨φ⟩))"
begin

lemma isTrue_implies_prv_neg_PPf:
"⋀ n φ. n ∈ num ⟹ φ ∈ fmla ⟹ Fvars φ = {} ⟹
 isTrue (B.neg (PPf n ⟨φ⟩)) ⟹ bprv (B.neg (PPf n ⟨φ⟩))"
  using Compl_NegPf by(simp add: PPf_def)

lemma isTrue_iff_prv_neg_PPf:
"⋀ n φ. n ∈ num ⟹ φ ∈ fmla ⟹ Fvars φ = {} ⟹ isTrue (B.neg (PPf n ⟨φ⟩)) ⟷ bprv (B.neg (PPf n ⟨φ⟩))"
using isTrue_implies_prv_neg_PPf
  using exists_no_Fvars B.not_isTrue_fls B.sound_isTrue by auto

lemma prv_PPf_decide:
assumes [simp]: "n ∈ num" "φ ∈ fmla" "Fvars φ = {}"
and np: "¬ bprv (PPf n ⟨φ⟩)"
shows "bprv (B.neg (PPf n ⟨φ⟩))"
proof-
  have "¬ isTrue (PPf n ⟨φ⟩)" using assms by (auto simp: isTrue_iff_bprv_PPf)
  hence "isTrue (B.neg (PPf n ⟨φ⟩))" using B.isTrue_neg[of "PPf n ⟨φ⟩"] by auto
  thus ?thesis by (auto simp: isTrue_iff_prv_neg_PPf)
qed

lemma not_prfOf_prv_neg_Pf:
assumes nφ: "n ∈ num" "φ ∈ fmla" "Fvars φ = {}" and "¬ prfOf n φ"
shows "bprv (B.neg (psubst Pf [(n, yy), (⟨φ⟩, xx)]))"
  using assms prv_PPf_decide[OF nφ] by (auto simp: prfOf_def PPf_def2 psubst_eq_rawpsubst2)

end ― ‹context @{locale Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf}›

sublocale Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf <
   repr: CleanRepr_Proofs
(* added label to avoid duplicated constant P, which is assumed
in Minimal_Truth_Soundness_HBL1iff_Compl_Pf but defined in CleanRepr_Proofs
(they are of course extensionally equal).
*)
  where "proof" = "proof" and prfOf = prfOf and encPf = encPf
  by standard (auto simp: bprv_prv prv_prfOf prfOf_prv_Pf not_prfOf_prv_neg_Pf)

(* Lemma 6 ("proof recovery") from the JAR paper: *)
sublocale Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf <
  min_truth: Minimal_Truth_Soundness_Proof_Repr
where "proof" = "proof" and prfOf = prfOf and encPf = encPf
  by standard



(* FOR THE CLASSICAL REASONING VERSION *)

locale Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf =
HBL1
  var trm fmla Var FvarsT substT Fvars subst
  num
  eql cnj imp all exi
  prv bprv
  enc
  P
+
B: Minimal_Truth_Soundness
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  dsj
  num
  bprv
  isTrue
+
Deduct_with_False_Disj
  var trm fmla Var FvarsT substT Fvars subst
  eql cnj imp all exi
  fls
  dsj
  num
  prv
for
var :: "'var set" and trm :: "'trm set" and fmla :: "'fmla set"
and Var FvarsT substT Fvars subst
and eql cnj imp all exi
and fls
and dsj
and num
and enc ("⟨_⟩")
and prv bprv
and P
and isTrue
+
fixes Pf :: 'fmla
assumes
(* Pf is a formula with free variables xx yy  *)
Pf[simp,intro!]: "Pf ∈ fmla"
and
Fvars_Pf[simp]: "Fvars Pf = {yy,xx}"
and
(* P relates to Pf internally just like a prv and a proofOf would
relate: via an existential *)
P_Pf:
"φ ∈ fmla ⟹
 let PPf = (λ t1 t2. psubst Pf [(t1,yy), (t2,xx)]) in
 bprv (eqv (subst P ⟨φ⟩ xx) (exi yy (PPf (Var yy) ⟨φ⟩)))"
assumes
(* We assume, in addition to HBL1, the strong form of HBL1_rev: *)
HBL1_rev_prv: "⋀ φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹ prv (PP ⟨φ⟩) ⟹ prv φ"
and
Compl_Pf:
"⋀ n φ. n ∈ num ⟹ φ ∈ fmla ⟹ Fvars φ = {} ⟹
 let PPf = (λ t1 t2. psubst Pf [(t1,yy), (t2,xx)]) in
 isTrue (PPf n ⟨φ⟩) ⟶ bprv (PPf n ⟨φ⟩)"
begin

lemma HBL1_rev:
  assumes f: "φ ∈ fmla" and fv: "Fvars φ = {}" and bp: "bprv (PP ⟨φ⟩)"
  shows "prv φ"
  using assms by (auto intro!: HBL1_rev_prv bprv_prv[OF _ _ bp])

lemma HBL1_iff: "φ ∈ fmla ⟹ Fvars φ = {} ⟹ bprv (PP ⟨φ⟩) ⟷ prv φ"
  using HBL1 HBL1_rev unfolding PP_def by auto

lemma HBL1_iff_prv: "φ ∈ fmla ⟹ Fvars φ = {} ⟹ prv (PP ⟨φ⟩) ⟷ prv φ"
  by (intro iffI bprv_prv[OF _ _ HBL1_PP], elim HBL1_rev_prv[rotated -1]) auto

end ― ‹context @{locale Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf}›

sublocale Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf <
  mts_prv_mts: Minimal_Truth_Soundness_HBL1iff_Compl_Pf where Pf = Pf
  using P_Pf HBL1_rev HBL1_PP Compl_Pf
  by unfold_locales auto

locale Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf_Classical =
Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf
+
assumes
― ‹NB: we don't really need to assume classical reasoning (double negation) all throughout,
but only for the provability predicate:›
classical_P: "⋀ φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹ let PP = (λt. subst P t xx) in
  prv (B.neg (B.neg (PP ⟨φ⟩))) ⟹ prv (PP ⟨φ⟩)"
begin

lemma classical_PP: "φ ∈ fmla ⟹ Fvars φ = {} ⟹ prv (B.neg (B.neg (PP ⟨φ⟩))) ⟹ prv (PP ⟨φ⟩)"
  using classical_P unfolding PP_def by auto

end ― ‹context @{locale Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf_Classical}›

(*<*)
end
(*>*)