Theory ex_LFUs
theory ex_LFUs
imports topo_derivative_algebra sse_operation_negative
begin
nitpick_params[assms=true, user_axioms=true, show_all, expect=genuine, format=3]
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::"bool⇒bool" ("∼_" [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 "[A⇩1, A⇩2 ❙⊢ B] ≡ A⇩1 ❙∧ A⇩2 ❙≼ B"
abbreviation conseq_local12::"σ⇒σ⇒σ⇒bool" ("[_ ❙⊢ _,_]") where "[A ❙⊢ B⇩1, B⇩2] ≡ A ❙≼ B⇩1 ❙∨ B⇩2"
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
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 ❙≈ 𝒞⇧f⇧p 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
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
lemma "𝔇 𝒟 ⟹ DNE(❙¬)" nitpick oops
lemma "Der_1b 𝒟 ⟹ CoPw(❙¬)" by (smt CoPw_def MONO_ADDIb PD1 compl_def ineg_def monI)
lemma "𝔇 𝒟 ⟹ CoP1(❙¬)" nitpick oops
lemma "𝔇 𝒟 ⟹ CoP2(❙¬)" nitpick oops
lemma "𝔇 𝒟 ⟹ CoP3(❙¬)" nitpick oops
lemma "𝔇 𝒟 ⟹ DM3(❙¬)" nitpick oops
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
lemma "𝔇 𝒟 ⟹ MT3(❙¬)" nitpick oops
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
lemma det_lcop1: "[❙∘a, a ❙→ b ❙⊢ ❙¬b ❙→ ❙¬a]" using dual_def pI1 conn by auto
lemma "𝔇 𝒟 ⟹ lCoP1(❙→)(❙¬)" nitpick oops
lemma det_lcop2: "[❙∘a, a ❙→ ❙¬b ❙⊢ b ❙→ ❙¬a]" using dual_def pI1 conn by auto
lemma "𝔇 𝒟 ⟹ lCoP2(❙→)(❙¬)" nitpick oops
lemma det_lcop3: "[❙∘a, ❙¬a ❙→ b ❙⊢ ❙¬b ❙→ a]" using dual_def pI1 conn by auto
lemma "𝔇 𝒟 ⟹ lCoP3(❙→)(❙¬)" nitpick oops
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
lemma det_ds2: "[❙∘a, ❙¬a ❙→ b ❙⊢ a ❙∨ b]" using pB1 dual_def conn by auto
end