Theory ex_LFIs

theory ex_LFIs
  imports topo_negation_conditions
begin
nitpick_params[assms=true, user_axioms=true, show_all, expect=genuine, format=3] (*default Nitpick settings*)

section ‹Example application: Logics of Formal Inconsistency (LFIs)›
text‹\noindent{The LFIs @{cite LFI} @{cite RLFI} 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 how to semantically embed LFIs as extensions of Boolean algebras (here as frontier algebras).}›

text‹\noindent{Logical validity can be defined as truth in all worlds/points (i.e. as denoting the top element)}›
abbreviation gtrue::"σ⇒bool" ("[❙⊢ _]") where  "[❙⊢  A] ≡ ∀w. A w"   
lemma gtrue_def: "[❙⊢ A] ≡ A ❙≈ ❙⊤"  by (simp add: top_def)

text‹\noindent{When defining a logic over an existing algebra we have two choices: a global (truth preserving)
and a local (truth-degree preserving) notion of logical consequence. For LFIs we prefer the latter.}›
abbreviation conseq_global1::"σ⇒σ⇒bool" ("[_ ❙⊢⇩_g _]") where "[A ❙⊢⇩_g B] ≡ [❙⊢ A] ⟶ [❙⊢ B]"
abbreviation conseq_global2::"σ⇒σ⇒σ⇒bool" ("[_,_ ❙⊢⇩_g _]") where "[A⇩₁, A⇩₂ ❙⊢⇩_g B] ≡ [❙⊢ A⇩₁] ∧ [❙⊢ A⇩₂] ⟶ [❙⊢ B]"
abbreviation conseq_global3::"σ⇒σ⇒σ⇒σ⇒bool" ("[_,_,_ ❙⊢⇩_g _]") where "[A⇩₁, A⇩₂, A⇩₃ ❙⊢⇩_g B] ≡ [❙⊢ A⇩₁] ∧ [❙⊢ A⇩₂] ∧ [❙⊢ A⇩₃] ⟶ [❙⊢ B]"
abbreviation conseq_local1::"σ⇒σ⇒bool" ("[_ ❙⊢ _]") where "[A ❙⊢ B] ≡ A ❙≼ B"
abbreviation conseq_local2::"σ⇒σ⇒σ⇒bool" ("[_,_ ❙⊢ _]") where "[A⇩₁, A⇩₂ ❙⊢ B] ≡ A⇩₁ ❙∧ A⇩₂ ❙≼ B"
abbreviation conseq_local3::"σ⇒σ⇒σ⇒σ⇒bool" ("[_,_,_ ❙⊢ _]") where "[A⇩₁, A⇩₂, A⇩₃ ❙⊢ B] ≡ A⇩₁ ❙∧ A⇩₂ ❙∧ A⇩₃ ❙≼ B"
(*add more as the need arises...*)

text‹\noindent{For LFIs we use the (paraconsistent) closure-based negation previously defined (taking frontier as primitive). }›
abbreviation cneg::"σ⇒σ" ("❙¬") where "❙¬A ≡ ❙¬⇧^CA"

text‹\noindent{In terms of the frontier operator the negation looks as follows:}›
lemma "❙¬A ❙≈ ❙─A ❙∨ ℱ(❙─A)" by (simp add: neg_C_def pC2)
lemma cneg_prop: "Fr_2 ℱ ⟹ ❙¬A ❙≈ ❙─A ❙∨ ℱ(A)" using pC2 pF2 unfolding conn by blast

