# Theory Deduction2

```chapter ‹Deduction with Two Provability Relations›
(*<*)
theory Deduction2 imports "Syntax_Independent_Logic.Deduction"
begin
(*>*)

text ‹We work with two provability relations:
provability @{term prv} and basic provability @{term bprv}.›

section ‹From Deduction with One Provability Relation to Two›

locale Deduct2 =
Deduct
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
prv
+
B: Deduct
var trm fmla Var FvarsT substT Fvars subst
num
eql cnj imp all exi
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
+
assumes bprv_prv: "⋀φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹ bprv φ ⟹ prv φ"
begin

(* Removing the sentence (empty Fvars) hypothesis from bprv_prv *)
lemma bprv_prv':
assumes φ: "φ ∈ fmla" and b: "bprv φ"
shows "prv φ"
proof-
obtain V where V: "Fvars φ = V" by blast
have VV: "V ⊆ var" using Fvars V φ by blast
have f: "finite V" using V finite_Fvars[OF φ] by auto
thus ?thesis using φ b V VV
proof(induction V arbitrary: φ rule: finite.induct)
case (emptyI φ)
then show ?case by (simp add: bprv_prv)
next
case (insertI W v φ)
show ?case proof(cases "v ∈ W")
case True
thus ?thesis
using insertI.IH[OF ‹φ ∈ fmla›] insertI.prems
next
case False
hence 1: "Fvars (all v φ) = W"
using insertI.prems by auto
moreover have "bprv (all v φ)"
using B.prv_all_gen insertI.prems by auto
ultimately have "prv (all v φ)" using insertI by auto
thus ?thesis using allE_id insertI.prems by blast
qed
qed
qed

end ― ‹context @{locale Deduct2}›

locale Deduct2_with_False =
Deduct_with_False
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
num
prv
+
B: Deduct_with_False
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
num
bprv
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 num
and prv bprv
+
assumes bprv_prv: "⋀φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹ bprv φ ⟹ prv φ"

sublocale Deduct2_with_False < d_dwf: Deduct2
by standard (fact bprv_prv)

context Deduct2_with_False begin

lemma consistent_B_consistent: "consistent ⟹ B.consistent"
using B.consistent_def bprv_prv consistent_def by blast

end ― ‹context @{locale Deduct2_with_False}›

locale Deduct2_with_False_Disj =
Deduct_with_False_Disj
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
prv
+
B: Deduct_with_False_Disj
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
bprv
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
+
assumes bprv_prv: "⋀φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹ bprv φ ⟹ prv φ"

sublocale Deduct2_with_False_Disj < dwf_dwfd: Deduct2_with_False
by standard (fact bprv_prv)

(* Factoring in a strict-order-like relation (not actually required to be an order): *)
locale Deduct2_with_PseudoOrder =
Deduct2_with_False_Disj
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
prv bprv
+
Syntax_PseudoOrder
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
Lq
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 Lq
+
assumes
(* We do not assume any ordering properties, but only these two axioms, Lq_num and Lq_num2,
which (interestingly) would be satisfied by both ≤ and < within a sufficiently strong
arithmetic such as Robinson's Q *)
(* For each formula φ(z) and numeral q, if φ(p) is provable for all p
then ∀ z ≤ q. φ(z) is provable.
(Note that a more natural property would assume φ(p) is provable for all p≤q,
but we can get away with the stronger assumption (on the left of the implication). )
*)
Lq_num:
"let LLq = (λ t1 t2. psubst Lq [(t1,zz), (t2,yy)]) in
∀ φ ∈ fmla. ∀ q ∈ num. Fvars φ = {zz} ∧ (∀ p ∈ num. bprv (subst φ p zz))
⟶ prv (all zz (imp (LLq (Var zz) q) φ))"
and
(* For each numeral p, there exists a finite set P such that it is provable that
∀ y. (⋁p∈P. x = p) ∨ y ≤ p
(where we write ≤ instead of Lq, but could also think of <):
*)
Lq_num2:
"let LLq = (λ t1 t2. psubst Lq [(t1,zz), (t2,yy)]) in
∀ p ∈ num. ∃ P ⊆ num. finite P ∧ prv (dsj (sdsj {eql (Var yy) r | r. r ∈ P}) (LLq p (Var yy)))"
begin

lemma LLq_num:
assumes "φ ∈ fmla" "q ∈ num" "Fvars φ = {zz}" "∀ p ∈ num. bprv (subst φ p zz)"
shows "prv (all zz (imp (LLq (Var zz) q) φ))"
using assms Lq_num unfolding LLq_def by auto

lemma LLq_num2:
assumes "p ∈ num"
shows "∃ P ⊆ num. finite P ∧ prv (dsj (sdsj {eql (Var yy) r | r. r ∈ P}) (LLq p (Var yy)))"
using assms Lq_num2 unfolding LLq_def by auto

end ― ‹context @{locale Deduct2_with_PseudoOrder}›

section ‹Factoring In Explicit Proofs›

locale Deduct_with_Proofs =
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 prv
+
fixes
"proof" :: "'proof set"
and
prfOf :: "'proof ⇒ 'fmla ⇒ bool"
assumes
― ‹Provability means there exists a proof (only needed for sentences):›
prv_prfOf: "⋀ φ. φ ∈ fmla ⟹ Fvars φ = {} ⟹ prv φ ⟷ (∃ prf ∈ proof. prfOf prf φ)"

(* We consider proof structure only for prv, not for bprv *)
locale Deduct2_with_Proofs =
Deduct2_with_False_Disj
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
prv bprv
+
Deduct_with_Proofs
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
prv
"proof" prfOf
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 "proof" :: "'proof set" and prfOf

locale Deduct2_with_Proofs_PseudoOrder =
Deduct2_with_Proofs
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
prv bprv
"proof" prfOf
+
Deduct2_with_PseudoOrder
var trm fmla Var FvarsT substT Fvars subst
eql cnj imp all exi
fls
dsj
num
prv bprv
Lq
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 "proof" :: "'proof set" and prfOf
and Lq

(*<*)
end
(*>*)```