Theory logics_LFU

theory logics_LFU
  imports logics_consequence conditions_relativized_infinitary
begin

subsection ‹Logics of Formal Undeterminedness (LFUs)›

text‹The LFUs 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.
We show a shallow semantical embedding of a family of self-extensional LFUs using the closure operator
as primitive.›

(*Let us assume a concrete type w (for 'worlds' or 'points').*)
typedecl w
(*Let us assume the following primitive unary operation intended as a closure operator.*)
consts 𝒞::"w σ ⇒ w σ"

(*From the topological cube of opposition:*)
abbreviation "ℐ ≡ 𝒞⇧d" 
abbreviation "ℬ ≡ (𝒞⇧f⇧p)⇧d" 

(*let us recall that: *)
lemma "EXPN 𝒞 = CNTR ℬ" using EXPN_CNTR_dual1 EXPN_fp by blast
lemma "EXPN 𝒞 = CNTR ℐ" by (simp add: EXPN_CNTR_dual1)

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

text‹In terms of the border operator the negation looks as follows:›
lemma neg_char: "EXPN 𝒞 ⟹ ❙¬A = (❙─A ❙∧ ℬ⇧d A)" unfolding conn by (metis EXPN_def compl_def dimpl_def dual_invol op_fixpoint_def subset_def svfun_compl_def)

abbreviation "CLOSURE φ ≡ ADDI φ ∧ EXPN φ ∧ NORM φ ∧ IDEM φ"

text‹This negation is of course paracomplete.›
lemma "CLOSURE 𝒞 ⟹ [⊢ a ❙∨ ❙¬a]" nitpick oops ―‹ countermodel ›

text‹We define two pairs of un/determinedness operators and show how they relate to each other.
This logic corresponds to the paracomplete dual of the LFI 'RmbC-ciw'.›
abbreviation op_det_a::"w σ ⇒ w σ" ("¤⇧A_" [57]58) 
  where "¤⇧AA ≡ A ❙∨ ❙¬A"
abbreviation op_und_a::"w σ ⇒ w σ" ("⋆⇧A_" [57]58) (* ⋆ as truth-gap *)
  where "⋆⇧AA ≡ ❙─¤⇧AA"
abbreviation op_det_b::"w σ ⇒ w σ" ("¤⇧B_" [57]58) 
  where "¤⇧BA ≡ ℬ⇧d A"
abbreviation op_und_b::"w σ ⇒ w σ" ("⋆⇧B_" [57]58) (* ⋆ as border of the complement *)
  where "⋆⇧BA ≡ ℬ⇧d⇧- A"


text‹Observe that assumming EXPN for closure we are allowed to exchange A and B variants.›
lemma pundAB: "EXPN 𝒞 ⟹ ⋆⇧AA = ⋆⇧BA" using neg_char by (metis BA_deMorgan1 BA_dn L4 L9 dimpl_char impl_char ofp_comm_dc2 op_fixpoint_def sdfun_dcompl_def setequ_ext svfun_compl_def)
lemma pdetAB: "EXPN 𝒞 ⟹ ¤⇧AA = ¤⇧BA" by (metis dual_compl_char1 pundAB sfun_compl_invol svfun_compl_def)

text‹Variants A and B give us slightly different properties (there are countermodels for those not shown).›
lemma Prop1: "¤⇧BA = 𝒞⇧f⇧p A" by (simp add: dual_invol setequ_ext)
lemma Prop2: "¤⇧AA = (𝒞 A ❙→ A)" unfolding conn by (metis compl_def svfun_compl_def)
lemma Prop3: "fp ℐ A ⟷ [⊢ ¤⇧B❙─A]" by (simp add: dual_invol fp_d_rel gtrue_def)
lemma Prop4a: "fp 𝒞 A ⟷ [⊢ ¤⇧BA]" by (simp add: dual_invol fp_rel gtrue_def)
lemma Prop4b: "fp 𝒞 A  ⟶ [⊢ ¤⇧AA]" by (simp add: compl_def fixpoints_def join_def setequ_ext svfun_compl_def)

text‹Recovering TND works for both variants.›
lemma "[¤⇧Aa ⊢ a, ❙¬a]" by (simp add: subset_def)
lemma "[⊢ ⋆⇧Aa ❙∨ a ❙∨ ❙¬a]" by (metis compl_def join_def)
lemma "[¤⇧Ba ⊢ a, ❙¬a]" by (simp add: compl_def dimpl_def dual_invol join_def op_fixpoint_def subset_def svfun_compl_def)
lemma "[⊢ ⋆⇧Ba ❙∨ a ❙∨ ❙¬a]" by (metis dimpl_def dual_compl_char1 dual_invol join_def ofp_comm_compl op_fixpoint_def)

text‹We show how (local) contraposition variants (among others) can be recovered using the
 determinedness operators.›
lemma "[¤⇧Aa, a ❙→ b ⊢ ❙¬b ❙→ ❙¬a]" nitpick oops
lemma det_lcop0_A: "EXPN 𝒞 ⟹ [¤⇧Aa,  a ❙→ b ⊢ ❙¬b ❙→ ❙¬a]" using neg_char impl_char unfolding conn order  by fastforce
lemma "[¤⇧Ba, a ❙→ b ⊢ ❙¬b ❙→ ❙¬a]" nitpick oops
lemma det_lcop0_B: "EXPN 𝒞 ⟹ [¤⇧Ba,  a ❙→ b ⊢ ❙¬b ❙→ ❙¬a]" by (metis det_lcop0_A pdetAB)
lemma "[¤⇧Aa, a ❙→ ❙¬b ⊢ b ❙→ ❙¬a]" nitpick oops
lemma det_lcop1_A: "EXPN 𝒞 ⟹ [¤⇧Aa, a ❙→ ❙¬b ⊢  b ❙→ ❙¬a]" by (smt (verit, ccfv_SIG) impl_char impl_def join_def meet_def neg_char subset_def)
lemma "[¤⇧Ba, a ❙→ ❙¬b ⊢ b ❙→ ❙¬a]" nitpick oops
lemma det_lcop1_B: "EXPN 𝒞 ⟹ [¤⇧Ba, a ❙→ ❙¬b ⊢  b ❙→ ❙¬a]" by (metis det_lcop1_A pdetAB)
lemma "[¤⇧Aa, ❙¬a ❙→ b ⊢ ❙¬b ❙→ a]" nitpick oops
lemma det_lcop2_A: "EXPN 𝒞 ⟹ [¤⇧Aa, ❙¬a ❙→ b ⊢ ❙¬b ❙→ a]" by (smt (verit, del_insts) neg_char compl_def impl_char join_def meet_def subset_def)
lemma "[¤⇧Ba, ❙¬a ❙→ b ⊢ ❙¬b ❙→ a]" nitpick oops
lemma det_lcop2_B: "EXPN 𝒞 ⟹ [¤⇧Ba, ❙¬a ❙→ b ⊢ ❙¬b ❙→ a]" by (metis det_lcop2_A pdetAB)

end