Theory AGM_Remainder
theory AGM_Remainder
imports AGM_Logic
begin
section ‹Remainders›
text‹In AGM, one important feature is to eliminate some proposition from a set of propositions by ensuring
that the set of retained clauses is maximal and that nothing among these clauses allows to retrieve the eliminated proposition›
subsection ‹Remainders in a Tarskian logic›
text ‹In a general context of a Tarskian logic, we consider a descriptive definition (by comprehension)›
context Tarskian_logic
begin
definition remainder::‹'a set ⇒ 'a ⇒ 'a set set› (infix ‹.⊥.› 55)
where rem: ‹A .⊥. φ ≡ {B. B ⊆ A ∧ ¬ B ⊢ φ ∧ (∀B'⊆ A. B ⊂ B' ⟶ B' ⊢ φ)}›
lemma rem_inclusion: ‹B ∈ A .⊥. φ ⟹ B ⊆ A›
by (auto simp add:rem split:if_splits)
lemma rem_closure: "K = Cn(A) ⟹ B ∈ K .⊥. φ ⟹ B = Cn(B)"
apply(cases ‹K .⊥. φ = {}›, simp)
by (simp add:rem infer_def) (metis idempotency_L inclusion_L monotonicity_L psubsetI)
lemma remainder_extensionality: ‹Cn({φ}) = Cn({ψ}) ⟹ A .⊥. φ = A .⊥. ψ›
unfolding rem infer_def apply safe
by (simp_all add: Cn_same) blast+
lemma nonconsequence_remainder: ‹A .⊥. φ = {A} ⟷ ¬ A ⊢ φ›
unfolding rem by auto
lemma taut2emptyrem: ‹⊩ φ ⟹ A .⊥. φ = {}›
unfolding rem by (simp add: infer_def validD_L)
end
subsection ‹Remainders in a supraclassical logic›
text‹In case of a supraclassical logic, remainders get impressive properties›
context Supraclassical_logic
begin
lemma remainder_recovery: ‹K = Cn(A) ⟹ K ⊢ ψ ⟹ B ∈ K .⊥. φ ⟹ B ⊢ φ .⟶. ψ›
proof -
{ fix ψ and B
assume a:‹K = Cn(A)› and c:‹ψ ∈ K› and d:‹B ∈ K .⊥. φ› and e:‹φ .⟶. ψ ∉ Cn(B)›
with a have f:‹φ .⟶. ψ ∈ K› using impI2 infer_def by blast
with d e have ‹φ ∈ Cn(B ∪ {φ .⟶. ψ})›
apply (simp add:rem, elim conjE)
by (metis dual_order.order_iff_strict inclusion_L insert_subset)
with d have False using rem imp_recovery1
by (metis (no_types, lifting) CollectD infer_def)
}
thus ‹K = Cn(A) ⟹ K ⊢ ψ ⟹ B ∈ K .⊥. φ ⟹ B ⊢ φ .⟶. ψ›
using idempotency_L by auto
qed
lemma remainder_recovery_bis: ‹K = Cn(A) ⟹ K ⊢ ψ ⟹ ¬ B ⊢ ψ ⟹ B ∈ K .⊥. φ ⟹ B ∈ K .⊥. ψ›
proof-
assume a:‹K = Cn(A)› and b:‹¬ B ⊢ ψ› and c:‹B ∈ K .⊥. φ› and d:‹K ⊢ ψ›
hence d:‹B ⊢ φ .⟶. ψ› using remainder_recovery by simp
with c show ‹B ∈ K .⊥. ψ›
by (simp add:rem) (meson b dual_order.trans infer_def insert_subset monotonicity_L mp_PL order_refl psubset_imp_subset)
qed
corollary remainder_recovery_imp: ‹K = Cn(A) ⟹ K ⊢ ψ ⟹ ⊩ (ψ .⟶. φ) ⟹ B ∈ K .⊥. φ ⟹ B ∈ K .⊥. ψ›
apply(rule remainder_recovery_bis, simp_all)
by (simp add:rem) (meson infer_def mp_PL validD_L)
lemma remainder_expansion: ‹K = Cn(A) ⟹ K ⊢ ψ ⟹ ¬ B ⊢ ψ ⟹ B ∈ K .⊥. φ ⟹ B ⊕ ψ = K›
proof
assume a:‹K = Cn(A)› and b:‹K ⊢ ψ› and c:‹¬ B ⊢ ψ› and d:‹B ∈ K .⊥. φ›
then show ‹B ⊕ ψ ⊆ K›
by (metis Un_insert_right expansion_def idempotency_L infer_def insert_subset
monotonicity_L rem_inclusion sup_bot.right_neutral)
next
assume a:‹K = Cn(A)› and b:‹K ⊢ ψ› and c:‹¬ B ⊢ ψ› and d:‹B ∈ K .⊥. φ›
{ fix χ
assume ‹χ ∈ K›
hence e:‹B ⊢ φ .⟶.χ› using remainder_recovery[OF a _ d, of χ] assumption_L by blast
have ‹ψ ∈ K› using a b idempotency_L infer_def by blast
hence f:‹B ∪ {ψ} ⊢ φ› using b c d apply(simp add:rem)
by (meson inclusion_L insert_iff insert_subsetI less_le_not_le subset_iff)
from e f have ‹B ∪ {ψ} ⊢ χ› using imp_PL imp_trans by blast
}
then show ‹K ⊆ B ⊕ ψ›
by (simp add: expansion_def subsetI)
qed
text‹To eliminate a conjunction, we only need to remove one side›
lemma remainder_conj: ‹K = Cn(A) ⟹ K ⊢ φ .∧. ψ ⟹ K .⊥. (φ .∧. ψ) = (K .⊥. φ) ∪ (K .⊥. ψ)›
apply(intro subset_antisym Un_least subsetI, simp add:rem)
apply (meson conj_PL infer_def)
using remainder_recovery_imp[of K A ‹φ .∧. ψ› φ]
apply (meson assumption_L conjE1_PL singletonI subsetI valid_imp_PL)
using remainder_recovery_imp[of K A ‹φ .∧. ψ› ψ]
by (meson assumption_L conjE2_PL singletonI subsetI valid_imp_PL)
end
subsection ‹Remainders in a compact logic›
text‹In case of a supraclassical logic, remainders get impressive properties›
context Compact_logic
begin
text ‹The following lemma is the Lindembaum's lemma requiring the Zorn's lemma (already available in standard Isabelle/HOL).
For more details, please refer to the book "Theory of logical calculi" \<^cite>‹wojcicki2013theory›.
This very important lemma states that we can get a maximal set (remainder ‹B'›) starting from any set
‹B› if this latter does not infer the proposition ‹φ› we want to eliminate›
lemma upper_remainder: ‹B ⊆ A ⟹ ¬ B ⊢ φ ⟹ ∃B'. B ⊆ B' ∧ B' ∈ A .⊥. φ›
proof -
assume a:‹B ⊆ A› and b:‹¬ B ⊢ φ›
have c:‹¬ ⊩ φ›
using b infer_def validD_L by blast
define ℬ where "ℬ ≡ {B'. B ⊆ B' ∧ B' ⊆ A ∧ ¬ B' ⊢ φ}"
have d:‹subset.chain ℬ C ⟹ subset.chain {B. ¬ B ⊢ φ} C› for C
unfolding ℬ_def
by (simp add: le_fun_def less_eq_set_def subset_chain_def)
have e:‹C ≠ {} ⟹ subset.chain ℬ C ⟹ B ⊆ ⋃ C› for C
by (metis (no_types, lifting) ℬ_def subset_chain_def less_eq_Sup mem_Collect_eq subset_iff)
{ fix C
assume f:‹C ≠ {}› and g:‹subset.chain ℬ C›
have ‹⋃ C ∈ ℬ›
using ℬ_def e[OF f g] chain_closure[OF c d[OF g]]
by simp (metis (no_types, lifting) CollectD Sup_least Sup_subset_mono g subset.chain_def subset_trans)
} note f=this
have ‹subset.chain ℬ C ⟹ ∃U∈ℬ. ∀X∈C. X ⊆ U› for C
apply (cases ‹C ≠ {}›)
apply (meson Union_upper f)
using ℬ_def a b by blast
with subset_Zorn[OF this, simplified] obtain B' where f:‹B'∈ ℬ ∧ (∀X∈ℬ. B' ⊆ X ⟶ X = B')› by auto
then show ?thesis
by (simp add:rem ℬ_def, rule_tac x=B' in exI) (metis psubsetE subset_trans)
qed
corollary emptyrem2taut: ‹A .⊥. φ = {} ⟹ ⊩ φ›
by (metis bot.extremum empty_iff upper_remainder valid_def)
end
end