# 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⇩1, A⇩2 ❙⊢⇩g B] ≡ [❙⊢ A⇩1] ∧ [❙⊢ A⇩2] ⟶ [❙⊢ B]"
abbreviation conseq_global3::"σ⇒σ⇒σ⇒σ⇒bool" ("[_,_,_ ❙⊢⇩g _]") where "[A⇩1, A⇩2, A⇩3 ❙⊢⇩g B] ≡ [❙⊢ A⇩1] ∧ [❙⊢ A⇩2] ∧ [❙⊢ A⇩3] ⟶ [❙⊢ B]"
abbreviation conseq_local1::"σ⇒σ⇒bool" ("[_ ❙⊢ _]") where "[A ❙⊢ B] ≡ A ❙≼ B"
abbreviation conseq_local2::"σ⇒σ⇒σ⇒bool" ("[_,_ ❙⊢ _]") where "[A⇩1, A⇩2 ❙⊢ B] ≡ A⇩1 ❙∧ A⇩2 ❙≼ B"
abbreviation conseq_local3::"σ⇒σ⇒σ⇒σ⇒bool" ("[_,_,_ ❙⊢ _]") where "[A⇩1, A⇩2, A⇩3 ❙⊢ B] ≡ A⇩1 ❙∧ A⇩2 ❙∧ A⇩3 ❙≼ 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}›
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