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
      by (simp add: insert_absorb)
    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
(*>*)