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 "[A1, A2 g B]  [ A1]  [ A2]  [ B]"
abbreviation conseq_global3::σσσbool" ("[_,_,_ g _]") where "[A1, A2, A3 g B]  [ A1]  [ A2]  [ A3]  [ B]"
abbreviation conseq_local1::σbool" ("[_  _]") where "[A  B]  A  B"
abbreviation conseq_local2::σσbool" ("[_,_  _]") where "[A1, A2  B]  A1  A2  B"
abbreviation conseq_local3::σσσbool" ("[_,_,_  _]") where "[A1, A2, A3  B]  A1  A2  A3  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 fp A" using fp1 unfolding conn equal_op_def by metis
lemma "AA  A A" nitpick oops (*countermodel*)
lemma Prop2: "Cl A  AA  " using pC2 unfolding conn by auto
lemma "Cl A  BA  " nitpick oops (*countermodel*)
lemma Prop3: "Cl A  AA  " using Cl_fr_def unfolding conn by auto
lemma "Cl A  BA  " 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