Theory Standard_Model_More
chapter ‹Standard Models with Two Provability Relations›
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
+
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
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
Pf[simp,intro!]: "Pf ∈ fmla"
and
Fvars_Pf[simp]: "Fvars Pf = {yy,xx}"
and
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
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
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
sublocale Minimal_Truth_Soundness_HBL1iff_Compl_Pf_Compl_NegPf <
repr: CleanRepr_Proofs
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)
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
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[simp,intro!]: "Pf ∈ fmla"
and
Fvars_Pf[simp]: "Fvars Pf = {yy,xx}"
and
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
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
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
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
end