text‹\noindent{This negation is of course boldly paraconsistent.}›
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‹\noindent{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' (cf. @{cite RLFI}).}›
abbreviation op_inc_a::"σ⇒σ" ("∙⇧^A_" [57]58) where "∙⇧^AA ≡ A ❙∧ ❙¬A"
abbreviation op_con_a::"σ⇒σ" ("❙∘⇧^A_" [57]58) where "❙∘⇧^AA ≡ ❙─∙⇧^AA"
abbreviation op_inc_b::"σ⇒σ" ("∙⇧^B_" [57]58) where "∙⇧^BA ≡ ℬ A"
abbreviation op_con_b::"σ⇒σ" ("❙∘⇧^B_" [57]58) where "❙∘⇧^BA ≡ ℬ⇧^c A"

text‹\noindent{Observe that assumming condition Fr-2 are we allowed to exchange A and B variants.}›
lemma pincAB: "Fr_2 ℱ ⟹ ∙⇧^AA ❙≈ ∙⇧^BA" using Br_fr_def Cl_fr_def pF2 conn by auto
lemma pconAB: "Fr_2 ℱ ⟹ ❙∘⇧^AA ❙≈ ❙∘⇧^BA" using pincAB unfolding conn by simp

text‹\noindent{Variants A and B give us slightly different properties.}›
lemma Prop1: "❙∘⇧^BA ❙≈ ℐ⇧^f⇧^p A" using fp1 unfolding conn equal_op_def by metis
lemma "❙∘⇧^AA ❙≈ A ❙→ ℐ A" nitpick oops (*countermodel*)
lemma Prop2: "Cl A ⟷ ❙∘⇧^A❙─A ❙≈ ❙⊤" using pC2 unfolding conn by auto
lemma "Cl A ⟶ ❙∘⇧^B❙─A ❙≈ ❙⊤" nitpick oops (*countermodel*)
lemma Prop3: "Cl A ⟷ ∙⇧^A❙─A ❙≈ ❙⊥" using Cl_fr_def unfolding conn by auto
lemma "Cl A ⟶ ∙⇧^B❙─A ❙≈ ❙⊥" nitpick oops (*countermodel*)
lemma Prop4: "Op A ⟷ ❙∘⇧^BA ❙≈ ❙⊤" using Op_Bzero unfolding conn by simp
lemma "Op A ⟶ ❙∘⇧^AA ❙≈ ❙⊤" nitpick oops (*countermodel*)
lemma Prop5: "Op A ⟷ ∙⇧^BA ❙≈ ❙⊥" using Op_Bzero by simp
lemma "Op A ⟶ ∙⇧^AA ❙≈ ❙⊥" nitpick oops (*countermodel*)

text‹\noindent{Importantly, LFIs must satisfy the so-called 'principle of gentle explosion'. Only variant A works here:}›
lemma "[❙∘⇧^Aa, a, ❙¬a ❙⊢ b]" using compl_def meet_def by auto
lemma "[❙∘⇧^Aa, a, ❙¬a ❙⊢⇩_g b]" using compl_def meet_def by auto
lemma "[❙∘⇧^Ba, a, ❙¬a ❙⊢ b]" nitpick oops (*countermodel*)
lemma "[❙∘⇧^Ba, a, ❙¬a ❙⊢⇩_g b]" nitpick oops (*countermodel*)

text‹\noindent{In what follows we employ the (minimal) A-variant and verify some properties.}›
abbreviation op_inc :: "σ⇒σ" ("∙_" [57]58) where "∙A  ≡ ∙⇧^AA"
abbreviation op_con :: "σ⇒σ" ("❙∘_" [57]58) where "❙∘A  ≡ ❙─∙A"

lemma "TND(❙¬)" by (simp add: TND_C)
lemma "ECQm(❙¬)" nitpick oops (*countermodel*)
lemma "Fr_1b ℱ ⟹ Fr_2 ℱ ⟹ LNC(❙¬)" by (simp add: LNC_C PF6)
lemma "𝔉 ℱ ⟹ DNI(❙¬)" nitpick oops (*countermodel*)
lemma "𝔉 ℱ ⟹ DNE(❙¬)" nitpick oops (*countermodel*)
lemma "Fr_1b ℱ ⟹ Fr_2 ℱ ⟹ CoPw(❙¬)" by (simp add: CoPw_C PF6)
lemma "𝔉 ℱ ⟹ CoP1(❙¬)" nitpick oops (*countermodel*)
lemma "𝔉 ℱ ⟹ CoP2(❙¬)" nitpick oops (*countermodel*)
lemma "𝔉 ℱ ⟹ CoP3(❙¬)" nitpick oops (*countermodel*)
lemma "Fr_1a ℱ ⟹ Fr_2 ℱ ⟹ DM3(❙¬)" by (simp add: DM3_C)
lemma "𝔉 ℱ ⟹ DM4(❙¬)" nitpick oops (*countermodel*)
lemma "nNor(❙¬)" by (simp add: nNor_C)
lemma "Fr_3 ℱ ⟹ nDNor(❙¬)" by (simp add: nDNor_C)
lemma "Fr_1b ℱ ⟹ Fr_2 ℱ ⟹ MT0(❙¬)" by (simp add: MT0_C PF6)
lemma "Fr_1b ℱ ⟹ Fr_2 ℱ ⟹ MT1(❙¬)" by (simp add: MT1_C PF6)
lemma "𝔉 ℱ ⟹ MT2(❙¬)" nitpick oops (*countermodel*)
lemma "Fr_1b ℱ ⟹ Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ MT3(❙¬)" using MT3_C by auto

text‹\noindent{We show how all local contraposition variants (lCoP) can be recovered using the consistency operator.
Observe that we can recover in the same way other (weaker) properties: CoP, MT and DNI/DNE (local \& global).}›
lemma "𝔉 ℱ ⟹ lCoPw(❙→)(❙¬)" nitpick oops (*countermodel*)
lemma cons_lcop1: "[❙∘b, a ❙→ b ❙⊢ ❙¬b ❙→ ❙¬a]" using Cl_fr_def conn by auto
lemma "𝔉 ℱ ⟹ lCoP1(❙→)(❙¬)" nitpick oops (*countermodel*)
lemma cons_lcop2: "[❙∘b, a ❙→ ❙¬b ❙⊢ b ❙→ ❙¬a]" using Cl_fr_def conn by auto
lemma "𝔉 ℱ ⟹ lCoP2(❙→)(❙¬)" nitpick oops (*countermodel*)
lemma cons_lcop3: "[❙∘b, ❙¬a ❙→ b ❙⊢ ❙¬b ❙→ a]" using Cl_fr_def conn by auto
lemma "𝔉 ℱ ⟹ lCoP3(❙→)(❙¬)" nitpick oops (*countermodel*)
lemma cons_lcop4: "[❙∘b, ❙¬a ❙→ ❙¬b ❙⊢ b ❙→ a]" using Cl_fr_def conn by auto
text‹\noindent{Disjunctive syllogism (DS).}›
lemma "𝔉 ℱ ⟹ DS1(❙→)(❙¬)" nitpick oops (*countermodel*)
lemma cons_ds1: "[❙∘a, a ❙∨ b ❙⊢ ❙¬a ❙→ b]" using conn by auto
lemma "DS2(❙→)(❙¬)" by (metis Cl_fr_def DS2_def compl_def impl_def join_def neg_C_def)
text‹\noindent{Further properties.}›
lemma "[a ❙∧ ❙¬a ❙⊢ ❙¬(❙∘a)]" by (simp add: pC2 conn)
lemma "𝔉 ℱ ⟹ [❙¬(❙∘a) ❙⊢ a ❙∧ ❙¬a]" nitpick oops (* countermodel found *)
lemma "[❙∘a ❙⊢ ❙¬(a ❙∧ ❙¬a)]" by (simp add: pC2 conn)
lemma "𝔉 ℱ ⟹ [❙¬(a ❙∧ ❙¬a) ❙⊢ ❙∘a]" nitpick oops (* countermodel found *)

text‹\noindent{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 ≡ DNE(❙¬)"
abbreviation ce where "ce ≡ DNI(❙¬)"
abbreviation ciw where "ciw ≡ ∀P. [❙⊢ ❙∘P ❙∨ ∙P]"
abbreviation ci  where  "ci ≡ ∀P.  [❙¬(❙∘P) ❙⊢ ∙P]"
abbreviation cl  where  "cl ≡ ∀P.  [❙¬(∙P) ❙⊢ ❙∘P]"
abbreviation ca_conj where "ca_conj ≡ ∀P Q. [❙∘P,❙∘Q ❙⊢ ❙∘(P ❙∧ Q)]"
abbreviation ca_disj where "ca_disj ≡ ∀P Q. [❙∘P,❙∘Q ❙⊢ ❙∘(P ❙∨ Q)]"
abbreviation ca_impl where "ca_impl ≡ ∀P Q. [❙∘P,❙∘Q ❙⊢ ❙∘(P ❙→ Q)]"
abbreviation ca where "ca ≡ ca_conj ∧ ca_disj ∧ ca_impl"

text‹\noindent{cf}›
lemma "𝔉 ℱ ⟹ cf" nitpick oops
lemma "𝔉 ℱ ∧ cf ∧ ∼ECQm(❙¬)" nitpick[satisfy] oops (*model found*)
text‹\noindent{ce}›
lemma "𝔉 ℱ ⟹ ce" nitpick oops
lemma "Fr_1 ℱ ∧ Fr_2 ℱ ∧ Fr_4 ℱ ∧ ce ∧ ∼ECQ(❙¬)" nitpick[satisfy] oops (*model found*)  
lemma "Fr_1 ℱ ∧ Fr_3 ℱ ∧ Fr_4 ℱ ∧ ce ∧ ∼ECQm(❙¬)" nitpick[satisfy] oops (*model found*)  
lemma "Fr_1a ℱ ∧ Fr_2 ℱ ∧ Fr_3 ℱ ∧ Fr_4 ℱ ∧ ce ∧ ∼ECQm(❙¬)" nitpick[satisfy] oops (*model found*)  
lemma "Fr_1b ℱ ⟹ Fr_2 ℱ ⟹ ce ⟶ ECQm(❙¬)" unfolding Defs  using CoP1_XCoP CoP1_def2 CoPw_C DNI_def ECQw_def PF6 XCoP_def2 by auto
text‹\noindent{ciw}›
lemma ciw by (simp add:conn)
text‹\noindent{ci}›
lemma "𝔉 ℱ ⟹ ci" nitpick oops
lemma "𝔉 ℱ ∧ ci ∧ ∼ECQm(❙¬)" nitpick[satisfy] oops (*model found*)
text‹\noindent{cl}›
lemma "𝔉 ℱ ⟹ cl" nitpick oops
lemma "Fr_1 ℱ ∧ Fr_3 ℱ ∧ Fr_4 ℱ ∧ cl ∧ ∼ECQm(❙¬)" nitpick[satisfy] oops (*model found*) 
lemma "Fr_1a ℱ ∧ Fr_2 ℱ ∧ Fr_3 ℱ ∧ Fr_4 ℱ ∧ cl ∧ ∼ECQm(❙¬)" nitpick[satisfy] oops (*model found*)
lemma "Fr_1b ℱ ⟹ Fr_2 ℱ ⟹ cl ⟶ ECQ(❙¬)" unfolding Defs  by (metis BC_rel Br_Border Br_cl_def bottom_def compl_def eq_ext' meet_def neg_C_def) 
text‹\noindent{ca-conj/disj}›
lemma "Fr_1a ℱ ⟹ Fr_2 ℱ ⟹ ca_conj" using DM3_C DM3_def conn by auto
lemma "Fr_1b ℱ ⟹ Fr_2 ℱ ⟹ ca_disj" using ADDI_b_def MONO_ADDIb monI pB1 pincAB unfolding conn by metis
lemma "𝔉 ℱ ⟹ ca_impl" nitpick oops
text‹\noindent{ca-impl}›
lemma "ca_impl ∧ ∼ECQ(❙¬)" (*nitpick[satisfy]*) oops (*cannot find finite model*)
lemma "ca_impl ⟶ ECQm(❙¬)" oops (*nor proof yet*)
text‹\noindent{cf \& ci}›
lemma "Fr_1 ℱ ∧ Fr_3 ℱ ∧ Fr_4 ℱ ∧ cf ∧ ci ∧ ∼ECQm(❙¬)" nitpick[satisfy] oops (*model found*)  
lemma "Fr_2 ℱ ∧ Fr_3 ℱ ∧ Fr_4 ℱ ∧ cf ∧ ci ∧ ∼ECQm(❙¬)" nitpick[satisfy] oops (*model found*)
lemma "Fr_1b ℱ ∧ Fr_2 ℱ ∧ cf ∧ ci ∧ ∼ECQ(❙¬)" (*nitpick[satisfy]*) oops (*cannot find finite model*) 
lemma "𝔉 ℱ ∧ cf ∧ ci ⟶ ECQm(❙¬)" oops (*nor proof yet*) 
text‹\noindent{cf \& cl}›
lemma "Fr_1 ℱ ∧ Fr_3 ℱ ∧ Fr_4 ℱ ∧ cf ∧ cl ∧ ∼ECQm(❙¬)" nitpick[satisfy] oops (*model found*) 
lemma "Fr_2 ℱ ∧ Fr_3 ℱ ∧ Fr_4 ℱ ∧ cf ∧ cl ∧ ∼ECQm(❙¬)" nitpick[satisfy] oops (*model found*)
lemma "Fr_1b ℱ ∧ Fr_2 ℱ ∧ cf ∧ cl ⟶ ECQ(❙¬)" unfolding Defs by (smt Br_fr_def Fr_1b_def Prop2 Prop3 pF3 cneg_prop conn) 

end