Theory ND_Compl_Truthtable_Compact

theory ND_Compl_Truthtable_Compact
imports ND_Compl_Truthtable Compactness
begin
  
theorem 
  fixes Γ :: "'a :: countable formula set"
  shows "Γ ⊫ F ⟹ Γ ⊢ F"
proof -
  assume ‹Γ ⊫ F›
  then obtain G  where "set G ⊆ Γ" "⊨ ❙⋀G ❙→ F" by (rule compact_to_formula)
  from ND_complete ‹⊨ ❙⋀G ❙→ F› have ‹{} ⊢ ❙⋀G ❙→ F› .
  with AssmBigAnd have ‹set G ⊢ F› ..
  with Weaken show ?thesis using ‹set G ⊆ Γ› .
qed
  

end