Theory AGM_Revision
theory AGM_Revision
imports AGM_Contraction
begin
section ‹Revisions›
text ‹The third operator of belief change introduce by the AGM framework is the revision. In revision a sentence
@{term ‹φ›} is added to the belief set @{term ‹K›} in such a way that other sentences
of @{term ‹K›} are removed if needed so that @{term ‹K›} is consistent›
subsection ‹AGM revision postulates›
text ‹The revision operator is denoted by the symbol @{text ‹❙*›} and respect the following conditions :
▪ @{text ‹revis_closure›} : a belief set @{term ‹K›} revised by @{term ‹φ›} should be logically closed
▪ @{text ‹revis_inclusion›} : a belief set @{term ‹K›} revised by @{term ‹φ›} should be a subset of @{term ‹K›} expanded by @{term ‹φ›}
▪ @{text ‹revis_vacuity›} : if @{text ‹¬φ›} is not in @{term ‹K›} then the revision of @{term ‹K›} by @{term ‹φ›} is equivalent of the expansion of @{term ‹K›} by @{term ‹φ›}
▪ @{text ‹revis_success›} : a belief set @{term ‹K›} revised by @{term ‹φ›} should contain @{term ‹φ›}
▪ @{text ‹revis_extensionality›} : Extensionality guarantees that the logic of contraction is extensional in the sense of allowing logically equivalent sentences to be freely substituted for each other
▪ @{text ‹revis_consistency›} : a belief set @{term ‹K›} revised by @{term ‹φ›} is consistent if @{term ‹φ›} is consistent›
locale AGM_Revision = Supraclassical_logic +
fixes revision:: ‹'a set ⇒ 'a ⇒ 'a set› (infix ‹❙*› 55)
assumes revis_closure: ‹K = Cn(A) ⟹ K ❙* φ = Cn(K ❙* φ)›
and revis_inclusion: ‹K = Cn(A) ⟹ K ❙* φ ⊆ K ⊕ φ›
and revis_vacuity: ‹K = Cn(A) ⟹ .¬ φ ∉ K ⟹ K ⊕ φ ⊆ K ❙* φ›
and revis_success: ‹K = Cn(A) ⟹ φ ∈ K ❙* φ›
and revis_extensionality: ‹K = Cn(A) ⟹ Cn({φ}) = Cn({ψ}) ⟹ K ❙* φ = K ❙* ψ›
and revis_consistency: ‹K = Cn(A) ⟹ .¬ φ ∉ Cn({}) ⟹ ⊥ ∉ K ❙* φ›
text‹A full revision is defined by two more postulates :
▪ @{text ‹revis_superexpansion›} : An element of @{text ‹ K ❙* (φ .∧. ψ)›} is also an element of @{term ‹K›} revised by @{term ‹φ›} and expanded by @{term ‹ψ›}
▪ @{text ‹revis_subexpansion›} : An element of @{text ‹(K ❙* φ) ⊕ ψ›} is also an element of @{term ‹K›} revised by @{text ‹φ .∧. ψ›} if @{text ‹(K ❙* φ)›} do not imply @{text ‹¬ ψ›}
›
locale AGM_FullRevision = AGM_Revision +
assumes revis_superexpansion: ‹K = Cn(A) ⟹ K ❙* (φ .∧. ψ) ⊆ (K ❙* φ) ⊕ ψ›
and revis_subexpansion: ‹K = Cn(A) ⟹ .¬ ψ ∉ (K ❙* φ) ⟹ (K ❙* φ) ⊕ ψ ⊆ K ❙* (φ .∧. ψ)›
begin
corollary revis_superexpansion_ext : ‹K = Cn(A) ⟹ (K ❙* φ) ∩ (K ❙* ψ) ⊆ (K ❙* (φ .∨. ψ))›
proof(intro subsetI, elim IntE)
fix χ
assume a:‹K = Cn(A)› and b:‹χ ∈ (K ❙* φ)› and c:‹χ ∈ (K ❙* ψ)›
have ‹ Cn({(φ' .∨. ψ') .∧. φ'}) = Cn({φ'})› for φ' ψ'
using conj_superexpansion2 by (simp add: Cn_same)
hence d:‹K ❙* φ' ⊆ (K ❙* (φ' .∨. ψ')) ⊕ φ'› for φ' ψ'
using revis_superexpansion[OF a, of ‹φ' .∨. ψ'› φ'] revis_extensionality a by metis
hence ‹φ .⟶. χ ∈ (K ❙* (φ .∨. ψ))› and ‹ψ .⟶. χ ∈ (K ❙* (φ .∨. ψ))›
using d[of φ ψ] d[of ψ φ] revis_extensionality[OF a disj_com_Cn, of ψ φ]
using imp_PL a b c expansion_def revis_closure by fastforce+
then show c:‹χ ∈ (K ❙* (φ .∨. ψ))›
using disjE_PL a revis_closure revis_success by fastforce
qed
end
subsection ‹Relation of AGM revision and AGM contraction ›
text‹The AGM contraction of @{term ‹K›} by @{term ‹φ›} can be defined as the AGM revision of @{term ‹K›} by @{text ‹¬φ›}
intersect with @{term ‹K›} (to remove @{text ‹¬φ›} from K revised). This definition is known as Harper identity \<^cite>‹"Harper1976"››
sublocale AGM_Revision ⊆ AGM_Contraction where contraction = ‹λK φ. K ∩ (K ❙* .¬ φ)›
proof(unfold_locales, goal_cases)
case closure:(1 K A φ)
then show ?case
by (metis Cn_inter revis_closure)
next
case inclusion:(2 K A φ)
then show ?case by blast
next
case vacuity:(3 K A φ)
hence ‹.¬ (.¬ φ) ∉ K›
using absurd_PL infer_def by blast
hence ‹K ⊆ (K ❙* .¬ φ)›
using revis_vacuity[where φ=‹.¬ φ›] expansion_def inclusion_L vacuity(1) by fastforce
then show ?case
by fast
next
case success:(4 K A φ)
hence ‹.¬ (.¬ φ) ∉ Cn({})›
using infer_def notnot_PL by blast
hence a:‹⊥ ∉ K ❙* (.¬ φ)›
by (simp add: revis_consistency success(1))
have ‹.¬ φ ∈ K ❙* (.¬ φ)›
by (simp add: revis_success success(1))
with a have ‹φ ∉ K ❙* (.¬ φ)›
using infer_def non_consistency revis_closure success(1) by blast
then show ?case
by simp
next
case recovery:(5 K A φ)
show ?case
proof
fix ψ
assume a:‹ψ ∈ K›
hence b:‹φ .⟶. ψ ∈ K› using impI2 recovery by auto
have ‹.¬ ψ .⟶. .¬ φ ∈ K ❙* .¬ φ›
using impI2 recovery revis_closure revis_success by fastforce
hence ‹φ .⟶. ψ ∈ K ❙* .¬ φ›
using imp_contrapos recovery revis_closure by fastforce
with b show ‹ψ ∈ Cn (K ∩ (K ❙* .¬ φ) ∪ {φ})›
by (meson Int_iff Supraclassical_logic.imp_PL Supraclassical_logic_axioms inclusion_L subsetD)
qed
next
case extensionality:(6 K A φ ψ)
hence ‹Cn({.¬ φ}) = Cn({.¬ ψ})›
using equiv_negation[of ‹{}› φ ψ] valid_Cn_equiv valid_def by auto
hence ‹(K ❙* .¬ φ) = (K ❙* .¬ ψ)›
using extensionality(1) revis_extensionality by blast
then show ?case by simp
qed
locale AGMC_S = AGM_Contraction + Supraclassical_logic
text‹The AGM revision of @{term ‹K›} by @{term ‹φ›} can be defined as the AGM contraction of @{term ‹K›} by @{text ‹¬φ›}
followed by an expansion by @{term ‹φ›}. This definition is known as Levi identity \<^cite>‹"Levi1977SubjunctivesDA"›.›
sublocale AGMC_S ⊆ AGM_Revision where revision = ‹λK φ. (K ÷ .¬ φ) ⊕ φ›
proof(unfold_locales, goal_cases)
case closure:(1 K A φ)
then show ?case
by (simp add: expansion_def idempotency_L)
next
case inclusion:(2 K A φ)
have "K ÷ .¬ φ ⊆ K ∪ {φ}"
using contract_inclusion inclusion by auto
then show ?case
by (simp add: expansion_def monotonicity_L)
next
case vacuity:(3 K A φ)
then show ?case
by (simp add: contract_vacuity expansion_def)
next
case success:(4 K A φ)
then show ?case
using assumption_L expansion_def by auto
next
case extensionality:(5 K A φ ψ)
hence ‹Cn({.¬ φ}) = Cn({.¬ ψ})›
using equiv_negation[of ‹{}› φ ψ] valid_Cn_equiv valid_def by auto
hence ‹(K ÷ .¬ φ) = (K ÷ .¬ ψ)›
using contract_extensionality extensionality(1) by blast
then show ?case
by (metis Cn_union expansion_def extensionality(2))
next
case consistency:(6 K A φ)
then show ?case
by (metis contract_closure contract_success expansion_def infer_def not_PL)
qed
text‹The relationship between AGM full revision and AGM full contraction is the same as the relation between AGM revison and AGM contraction›
sublocale AGM_FullRevision ⊆ AGM_FullContraction where contraction = ‹λK φ. K ∩ (K ❙* .¬ φ)›
proof(unfold_locales, goal_cases)
case conj_overlap:(1 K A φ ψ)
have a:‹Cn({.¬ (φ .∧. ψ)}) = Cn({(.¬ φ) .∨. (.¬ ψ)})›
using Cn_same morgan by simp
show ?case (is ?A)
using revis_superexpansion_ext[OF conj_overlap(1), of ‹.¬ φ› ‹.¬ ψ›]
revis_extensionality[OF conj_overlap(1) a] by auto
next
case conj_inclusion:(2 K A φ ψ)
have a:‹Cn({.¬ (φ .∧. ψ) .∧. .¬ φ}) = Cn({.¬ φ})›
using conj_superexpansion1 by (simp add: Cn_same)
from conj_inclusion show ?case
proof(cases ‹φ ∈ K›)
case True
hence b:‹.¬ (.¬ φ) ∉ K ❙* .¬ (φ .∧. ψ)›
using absurd_PL conj_inclusion revis_closure by fastforce
show ?thesis
using revis_subexpansion[OF conj_inclusion(1) b] revis_extensionality[OF conj_inclusion(1) a]
expansion_def inclusion_L by fastforce
next
case False
then show ?thesis
by (simp add: conj_inclusion(1) contract_vacuity)
qed
qed
locale AGMFC_S = AGM_FullContraction + AGMC_S
sublocale AGMFC_S ⊆ AGM_FullRevision where revision = ‹λK φ. (K ÷ .¬ φ) ⊕ φ›
proof(unfold_locales, safe, goal_cases)
case super:(1 K A φ ψ χ)
hence a:‹(φ .∧. ψ) .⟶. χ ∈ Cn(Cn(A) ÷ .¬ (φ .∧. ψ))›
using Supraclassical_logic.imp_PL Supraclassical_logic_axioms expansion_def by fastforce
have b:‹(φ .∧. ψ) .⟶. χ ∈ Cn({.¬ (φ .∧. ψ)})›
by (meson Supraclassical_logic.imp_recovery0 Supraclassical_logic.valid_disj_PL Supraclassical_logic_axioms)
have c:‹(φ .∧. ψ) .⟶. χ ∈ Cn(A) ÷ (.¬ (φ .∧. ψ) .∧. .¬ φ)›
using contract_conj_overlap_variant[of ‹Cn(A)› A ‹.¬ (φ .∧. ψ)› ‹.¬ φ›] a b
using AGM_Contraction.contract_closure AGM_FullContraction_axioms AGM_FullContraction_def by fastforce
have d:‹Cn({.¬ (φ .∧. ψ) .∧. .¬ φ}) = Cn({.¬ φ})›
using conj_superexpansion1 by (simp add: Cn_same)
hence e:‹(φ .∧. ψ) .⟶. χ ∈ Cn(A) ÷ .¬ φ›
using AGM_Contraction.contract_extensionality[OF _ _ d] c
AGM_FullContraction_axioms AGM_FullContraction_def by fastforce
hence f:‹φ .⟶. (ψ .⟶. χ) ∈ Cn(A) ÷ .¬ φ›
using conj_imp AGM_Contraction.contract_closure AGM_FullContraction_axioms AGM_FullContraction_def conj_imp by fastforce
then show ?case
by (metis assumption_L expansion_def imp_PL infer_def)
next
case sub:(2 K A ψ φ χ)
hence a:‹φ .⟶. (ψ .⟶. χ) ∈ Cn(A) ÷ .¬ φ›
by (metis AGMC_S.axioms(1) AGMC_S_axioms AGM_Contraction.contract_closure expansion_def impI_PL infer_def revis_closure)
have b:‹Cn({.¬ (φ .∧. ψ) .∧. .¬ φ}) = Cn({.¬ φ})›
using conj_superexpansion1 by (simp add: Cn_same)
have c:‹.¬ (φ .∧. ψ) ∉ Cn A ÷ (.¬ φ)›
using sub(1) by (metis assumption_L conj_imp expansion_def imp_PL infer_def not_PL)
have c:‹Cn(A) ÷ .¬ φ ⊆ Cn(A) ÷ (.¬ (φ .∧. ψ))›
using contract_conj_inclusion[of ‹Cn(A)› A ‹.¬ (φ .∧. ψ)› ‹.¬ φ›]
by (metis AGM_Contraction.contract_extensionality AGM_FullContraction.axioms(1) AGM_FullContraction_axioms b c)
then show ?case
by (metis a assumption_L conj_imp expansion_def imp_PL in_mono infer_def)
qed
end