Theory logics_LFI

theory logics_LFI
  imports logics_consequence conditions_relativized_infinitary
begin

subsection ‹Logics of Formal Inconsistency (LFIs)›

text‹The LFIs are a family of paraconsistent logics featuring a 'consistency' operator @{text "∘"}
that can be used to recover some classical properties of negation (in particular ECQ).
We show a shallow semantical embedding of a family of self-extensional LFIs using the border operator
as primitive.›

text‹Let us assume a concrete type w (for 'worlds' or 'points').›
typedecl w
text‹Let us assume the following primitive unary operation intended as a border operator.›
consts ℬ::"w σ ⇒ w σ"

text‹From the topological cube of opposition we have that:›
abbreviation "𝒞 ≡ (ℬfp)d-" 
abbreviation "ℐ ≡ ℬfp-" 
lemma "𝒞d- = ℬfp" by (simp add: dualcompl_invol)

text‹Let us recall that:›
lemma expn_cntr: "EXPN 𝒞 = CNTR ℬ" by (metis EXPN_CNTR_dual2 EXPN_fp ofp_comm_dc1)

text‹For LFIs we use the negation previously defined as @{text "𝒞d- = ℬfp"}.›
abbreviation neg (‹¬_›[70]71) where "neg ≡ ℬfp"

text‹In terms of the border operator the negation looks as follows (under appropriate assumptions):›
lemma neg_char: "CNTR ℬ ⟹ ¬A = (─A ∨ ℬ A)" unfolding conn by (metis CNTR_def dimpl_def op_fixpoint_def subset_def)

text‹This negation is of course boldly paraconsistent (for both local and global consequence).›
lemma "[a, ¬a ⊢ b]" nitpick oops ―‹ countermodel ›
lemma "[a, ¬a ⊢ ¬b]" nitpick oops ―‹ countermodel ›
lemma "[a, ¬a ⊢g b]" nitpick oops ―‹ countermodel › 
lemma "[a, ¬a ⊢g ¬b]" nitpick oops ―‹ countermodel ›

text‹We define two pairs of in/consistency operators and show how they relate to each other.
Using LFIs terminology, the minimal logic so encoded corresponds to RmbC + 'ciw' axiom.›
abbreviation op_inc_a::"w σ ⇒ w σ" (‹∙A_› [57]58) (* ∙ as truth-glut *)
  where "∙AA ≡ A ∧ ¬A"
abbreviation op_con_a::"w σ ⇒ w σ" (‹∘A_› [57]58) 
  where "∘AA ≡ ─∙AA"
abbreviation op_inc_b::"w σ ⇒ w σ" (‹∙B_› [57]58) (* ∙ as border *)
  where "∙BA ≡ ℬ A"
abbreviation op_con_b::"w σ ⇒ w σ" (‹∘B_› [57]58) 
  where "∘BA ≡ ℬ- A"

text‹Observe that assumming CNTR for border we are allowed to exchange A and B variants.›
lemma pincAB: "CNTR ℬ ⟹ ∙AA = ∙BA" using neg_char by (metis CNTR_def CNTR_fpc L5 L6 L9 dimpl_char impl_char ofp_invol op_fixpoint_def setequ_ext svfun_compl_def)
lemma pconAB: "CNTR ℬ ⟹ ∘AA = ∘BA" by (metis pincAB setequ_ext svfun_compl_def) 

text‹Variants A and B give us slightly different properties (there are countermodels for those not shown).›
lemma Prop1: "∘BA = ℐfp A" by (simp add: ofp_comm_compl ofp_invol)
lemma Prop2: "∘AA = (A → ℐ A)" by (simp add: compl_def impl_def meet_def svfun_compl_def)
lemma Prop3: "fp 𝒞 A ⟷ [⊢ ∘B─A]" by (simp add: fp_rel gtrue_def ofp_comm_dc2 ofp_invol op_dual_def svfun_compl_def)
lemma Prop4a: "fp ℐ A ⟷ [⊢ ∘BA]" by (simp add: fp_rel gtrue_def ofp_comm_compl ofp_invol)
lemma Prop4b: "fp ℐ A  ⟶ [⊢ ∘AA]" by (simp add: Prop2 fixpoints_def impl_def setequ_ext)

text‹The 'principle of gentle explosion' works for both variants (both locally and globally).›
lemma "[∘Aa, a, ¬a ⊢ b]" by (metis (mono_tags, lifting) compl_def meet_def subset_def)
lemma "[∘Aa, a, ¬a ⊢g b]" by (metis compl_def meet_def)
lemma "[∘Ba, a, ¬a ⊢ b]" by (smt (z3) meet_def ofp_fixpoint_compl_def ofp_invol sdiff_def subset_def)
lemma "[∘Ba, a, ¬a ⊢g b]" by (metis compl_def fixpoints_def fp_rel gtrue_def setequ_ext svfun_compl_def)

abbreviation "BORDER φ ≡ nMULTr φ ∧ CNTR φ ∧ nDNRM φ ∧ nIDEMrb φ"

text‹We show how (local) contraposition variants (among others) can be recovered using the
 consistency operators.›
