Theory ex_LFUs

theory ex_LFUs
  imports topo_derivative_algebra sse_operation_negative
nitpick_params[assms=true, user_axioms=true, show_all, expect=genuine, format=3] (*default Nitpick settings*)

section ‹Example application: Logics of Formal Undeterminedness (LFUs)›
text‹\noindent{The LFUs @{cite LFU} @{cite LFI} are a family of paracomplete logics featuring a 'determinedness'
operator @{text ""} that can be used to recover some classical properties of negation (in particular TND).
LFUs behave in a sense dually to LFIs. Both can be semantically embedded as extensions of Boolean algebras.
Here we show how to semantically embed LFUs as derivative algebras.}›

text‹\noindent{(We rename (classical) meta-logical negation to avoid terminological confusion)}›
abbreviation cneg::"boolbool" ("_" [40]40) where "φ  ¬φ" 

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{As for LFIs, we focus on the local (truth-degree preserving) notion of logical consequence.}›
abbreviation conseq_local1::σbool" ("[_  _]") where "[A  B]  A  B"
abbreviation conseq_local2::σσbool" ("[_,_  _]") where "[A1, A2  B]  A1  A2  B"
abbreviation conseq_local12::σσbool" ("[_  _,_]") where "[A  B1, B2]  A  B1  B2"
(*add more as the need arises...*)

text‹\noindent{For LFUs we use the interior-based negation previously defined (taking derivative as primitive). }›
definition ineg::σ" ("¬")  where  "¬A (A)"
declare ineg_def[conn]

text‹\noindent{In terms of the derivative operator the negation looks as follows:}›
lemma ineg_prop: "¬A  (𝒟 A)  A" using Cl_der_def IB_rel Int_br_def eq_ext' pB4 conn by fastforce

text‹\noindent{This negation is of course paracomplete.}›
lemma "[ a  ¬a]" nitpick oops (*countermodel*)

text‹\noindent{We define two pairs of in/determinedness operators and show how they relate to each other.}›
abbreviation op_det::σ" ("_" [57]58) where "A  d A"
abbreviation op_ind::σ" ("_" [57]58) where "A   A"

lemma op_det_def: "a  a  ¬a" by (simp add: compl_def diff_def dual_def ineg_def join_def pB1)
lemma Prop1: "A  𝒞fp A" by (metis dimp_def eq_ext' fp3)
lemma Prop2: "Op A  A  " by (metis dual_def dual_symm pB1 pI1 top_def compl_def diff_def)
lemma Prop3: "Op A  A  " by (metis Op_Bzero dual_def dual_symm)
lemma Prop4: "Cl A  A  " by (metis Prop1 dimp_def top_def)
lemma Prop5: "Cl A  A  " by (simp add: Prop4 bottom_def compl_def top_def)

text‹\noindent{Analogously as for LFIs, LFUs provide means for recovering the principle of excluded middle.}›
lemma "[Γ  a, a  ¬a]" using IB_rel Int_br_def compl_def diff_def dual_def eq_ext' ineg_def join_def by fastforce
lemma "[Γ, a  a  ¬a]" using dual_def pB1 unfolding conn by auto

lemma "TNDm(¬)" nitpick oops (*countermodel*)
lemma "ECQ(¬)" by (simp add: ECQ_def bottom_def diff_def ineg_prop meet_def)
lemma "Der_3 𝒟  LNC(¬)" using ineg_prop ECQ_def ID3 LNC_def dNOR_def unfolding conn by auto
lemma "𝔇 𝒟  DNI(¬)" nitpick oops (*countermodel*)
lemma "𝔇 𝒟  DNE(¬)" nitpick oops (*countermodel*)
lemma "Der_1b 𝒟  CoPw(¬)" by (smt CoPw_def MONO_ADDIb PD1 compl_def ineg_def monI)
lemma "𝔇 𝒟  CoP1(¬)" nitpick oops (*countermodel*)
lemma "𝔇 𝒟  CoP2(¬)" nitpick oops (*countermodel*)
lemma "𝔇 𝒟  CoP3(¬)" nitpick oops (*countermodel*)
lemma "𝔇 𝒟  DM3(¬)" nitpick oops (*countermodel*)
lemma "Der_1a 𝒟  DM4(¬)" unfolding Defs using ADDI_a_def ineg_prop compl_def diff_def  join_def meet_def by auto
lemma "Der_3 𝒟  nNor(¬)" by (simp add: NOR_def ineg_prop nNor_def bottom_def compl_def diff_def top_def)
lemma "nDNor(¬)" by (simp add: bottom_def diff_def ineg_prop nDNor_def top_def)
lemma "Der_1b 𝒟  MT0(¬)" unfolding Defs by (metis (mono_tags, hide_lams) CD1b Disj_I OpCldual PD1 bottom_def compl_def ineg_def meet_def top_def)
lemma "Der_1b 𝒟  Der_3 𝒟  MT1(¬)" unfolding Defs by (metis (full_types) NOR_def PD1 bottom_def compl_def diff_def ineg_prop top_def)
lemma "𝔇 𝒟  MT2(¬)" nitpick oops (*countermodel*)
lemma "𝔇 𝒟  MT3(¬)" nitpick oops (*countermodel*)

text‹\noindent{We show how all local contraposition variants (lCoP) can be recovered using the determinedness 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 det_lcop1: "[a, a  b  ¬b  ¬a]" using dual_def pI1 conn by auto 
lemma "𝔇 𝒟  lCoP1()(¬)" nitpick oops (*countermodel*)
lemma det_lcop2: "[a, a  ¬b  b  ¬a]" using dual_def pI1 conn by auto
lemma "𝔇 𝒟  lCoP2()(¬)" nitpick oops (*countermodel*)
lemma det_lcop3: "[a, ¬a  b  ¬b  a]" using dual_def pI1 conn by auto
lemma "𝔇 𝒟  lCoP3()(¬)" nitpick oops (*countermodel*)
lemma det_lcop4: "[a, ¬a  ¬b  b  a]" using dual_def pI1 conn by auto

text‹\noindent{Disjunctive syllogism (DS).}›
lemma "DS1()(¬)" by (simp add: DS1_def diff_def impl_def ineg_prop join_def)
lemma "𝔇 𝒟  DS2()(¬)" nitpick oops (*countermodel*)
lemma det_ds2: "[a, ¬a  b  a  b]" using pB1 dual_def conn by auto