# Theory topo_negation_fixedpoints

theory topo_negation_fixedpoints
imports topo_frontier_algebra sse_operation_negative_quantification
begin
nitpick_params[assms=true, user_axioms=true, show_all, expect=genuine, format=3] (*default Nitpick settings*)

section ‹Frontier-based negation - Fixed-points›

text‹\noindent{We define a paracomplete and a paraconsistent negation employing the interior and the closure operation
respectively. We explore the use of fixed-point predicates to recover some relevant properties of negation,
many of which cannot be readily recovered by just adding semantic conditions.
We take the frontier operator as primitive and explore which semantic conditions are minimally required.}›

definition neg_I::"σ⇒σ" ("❙¬⇧I")  where  "❙¬⇧I φ ≡ ℐ(❙─φ)"
definition neg_C::"σ⇒σ" ("❙¬⇧C")  where  "❙¬⇧C φ ≡ 𝒞(❙─φ)"
declare neg_I_def[conn] neg_C_def[conn]

text‹\noindent{Note that all results obtained for fixed-point predicates extend to their associated operators as follows:}›
lemma "∀A. γ⇧f⇧p(A) ❙∧ φ(A) ❙≼ ψ(A) ⟹ ∀A. (fp γ)(A) ⟶ φ(A) ❙≼ ψ(A)" unfolding conn by simp
lemma "∀A B. γ⇧f⇧p(A) ❙∧ γ⇧f⇧p(B) ❙∧ (φ A B) ❙≼ (ψ A B) ⟹ ∀A B. (fp γ)(A) ∧ (fp γ)(B) ⟶ (φ A B) ❙≼ (ψ A B)" unfolding conn by simp

text‹\noindent{Recall from previous results that if we have Fr(A) then we also have both Cl(A) and Br(A).
With this understanding we will tacitly assume the corresponding results for Fr(-) below.
Moreover, we obtained countermodels (using Nitpick) for all formulas featuring other combinations (not shown).}›

subsection ‹'Explosion' (ECQ) and excluded middle (TND)›

text‹\noindent{TND-I}›
lemma "Fr_2 ℱ ⟹ ∀A. Cl(A) ⟶ TND⇧A ❙¬⇧I" by (simp add: OpCldual conn)
text‹\noindent{ECQ-C}›
lemma "Fr_2 ℱ ⟹ ∀A. Op(A) ⟶ ECQ⇧A ❙¬⇧C" using Cl_fr_def Int_fr_def pF2 unfolding conn by fastforce

subsection ‹Contraposition rules›

text‹\noindent{CoPw-I}›
lemma "∀A B. Br(❙─B) ⟶ CoPw⇧A⇧B ❙¬⇧I" using Int_fr_def pB1 conn by auto
lemma "Fr_2 ℱ ⟹ ∀A B. Cl(A)  ⟶ CoPw⇧A⇧B ❙¬⇧I" using Int_fr_def OpCldual conn by auto
text‹\noindent{CoPw-C}›
lemma "Fr_2 ℱ ⟹ ∀A B. Br(A) ⟶ CoPw⇧A⇧B ❙¬⇧C" using pA2 pB2 pF2 unfolding conn by metis
lemma "Fr_2 ℱ ⟹ ∀A B. Op(B) ⟶ CoPw⇧A⇧B ❙¬⇧C" using ClOpdual Cl_fr_def unfolding conn by auto

text‹\noindent{CoP1-I}›
lemma "Fr_2 ℱ ⟹ ∀A B. Cl(A) ⟶  CoP1⇧A⇧B ❙¬⇧I" using Int_fr_def OpCldual conn by auto
lemma "Fr_1b ℱ ⟹ ∀A B. Op(B) ⟶  CoP1⇧A⇧B ❙¬⇧I" by (smt IF2 dEXP_def MONO_def monI conn)
lemma CoP1_I_rec: "Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ ∀A B. Br (❙─B) ⟶ CoP1⇧A⇧B ❙¬⇧I" using IF3 dNOR_def Br_boundary unfolding conn by auto
text‹\noindent{CoP1-C}›
lemma "Fr_2 ℱ ⟹ ∀A B. Op(B) ⟶ CoP1⇧A⇧B ❙¬⇧C" using Int_fr_def pC2 pF2 unfolding conn by metis
lemma "Fr_2 ℱ ⟹ ∀A B. Br(A) ⟶ CoP1⇧A⇧B ❙¬⇧C" using Br_fr_def Cl_fr_def pF2 unfolding conn by fastforce

