Theory ND_Compl_SC

subsection‹An alternate proof of ND completeness›
theory ND_Compl_SC
imports SC_Sema ND_Sound SCND Compactness
begin

lemma ND_sound_complete_countable:
  fixes Γ :: "'a :: countable formula set"
  shows "Γ ⊢ F ⟷ Γ ⊫ F" (is "?n ⟷ ?s")
proof
  assume ?n thus ?s by (fact ND_sound)
next
  assume s: ?s
  with compact_entailment obtain Γ' where 0: "finite Γ'" "Γ' ⊫ F" "Γ' ⊆ Γ" 
    unfolding entailment_def by metis
  then obtain Γ'' where Γ'': "Γ' = set_mset Γ''" using finite_set_mset_mset_set by blast
  have su: "set_mset Γ'' ⊆ Γ" using 0  Γ'' by fast
  from 0 have "⊨ Γ'' ⇒ {#F#}" unfolding sequent_semantics_def entailment_def Γ'' by simp
  with SC_sound_complete have "Γ'' ⇒ {#F#}" by blast
  with SCND have "set_mset Γ'' ∪ ❙¬ ` set_mset {#F#} ⊢ ⊥" .
  thus ?n using ND.CC Weaken[OF _ su[THEN insert_mono]] by force
qed
  
text‹If you do not like the requirement that our atoms are countable,
you can also restrict yourself to a finite set of assumptions.›
  
lemma ND_sound_complete_finite:
  assumes "finite Γ"
  shows "Γ ⊢ F ⟷ Γ ⊫ F" (is "?n ⟷ ?s")
proof
  assume ?n thus ?s by (fact ND_sound)
next
  assume s: ?s
  then obtain Γ'' where Γ'': "Γ = set_mset Γ''" using finite_set_mset_mset_set assms by blast
  have su: "set_mset Γ'' ⊆ Γ" using Γ'' by fast
  have "⊨ Γ'' ⇒ {#F#}" using s unfolding sequent_semantics_def entailment_def Γ'' by auto
  with SC_sound_complete have "Γ'' ⇒ {#F#}" by blast
  with SCND have "set_mset Γ'' ∪ ❙¬ ` set_mset {#F#} ⊢ ⊥" .
  thus ?n using ND.CC Weaken[OF _ su[THEN insert_mono]] by force
qed

end