lemma "[∘Ab, a → b ⊢ ¬b → ¬a]" nitpick oops ―‹ countermodel ›
lemma cons_lcop0_A: "CNTR ℬ ⟶ [∘Ab,  a → b ⊢ ¬b → ¬a]" by (smt (verit, del_insts) neg_char compl_def impl_char join_def meet_def subset_def)
lemma "[∘Bb, a → b ⊢ ¬b → ¬a]" nitpick oops ―‹ countermodel ›
lemma cons_lcop0_B: "CNTR ℬ ⟶ [∘Bb,  a → b ⊢ ¬b → ¬a]" by (metis cons_lcop0_A pconAB)
lemma "[∘Ab, a → ¬b ⊢ b → ¬a]" nitpick oops ―‹ countermodel ›
lemma cons_lcop1_A: "CNTR ℬ ⟶ [∘Ab, a → ¬b ⊢  b → ¬a]" by (smt (verit, del_insts) neg_char compl_def impl_char join_def meet_def subset_def)
lemma "[∘Bb, a → ¬b ⊢ b → ¬a]" nitpick oops ―‹ countermodel ›
lemma cons_lcop1_B: "CNTR ℬ ⟶ [∘Bb, a → ¬b ⊢  b → ¬a]" by (metis cons_lcop1_A pconAB)
lemma "[∘Ab, ¬a → b ⊢ ¬b → a]" nitpick oops ―‹ countermodel ›
lemma cons_lcop2_A: "CNTR ℬ ⟶ [∘Ab, ¬a → b ⊢ ¬b → a]" by (smt (verit, del_insts) neg_char compl_def impl_char join_def meet_def subset_def)
lemma "[∘Bb, ¬a → b ⊢ ¬b → a]" nitpick oops ―‹ countermodel ›
lemma cons_lcop2_B: "CNTR ℬ ⟶ [∘Bb, ¬a → b ⊢ ¬b → a]" by (metis cons_lcop2_A pconAB)

text‹The following axioms are commonly employed in the literature on LFIs to obtain stronger logics.
We explore under which conditions they can be assumed while keeping the logic boldly paraconsistent.›
abbreviation cf where "cf ≡ ∀P. [¬¬P ⊢ P]"
abbreviation ce where "ce ≡ ∀P. [P ⊢ ¬¬P]"
abbreviation ciw_a where "ciw_a ≡ ∀P. [⊢ ∘AP ∨ ∙AP]"
abbreviation ciw_b where "ciw_b ≡ ∀P. [⊢ ∘BP ∨ ∙BP]"
abbreviation ci_a  where  "ci_a ≡ ∀P. [¬(∘AP) ⊢ ∙AP]"
abbreviation ci_b  where  "ci_b ≡ ∀P. [¬(∘BP) ⊢ ∙BP]"
abbreviation cl_a  where  "cl_a ≡ ∀P.  [¬(∙AP) ⊢ ∘AP]"
abbreviation cl_b  where  "cl_b ≡ ∀P.  [¬(∙BP) ⊢ ∘BP]"
abbreviation ca_conj_a where "ca_conj_a ≡ ∀P Q. [∘AP,∘AQ ⊢ ∘A(P ∧ Q)]"
abbreviation ca_conj_b where "ca_conj_b ≡ ∀P Q. [∘BP,∘BQ ⊢ ∘B(P ∧ Q)]"
abbreviation ca_disj_a where "ca_disj_a ≡ ∀P Q. [∘AP,∘AQ ⊢ ∘A(P ∨ Q)]"
abbreviation ca_disj_b where "ca_disj_b ≡ ∀P Q. [∘BP,∘BQ ⊢ ∘B(P ∨ Q)]"
abbreviation ca_impl_a where "ca_impl_a ≡ ∀P Q. [∘AP,∘AQ ⊢ ∘A(P → Q)]"
abbreviation ca_impl_b where "ca_impl_b ≡ ∀P Q. [∘BP,∘BQ ⊢ ∘B(P → Q)]"
abbreviation ca_a where "ca_a ≡ ca_conj_a ∧ ca_disj_a ∧ ca_impl_a"
abbreviation ca_b where "ca_b ≡ ca_conj_b ∧ ca_disj_b ∧ ca_impl_b"

text‹cf›
lemma "BORDER ℬ ⟹ cf" nitpick oops ―‹ countermodel ›

text‹ce›
lemma "BORDER ℬ ⟹ ce" nitpick oops ―‹ countermodel ›

text‹ciw›
lemma prop_ciw_a: "ciw_a" by (simp add: conn)
lemma prop_ciw_b: "ciw_b" by (simp add: conn svfun_compl_def)

text‹ci›
lemma "BORDER ℬ ⟹ ci_a" nitpick oops ―‹ countermodel ›
lemma "BORDER ℬ ⟹ ci_b" nitpick oops ―‹ countermodel ›

text‹cl›
lemma "BORDER ℬ ⟹ cl_a" nitpick oops ―‹ countermodel ›
lemma "BORDER ℬ ⟹ cl_b" nitpick oops ―‹ countermodel ›

text‹ca-conj›
lemma prop_ca_conj_b: "nMULTb ℬ = ca_conj_b" by (metis MULT_b_def nMULTb_compl sfun_compl_invol)
lemma prop_ca_conj_a: "nMULTrb ℬ = ca_conj_a" unfolding cond op_fixpoint_def by (smt (z3) compl_def dimpl_def join_def meet_def op_fixpoint_def subset_def subset_in_def)

text‹ca-disj›
lemma prop_ca_disj_b: "ADDIa ℬ = ca_disj_b" by (simp add: nADDI_a_def nADDIa_compl)
lemma prop_ca_disj_a: "nMULTra ℬ = ca_disj_a" oops (*TODO*)

text‹ca-impl›
lemma "BORDER ℬ ⟹ ca_impl_a" nitpick oops ―‹ countermodel ›
lemma "BORDER ℬ ⟹ ca_impl_b" nitpick oops ―‹ countermodel ›

end