text‹\noindent{CoP2-I}›
lemma "Fr_2 ℱ ⟹ ∀A B. Cl(A) ⟶ CoP2⇧A⇧B ❙¬⇧I" using Int_fr_def OpCldual unfolding conn by auto
lemma "∀A B. Br (❙─B) ⟶ CoP2⇧A⇧B ❙¬⇧I" by (simp add: pI1 conn)
text‹\noindent{CoP2-C}›
lemma "Fr_2 ℱ ⟹ ∀A B. Op(B) ⟶  CoP2⇧A⇧B ❙¬⇧C" using Cl_fr_def Int_fr_def pF2 unfolding conn by fastforce
lemma "Fr_6 ℱ ⟹ ∀A B. Cl(A) ⟶  CoP2⇧A⇧B ❙¬⇧C" by (smt Cl_fr_def MONO_def monC conn)
lemma "Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ ∀A B. Br(A) ⟶ CoP2⇧A⇧B ❙¬⇧C" using CoP1_I_rec Disj_IF pA2 pF2 pF3 unfolding conn by smt

text‹\noindent{CoP3-I}›
lemma "Fr_2 ℱ ⟹ ∀A B. Cl(A) ⟶ CoP3⇧A⇧B ❙¬⇧I" by (metis Disj_I ICdual' compl_def dual_def eq_ext' meet_def neg_I_def)
text‹\noindent{CoP3-C}›
lemma "Fr_2 ℱ ⟹ ∀A B. Op(B) ⟶ CoP3⇧A⇧B ❙¬⇧C" by (metis Disj_I ICdual compl_def dual_def eq_ext' meet_def neg_C_def)

text‹\noindent{XCoP-I}›
lemma "Fr_2 ℱ ⟹ ∀A B. Cl(A) ⟶  XCoP⇧A⇧B ❙¬⇧I" using Fr_2_def pA1 pA2 pF1 unfolding conn by metis
lemma "∀A B. Br(❙─B) ⟶  XCoP⇧A⇧B ❙¬⇧I" using IB_rel Int_br_def diff_def eq_ext' conn by fastforce
text‹\noindent{XCoP-C}›
lemma "Fr_2 ℱ ⟹ ∀A B. Op(B) ⟶ XCoP⇧A⇧B ❙¬⇧C" by (metis ClOpdual compl_def diff_def meet_def neg_C_def pA2)
lemma "Fr_2 ℱ ⟹ ∀A B.  ∀A B. Br(A) ⟶ XCoP⇧A⇧B ❙¬⇧C" using Cl_fr_def compl_def join_def neg_C_def pF3 by fastforce

subsection ‹Double negation introduction/elimination›

text‹\noindent{DNI-I}›
lemma "Fr_1b ℱ ⟹ ∀A. Op(A) ⟶ DNI⇧A ❙¬⇧I" using MONO_def monI pA1 unfolding conn by smt
lemma "Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ ∀A. Br (❙─A) ⟶ DNI⇧A ❙¬⇧I" using CoP1_I_rec by simp
text‹\noindent{DNI-C}›
lemma "Fr_2 ℱ ⟹ ∀A. Op(A) ⟶ DNI⇧A ❙¬⇧C" using Cl_fr_def Int_fr_def pF2 unfolding conn by fastforce

text‹\noindent{DNE-I}›
lemma "Fr_2 ℱ ⟹ ∀A. Cl(A) ⟶ DNE⇧A ❙¬⇧I" by (simp add: Cl_fr_def Fr_2_def Int_fr_def conn)
text‹\noindent{DNE-C}›
lemma "Fr_6 ℱ ⟹ ∀A. Cl(A) ⟶ DNE⇧A ❙¬⇧C" by (smt MONO_def monC pC2 conn)
lemma "Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ ∀A. Br(A) ⟶ DNE⇧A ❙¬⇧C" using CoP1_I_rec Disj_IF pA2 pF2 pF3 unfolding conn by smt

subsection ‹De Morgan laws›

text‹\noindent{DM1-I}›
lemma "Fr_1b ℱ ⟹ ∀A B. DM1⇧A⇧B ❙¬⇧I" by (smt MONO_def monI conn)
lemma "Fr_2 ℱ ⟹ ∀A B. Cl(A) ∧ Cl(B) ⟶ DM1⇧A⇧B ❙¬⇧I" using pF2 pI2 conn by fastforce
text‹\noindent{DM1-C}›
lemma "Fr_6 ℱ ⟹ ∀A B. DM1⇧A⇧B ❙¬⇧C" by (smt MONO_def monC conn)
lemma "Fr_2 ℱ ⟹ ∀A B. Br(A) ∧ Br(B) ⟶ DM1⇧A⇧B ❙¬⇧C" using CF2 EXP_def pF2 pF3 unfolding conn by metis

text‹\noindent{DM2-I}›
lemma "Fr_1b ℱ ⟹ ∀A B. DM2⇧A⇧B ❙¬⇧I" by (smt MONO_def monI conn)
lemma "∀A B. Br(❙─A) ∧ Br(❙─B) ⟶ DM2⇧A⇧B ❙¬⇧I" using Int_fr_def pB1 conn by auto
text‹\noindent{DM2-C}›
lemma "Fr_6 ℱ ⟹ ∀A B. DM2⇧A⇧B ❙¬⇧C" by (smt MONO_def monC conn)
lemma "Fr_2 ℱ ⟹ ∀A B. Op(A) ∧ Op(B) ⟶ DM2⇧A⇧B ❙¬⇧C" using CF2 ClOpdual EXP_def unfolding conn by auto

text‹\noindent{DM3-I}›
lemma "Fr_2 ℱ ⟹ ∀A B. Cl(A) ∧ Cl(B) ⟶ DM3⇧A⇧B ❙¬⇧I" using Int_fr_def pF2 unfolding conn by fastforce
text‹\noindent{DM3-C}›
lemma "Fr_1a ℱ ⟹ Fr_2 ℱ ⟹ ∀A B. DM3⇧A⇧B ❙¬⇧C" using Cl_fr_def Fr_1a_def pF2 unfolding conn by metis
lemma "Fr_2 ℱ ⟹ ∀A B. Br(A) ∧ Br(B) ⟶ DM3⇧A⇧B ❙¬⇧C" using Cl_fr_def pF3 unfolding conn by fastforce

text‹\noindent{DM4-I}›
lemma "Fr_1a ℱ ⟹ Fr_2 ℱ ⟹ ∀A B. DM4⇧A⇧B ❙¬⇧I" using ADDI_a_def Br_fr_def CF1a Int_fr_def pC1 unfolding conn by (metis (full_types))
lemma "∀A B. Br(❙─A) ∧ Br(❙─B) ⟶ DM4⇧A⇧B ❙¬⇧I" using Int_fr_def pB1 conn by auto
text‹\noindent{DM4-C}›
lemma "Fr_2 ℱ ⟹ ∀A B. Op(A) ∧ Op(B) ⟶ DM4⇧A⇧B ❙¬⇧C" using Cl_fr_def Int_fr_def pF2 unfolding conn by (metis (full_types))
lemma "Fr_1 ℱ ⟹ Fr_2 ℱ ⟹ Fr_4 ℱ ⟹ ∀A B. Fr(A) ∧ Fr(B) ⟶ DM4⇧A⇧B ❙¬⇧C" using Cl_fr_def Fr_join_closed Fr_2_def compl_def join_def neg_C_def by auto

subsection ‹Local contraposition axioms›

text‹\noindent{lCoPw-I}›
lemma "Fr_2 ℱ ⟹ ∀A B. Cl(A) ⟶ lCoPw⇧A⇧B(❙→) ❙¬⇧I" using Int_fr_def OpCldual unfolding conn by auto
lemma "∀A B. Br(❙─B) ⟶ lCoPw⇧A⇧B(❙→) ❙¬⇧I" by (simp add: pI1 conn)
text‹\noindent{lCoPw-C}›
lemma "Fr_2 ℱ ⟹ ∀A B. Op(B) ⟶ lCoPw⇧A⇧B(❙→) ❙¬⇧C" using Cl_fr_def Int_fr_def pF2 unfolding conn by fastforce
lemma "Fr_2 ℱ ⟹ ∀A B. Br(A) ⟶ lCoPw⇧A⇧B(❙→) ❙¬⇧C" by (simp add: pC1 conn)

text‹\noindent{lCoP1-I}›
lemma "Fr_2 ℱ ⟹ ∀A B. Cl(A) ⟶ lCoP1⇧A⇧B(❙→) ❙¬⇧I" using Int_fr_def OpCldual unfolding conn by auto
text‹\noindent{lCoP1-C}›
lemma "Fr_2 ℱ ⟹ ∀A B. Op(B) ⟶ lCoP1⇧A⇧B(❙→) ❙¬⇧C" using Cl_fr_def Int_fr_def pF2 unfolding conn by fastforce
lemma "Fr_2 ℱ ⟹ ∀A B. Br(A) ⟶ lCoP1⇧A⇧B(❙→) ❙¬⇧C" by (simp add: pC1 conn)

text‹\noindent{lCoP2-I}›
lemma "Fr_2 ℱ ⟹ ∀A B. Cl(A) ⟶ lCoP2⇧A⇧B(❙→) ❙¬⇧I" using Int_fr_def OpCldual unfolding conn by auto
lemma "∀A B. Br(❙─B) ⟶ lCoP2⇧A⇧B(❙→) ❙¬⇧I" by (simp add: pI1 conn)
text‹\noindent{lCoP2-C}›
lemma "Fr_2 ℱ ⟹ ∀A B. Op(B) ⟶ lCoP2⇧A⇧B(❙→) ❙¬⇧C" using Cl_fr_def Int_fr_def pF2 unfolding conn by fastforce

text‹\noindent{lCoP3-I}›
lemma "Fr_2 ℱ ⟹ ∀A B. Cl(A) ⟶ lCoP3⇧A⇧B(❙→) ❙¬⇧I" using Int_fr_def OpCldual unfolding conn by auto
text‹\noindent{lCoP3-C}›
lemma "Fr_2 ℱ ⟹ ∀A B. Op(B) ⟶ lCoP3⇧A⇧B(❙→) ❙¬⇧C" using Cl_fr_def Int_fr_def pF2 unfolding conn by fastforce

subsection ‹Disjunctive syllogism›

text‹\noindent{DS1-I}›
lemma "∀A B. DS1⇧A⇧B(❙→) ❙¬⇧I" by (simp add: Int_fr_def conn)
text‹\noindent{DS1-C}›
lemma "Fr_2 ℱ ⟹ ∀A B.  Op(A) ⟶ DS1⇧A⇧B(❙→) ❙¬⇧C" using Cl_fr_def Int_fr_def pF2 unfolding conn by fastforce

text‹\noindent{DS2-I}›
lemma "Fr_2 ℱ ⟹ ∀A B. Cl(A) ⟶ DS2⇧A⇧B(❙→) ❙¬⇧I" using OpCldual unfolding conn by auto
text‹\noindent{DS2-C}›
lemma "∀A B. DS2⇧A⇧B(❙→) ❙¬⇧C"  using Cl_fr_def unfolding conn by auto

end