Theory FinitenessClosedCharProp
theory FinitenessClosedCharProp
imports Closedness
begin
section ‹ Finiteness Character Property ›
text ‹ This theory formalises the theorem that states that subset closed propositional consistency properties can be extended to satisfy the finite character property.
The proof is by induction on the structure of propositional formulas based on the analysis of cases for the possible different types of formula in the sets of the collection of sets that hold the propositional consistency property.
›
definition finite_character :: "'a set set ⇒ bool" where
"finite_character 𝒞 = (∀S. S ∈ 𝒞 = (∀S'. finite S' ⟶ S' ⊆ S ⟶ S' ∈ 𝒞))"
theorem finite_character_closed:
assumes "finite_character 𝒞"
shows "subset_closed 𝒞"
proof -
{ fix S T
assume "S ∈ 𝒞" and "T ⊆ S"
have "T ∈ 𝒞" using "finite_character_def"
proof -
{ fix U
assume "finite U" and "U ⊆ T"
have "U ∈ 𝒞"
proof -
have "U ⊆ S" using `U ⊆ T` and `T ⊆ S` by simp
thus "U ∈ 𝒞" using `S ∈ 𝒞` and `finite U` and assms
by (unfold finite_character_def) blast
qed}
thus ?thesis using assms by( unfold finite_character_def) blast
qed }
thus ?thesis by(unfold subset_closed_def) blast
qed
definition closure_cfinite :: "'a set set ⇒ 'a set set" ("_⁻" [1000] 999) where
"𝒞⁻ = {S. ∀S'. S' ⊆ S ⟶ finite S' ⟶ S' ∈ 𝒞}"
lemma finite_character_subset:
assumes "subset_closed 𝒞"
shows "𝒞 ⊆ 𝒞⁻"
proof -
{ fix S
assume "S ∈ 𝒞"
have "S ∈ 𝒞⁻"
proof -
{ fix S'
assume "S' ⊆ S" and "finite S'"
hence "S' ∈ 𝒞" using `subset_closed 𝒞` and `S ∈ 𝒞`
by (simp add: subset_closed_def)}
thus ?thesis by (simp add: closure_cfinite_def)
qed}
thus ?thesis by auto
qed
lemma finite_character: "finite_character (𝒞⁻)"
proof (unfold finite_character_def)
show "∀S. (S ∈ 𝒞⁻) = (∀S'. finite S' ⟶ S' ⊆ S ⟶ S' ∈ 𝒞⁻)"
proof
fix S
{ assume "S ∈ 𝒞⁻"
hence "∀S'. finite S' ⟶ S' ⊆ S ⟶ S' ∈ 𝒞⁻"
by(simp add: closure_cfinite_def)}
moreover
{ assume "∀S'. finite S' ⟶ S' ⊆ S ⟶ S' ∈ 𝒞⁻"
hence "S ∈ 𝒞⁻" by(simp add: closure_cfinite_def)}
ultimately
show "(S ∈ 𝒞⁻) = (∀S'. finite S' ⟶ S' ⊆ S ⟶ S' ∈ 𝒞⁻)"
by blast
qed
qed
lemma cond_characterP1:
assumes "consistenceP 𝒞"
and "subset_closed 𝒞"
and hip: "∀S'⊆S. finite S' ⟶ S' ∈ 𝒞"
shows "(∀P. ¬(atom P ∈ S ∧ (¬.atom P) ∈ S))"
proof (rule allI)+
fix P t
show "¬(atom P ∈ S ∧ (¬.atom P) ∈ S)"
proof (rule notI)
assume "atom P ∈ S ∧ (¬.atom P) ∈ S"
hence "{atom P , ¬.atom P} ⊆ S" by simp
hence "{atom P, ¬.atom P} ∈ 𝒞" using hip by simp
moreover
have "∀S. S ∈ 𝒞 ⟶ (∀P ts. ¬(atom P ∈ S ∧ (¬.atom P) ∈ S))"
using `consistenceP 𝒞`
by (simp add: consistenceP_def)
ultimately
have "¬(atom P ∈ {atom P , ¬.atom P} ∧
(¬.atom P) ∈ {atom P, ¬.atom P})"
by auto
thus False by simp
qed
qed
lemma cond_characterP2:
assumes "consistenceP 𝒞"
and "subset_closed 𝒞"
and hip: "∀S'⊆S. finite S' ⟶ S' ∈ 𝒞"
shows "FF ∉ S ∧ (¬.TT)∉ S"
proof -
have "FF ∉ S"
proof(rule notI)
assume "FF ∈ S"
hence "{FF} ⊆ S" by simp
hence "{FF}∈ 𝒞" using hip by simp
moreover
have "∀S. S ∈ 𝒞 ⟶ FF ∉ S" using `consistenceP 𝒞`
by (simp add: consistenceP_def)
ultimately
have "FF ∉ {FF}" by auto
thus False by simp
qed
moreover
have "(¬.TT)∉ S"
proof(rule notI)
assume "(¬.TT) ∈ S"
hence "{¬.TT} ⊆ S" by simp
hence "{¬.TT}∈ 𝒞" using hip by simp
moreover
have "∀S. S ∈ 𝒞 ⟶ (¬.TT) ∉ S" using `consistenceP 𝒞`
by (simp add: consistenceP_def)
ultimately
have "(¬.TT) ∉ {(¬.TT)}" by auto
thus False by simp
qed
ultimately show ?thesis by simp
qed
text‹ ›
lemma cond_characterP3:
assumes "consistenceP 𝒞"
and "subset_closed 𝒞"
and hip: "∀S'⊆S. finite S' ⟶ S' ∈ 𝒞"
shows "∀F. (¬.¬.F) ∈ S ⟶ S ∪ {F} ∈ 𝒞⁻"
proof (rule allI)
fix F
show "(¬.¬.F) ∈ S ⟶ S ∪ {F} ∈ 𝒞⁻"
proof (rule impI)
assume "(¬.¬.F) ∈ S"
show "S ∪ {F} ∈ 𝒞⁻"
proof (unfold closure_cfinite_def)
show "S ∪ {F} ∈ {S. ∀S'⊆S. finite S' ⟶ S' ∈ 𝒞}"
proof (rule allI impI CollectI)+
fix S'
assume "S' ⊆ S ∪ {F}" and "finite S'"
show "S' ∈ 𝒞"
proof -
have "S' - {F} ∪ {¬.¬.F} ⊆ S"
using `(¬.¬.F) ∈ S` and `S'⊆ S ∪ {F}` by auto
moreover
have "finite (S' - {F} ∪ {¬.¬.F})" using `finite S'` by auto
ultimately
have "(S' - {F} ∪ {¬.¬.F}) ∈ 𝒞" using hip by simp
moreover
have "(¬.¬.F) ∈ (S' - {F} ∪ {¬.¬.F})" by simp
ultimately
have "(S' - {F} ∪ {¬.¬.F})∪ {F} ∈ 𝒞"
using `consistenceP 𝒞` by (simp add: consistenceP_def)
moreover
have "(S' - {F} ∪ {¬.¬.F})∪ {F} = (S' ∪ {¬.¬.F})∪ {F}"
by auto
ultimately
have "(S' ∪ {¬.¬.F})∪ {F} ∈ 𝒞" by simp
moreover
have "S' ⊆ (S' ∪ {¬.¬.F})∪ {F}" by auto
ultimately
show "S'∈ 𝒞" using `subset_closed 𝒞`
by (simp add: subset_closed_def)
qed
qed
qed
qed
qed
lemma cond_characterP4:
assumes "consistenceP 𝒞"
and "subset_closed 𝒞"
and hip: "∀S'⊆S. finite S' ⟶ S' ∈ 𝒞"
shows "(∀F. ((FormulaAlfa F) ∧ F ∈ S) ⟶ (S ∪ {Comp1 F, Comp2 F}) ∈ 𝒞⁻)"
proof (rule allI)
fix F
show "((FormulaAlfa F) ∧ F ∈ S) ⟶ S ∪ {Comp1 F, Comp2 F} ∈ 𝒞⁻"
proof (rule impI)
assume "(FormulaAlfa F) ∧ F ∈ S"
hence "(FormulaAlfa F)" and "F ∈ S" by auto
show "S ∪ {Comp1 F, Comp2 F} ∈ 𝒞⁻"
proof (unfold closure_cfinite_def)
show "S ∪ {Comp1 F, Comp2 F} ∈ {S. ∀S'⊆S. finite S' ⟶ S' ∈ 𝒞}"
proof (rule allI impI CollectI)+
fix S'
assume "S' ⊆ S ∪ {Comp1 F, Comp2 F}" and "finite S'"
show "S' ∈ 𝒞"
proof -
have "S' - {Comp1 F, Comp2 F} ∪ {F} ⊆ S"
using `F ∈ S` and `S'⊆ S ∪ {Comp1 F, Comp2 F}` by auto
moreover
have "finite (S' - {Comp1 F, Comp2 F} ∪ {F})"
using `finite S'` by auto
ultimately
have "(S' - {Comp1 F, Comp2 F} ∪ {F}) ∈ 𝒞" using hip by simp
moreover
have "F ∈ (S' - {Comp1 F, Comp2 F} ∪ {F})" by simp
ultimately
have "(S' - {Comp1 F, Comp2 F} ∪ {F}) ∪ {Comp1 F, Comp2 F} ∈ 𝒞"
using `consistenceP 𝒞` `FormulaAlfa F`
by (simp add: consistenceP_def)
moreover
have "(S' - {Comp1 F, Comp2 F} ∪ {F}) ∪ {Comp1 F, Comp2 F} =
(S' ∪ {F}) ∪ {Comp1 F, Comp2 F}"
by auto
ultimately
have "(S' ∪ {F}) ∪ {Comp1 F, Comp2 F} ∈ 𝒞" by simp
moreover
have "S' ⊆ (S' ∪ {F}) ∪ {Comp1 F, Comp2 F}" by auto
ultimately
show "S'∈ 𝒞" using `subset_closed 𝒞`
by (simp add: subset_closed_def)
qed
qed
qed
qed
qed
lemma cond_characterP5:
assumes "consistenceP 𝒞"
and "subset_closed 𝒞"
and hip: "∀S'⊆S. finite S' ⟶ S' ∈ 𝒞"
shows "∀F. FormulaBeta F ∧ F ∈ S ⟶ S ∪ {Comp1 F} ∈ 𝒞⁻ ∨ S ∪ {Comp2 F} ∈ 𝒞⁻"
proof (rule allI)
fix F
show "FormulaBeta F ∧ F ∈ S ⟶ S ∪ {Comp1 F} ∈ 𝒞⁻ ∨ S ∪ {Comp2 F} ∈ 𝒞⁻"
proof (rule impI)
assume "(FormulaBeta F) ∧ F ∈ S"
hence "FormulaBeta F" and "F ∈ S" by auto
show "S ∪ {Comp1 F} ∈ 𝒞⁻ ∨ S ∪ {Comp2 F} ∈ 𝒞⁻"
proof (rule ccontr)
assume "¬(S ∪ {Comp1 F} ∈ 𝒞⁻ ∨ S ∪ {Comp2 F} ∈ 𝒞⁻)"
hence "S ∪ {Comp1 F} ∉ 𝒞⁻ ∧ S ∪ {Comp2 F} ∉ 𝒞⁻" by simp
hence 1: "∃ S1. (S1 ⊆ S ∪ {Comp1 F} ∧ finite S1 ∧ S1 ∉ 𝒞)"
and 2: "∃ S2. (S2 ⊆ S ∪ {Comp2 F} ∧ finite S2 ∧ S2 ∉ 𝒞)"
by (auto simp add: closure_cfinite_def)
obtain S1 where S1: "S1 ⊆ S ∪ {Comp1 F} ∧ finite S1 ∧ S1 ∉ 𝒞"
using 1 by auto
obtain S2 where S2: "S2 ⊆ S ∪ {Comp2 F} ∧ finite S2 ∧ S2 ∉ 𝒞"
using 2 by auto
have "(S1-{Comp1 F}) ∪ (S2-{Comp2 F}) ∪ {F} ⊆ S"
using `F ∈ S` S1 S2 by auto
moreover
have "finite ((S1-{Comp1 F}) ∪ (S2-{Comp2 F}) ∪ {F})"
using S1 and S2 by simp
ultimately
have "(S1-{Comp1 F}) ∪ (S2-{Comp2 F}) ∪ {F} ∈ 𝒞" using hip by simp
moreover
have "F ∈ (S1-{Comp1 F}) ∪ (S2-{Comp2 F}) ∪ {F}" by simp
ultimately
have 3: "((S1-{Comp1 F}) ∪ (S2-{Comp2 F}) ∪ {F} ∪ {Comp1 F}) ∈ 𝒞 ∨
((S1-{Comp1 F}) ∪ (S2-{Comp2 F}) ∪ {F} ∪ {Comp2 F}) ∈ 𝒞"
using `consistenceP 𝒞` `FormulaBeta F`
by (simp add: consistenceP_def)
hence "S1 ∈ 𝒞 ∨ S2 ∈ 𝒞"
proof (cases)
assume "((S1-{Comp1 F}) ∪ (S2-{Comp2 F}) ∪ {F} ∪ {Comp1 F}) ∈ 𝒞"
moreover
have "S1 ⊆ ((S1-{Comp1 F}) ∪ (S2-{Comp2 F}) ∪ {F} ∪ {Comp1 F})"
by auto
ultimately
have "S1 ∈ 𝒞" using `subset_closed 𝒞`
by (simp add: subset_closed_def)
thus ?thesis by simp
next
assume "¬((S1-{Comp1 F}) ∪ (S2-{Comp2 F}) ∪ {F} ∪ {Comp1 F}) ∈ 𝒞"
hence "((S1-{Comp1 F}) ∪ (S2-{Comp2 F}) ∪ {F} ∪ {Comp2 F}) ∈ 𝒞"
using 3 by simp
moreover
have "S2 ⊆ ((S1-{Comp1 F}) ∪ (S2-{Comp2 F}) ∪ {F} ∪ {Comp2 F})"
by auto
ultimately
have "S2 ∈ 𝒞" using `subset_closed 𝒞`
by (simp add: subset_closed_def)
thus ?thesis by simp
qed
thus False using S1 and S2 by simp
qed
qed
qed
theorem cfinite_consistenceP:
assumes hip1: "consistenceP 𝒞" and hip2: "subset_closed 𝒞"
shows "consistenceP (𝒞⁻)"
proof -
{ fix S
assume "S ∈ 𝒞⁻"
hence hip3: "∀S'⊆S. finite S' ⟶ S' ∈ 𝒞"
by (simp add: closure_cfinite_def)
have "(∀P. ¬(atom P ∈ S ∧ (¬.atom P) ∈ S)) ∧
FF ∉ S ∧ (¬.TT) ∉ S ∧
(∀F. (¬.¬.F) ∈ S ⟶ S ∪ {F} ∈ 𝒞⁻) ∧
(∀F. ((FormulaAlfa F) ∧ F ∈ S) ⟶ (S ∪ {Comp1 F, Comp2 F}) ∈ 𝒞⁻) ∧
(∀F. ((FormulaBeta F) ∧ F ∈ S) ⟶
(S ∪ {Comp1 F} ∈ 𝒞⁻) ∨ (S ∪ {Comp2 F} ∈ 𝒞⁻))"
using
cond_characterP1[OF hip1 hip2 hip3] cond_characterP2[OF hip1 hip2 hip3]
cond_characterP3[OF hip1 hip2 hip3] cond_characterP4[OF hip1 hip2 hip3]
cond_characterP5[OF hip1 hip2 hip3] by auto }
thus ?thesis by (simp add: consistenceP_def)
qed
end