# Theory sse_operation_negative

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

section ‹Negative semantic conditions for operations›

text‹\noindent{We define and interrelate some conditions on operations (i.e. propositional functions of type
@{text "σ⇒σ"}), this time involving negative-like properties.}›

named_theorems Defs

subsection ‹Definitions and interrelations (finitary case)›

subsubsection ‹Principles of excluded middle, contradiction and explosion›

text‹\noindent{TND: tertium non datur, aka. law of excluded middle (resp. strong, weak, minimal).}›
abbreviation pTND  ("TND⇧_  _") where "TND⇧a  η ≡       ❙⊤  ❙≈ a ❙∨ (η a)"
abbreviation pTNDw ("TNDw⇧_ _") where "TNDw⇧a η ≡ ∀b. (η b) ❙≼ a ❙∨ (η a)"
abbreviation pTNDm ("TNDm⇧_ _") where "TNDm⇧a η ≡     (η ❙⊥) ❙≼ a ❙∨ (η a)"
definition "TND  η ≡ ∀φ. TND⇧φ  η"
definition "TNDw η ≡ ∀φ. TNDw⇧φ η"
definition "TNDm η ≡ ∀φ. TNDm⇧φ η"
declare TND_def[Defs] TNDw_def[Defs] TNDm_def[Defs]

text‹\noindent{Explore some (non)entailment relations:}›
lemma "TND  η ⟹ TNDw η" unfolding Defs conn by simp
lemma "TNDw η ⟹ TND  η" nitpick oops
lemma "TNDw η ⟹ TNDm η" unfolding Defs by simp
lemma "TNDm η ⟹ TNDw η" nitpick oops

text‹\noindent{ECQ: ex contradictione (sequitur) quodlibet (resp: strong, weak, minimal).}›
abbreviation pECQ  ("ECQ⇧_ _")  where "ECQ⇧a  η ≡     a ❙∧ (η a) ❙≈ ❙⊥"
abbreviation pECQw ("ECQw⇧_ _") where "ECQw⇧a η ≡ ∀b. a ❙∧ (η a) ❙≼ (η b)"
abbreviation pECQm ("ECQm⇧_ _") where "ECQm⇧a η ≡     a ❙∧ (η a) ❙≼ (η ❙⊤)"
definition "ECQ  η ≡ ∀a. ECQ⇧a  η"
definition "ECQw η ≡ ∀a. ECQw⇧a η"
definition "ECQm η ≡ ∀a. ECQm⇧a η"
declare ECQ_def[Defs] ECQw_def[Defs] ECQm_def[Defs]

text‹\noindent{Explore some (non)entailment relations:}›
lemma "ECQ  η ⟹ ECQw η" unfolding Defs conn by blast
lemma "ECQw η ⟹ ECQ  η" nitpick oops
lemma "ECQw η ⟹ ECQm η" unfolding Defs conn by simp
lemma "ECQm η ⟹ ECQw η" nitpick oops

abbreviation pLNC  ("LNC⇧_ _")  where "LNC⇧a η ≡ η(a ❙∧ η a) ❙≈ ❙⊤"
definition "LNC η ≡ ∀a. LNC⇧a η"
declare LNC_def[Defs]

text‹\noindent{ECQ and LNC are in general independent.}›
lemma "ECQ η ⟹ LNC η" nitpick oops
lemma "LNC η ⟹ ECQm η" nitpick oops

subsubsection ‹Contraposition rules›

text‹\noindent{CoP: contraposition (global/rule variants, resp. weak, strong var. 1, strong var. 2, strong var. 3).}›
abbreviation pCoPw ("CoPw⇧_⇧_ _") where "CoPw⇧a⇧b η ≡ a ❙≼ b ⟶ (η b) ❙≼ (η a)"
abbreviation pCoP1 ("CoP1⇧_⇧_ _") where "CoP1⇧a⇧b η ≡ a ❙≼ (η b) ⟶ b ❙≼ (η a)"
abbreviation pCoP2 ("CoP2⇧_⇧_ _") where "CoP2⇧a⇧b η ≡ (η a) ❙≼ b ⟶ (η b) ❙≼ a"
abbreviation pCoP3 ("CoP3⇧_⇧_ _") where "CoP3⇧a⇧b η ≡ (η a) ❙≼ (η b) ⟶ b ❙≼ a"
definition "CoPw  η ≡ ∀a b. CoPw⇧a⇧b η"
definition "CoP1  η ≡ ∀a b. CoP1⇧a⇧b η"
definition "CoP1' η ≡ ∀a b. a ❙≼ (η b) ⟷ b ❙≼ (η a)"
definition "CoP2  η ≡ ∀a b. CoP2⇧a⇧b η"
definition "CoP2' η ≡ ∀a b. (η a) ❙≼ b ⟷ (η b) ❙≼ a"
definition "CoP3  η ≡ ∀a b. CoP3⇧a⇧b η"
declare CoPw_def[Defs] CoP1_def[Defs] CoP1'_def[Defs]
CoP2_def[Defs] CoP2'_def[Defs] CoP3_def[Defs]

lemma CoP1_defs_rel: "CoP1 η = CoP1' η" unfolding Defs by metis
lemma CoP2_defs_rel: "CoP2 η = CoP2' η" unfolding Defs by metis

text‹\noindent{Explore some (non)entailment relations:}›
lemma "CoP1 η ⟹ CoPw η" unfolding Defs by metis
lemma "CoPw η ⟹ CoP1 η" nitpick oops
lemma "CoP2 η ⟹ CoPw η" unfolding Defs by metis
lemma "CoPw η ⟹ CoP2 η" nitpick oops
lemma "CoP3 η ⟹ CoPw η" (*nitpick*) oops ―‹ no countermodel found so far ›
lemma "CoPw η ⟹ CoP3 η" nitpick oops

text‹\noindent{All three strong variants are pairwise independent. However, CoP3 follows from CoP1 plus CoP2.}›
lemma CoP123: "CoP1 η ⟹ CoP2 η ⟹ CoP3 η" unfolding Defs by smt
text‹\noindent{Taking all CoP together still leaves room for a boldly paraconsistent resp. paracomplete logic.}›
lemma "CoP1 η ⟹ CoP2 η ⟹ ECQm η" nitpick oops
lemma "CoP1 η ⟹ CoP2 η ⟹ TNDm η" nitpick oops

subsubsection ‹Modus tollens rules›

text‹\noindent{MT: modus (tollendo) tollens (global/rule variants).}›
abbreviation pMT0 ("MT0⇧_⇧_ _") where "MT0⇧a⇧b η ≡ a ❙≼ b ∧ (η b) ❙≈ ❙⊤ ⟶ (η a) ❙≈ ❙⊤"
abbreviation pMT1 ("MT1⇧_⇧_ _") where "MT1⇧a⇧b η ≡ a ❙≼ (η b) ∧ b ❙≈ ❙⊤ ⟶ (η a) ❙≈ ❙⊤"
abbreviation pMT2 ("MT2⇧_⇧_ _") where "MT2⇧a⇧b η ≡ (η a) ❙≼ b ∧ (η b) ❙≈ ❙⊤ ⟶ a ❙≈ ❙⊤"
abbreviation pMT3 ("MT3⇧_⇧_ _") where "MT3⇧a⇧b η ≡ (η a) ❙≼ (η b) ∧ b ❙≈ ❙⊤ ⟶ a ❙≈ ❙⊤"
definition "MT0 η ≡ ∀a b. MT0⇧a⇧b η"
definition "MT1 η ≡ ∀a b. MT1⇧a⇧b η"
definition "MT2 η ≡ ∀a b. MT2⇧a⇧b η"
definition "MT3 η ≡ ∀a b. MT3⇧a⇧b η"
declare MT0_def[Defs] MT1_def[Defs] MT2_def[Defs] MT3_def[Defs]

text‹\noindent{Again, all MT variants are pairwise independent. We explore some (non)entailment relations:}›
lemma "CoPw η ⟹ MT0 η" unfolding Defs by (metis top_def)
lemma "CoP1 η ⟹ MT1 η" unfolding Defs by (metis top_def)
lemma "CoP2 η ⟹ MT2 η" unfolding Defs by (metis top_def)
lemma "CoP3 η ⟹ MT3 η" unfolding Defs by (metis top_def)
lemma "MT0 η ⟹ MT1 η ⟹ MT2 η ⟹ MT3 η ⟹ CoPw η" nitpick oops
lemma "MT0 η ⟹ MT1 η ⟹ MT2 η ⟹ MT3 η ⟹ ECQm η" nitpick oops
lemma "MT0 η ⟹ MT1 η ⟹ MT2 η ⟹ MT3 η ⟹ TNDm η" nitpick oops
lemma MT123: "MT1 η ⟹ MT2 η ⟹ MT3 η"  unfolding Defs by smt

subsubsection ‹Double negation introduction and elimination›

text‹\noindent{DNI/DNE: double negation introduction/elimination (as axioms).}›
abbreviation pDNI ("DNI⇧_ _") where "DNI⇧a η ≡ a ❙≼ η (η a)"
abbreviation pDNE ("DNE⇧_ _") where "DNE⇧a η ≡ η (η a) ❙≼ a"
definition "DNI η ≡ ∀a. DNI⇧a η"
definition "DNE η ≡ ∀a. DNE⇧a η"
declare DNI_def[Defs] DNE_def[Defs]

text‹\noindent{CoP1 (resp. CoP2) can alternatively be defined as CoPw plus DNI (resp. DNE).}›
lemma "DNI η ⟹ CoP1 η" nitpick oops
lemma CoP1_def2: "CoP1 η = (CoPw η ∧ DNI η)" unfolding Defs by smt
lemma "DNE η ⟹  CoP2 η" nitpick oops
lemma CoP2_def2: "CoP2 η = (CoPw η ∧ DNE η)" unfolding Defs by smt

text‹\noindent{Explore some non-entailment relations:}›
lemma "DNI η ⟹ DNE η ⟹ CoPw η" nitpick oops
lemma "DNI η ⟹ DNE η ⟹ TNDm η" nitpick oops
lemma "DNI η ⟹ DNE η ⟹ ECQm η" nitpick oops
lemma "DNI η ⟹ DNE η ⟹ MT0 η" nitpick oops
lemma "DNI η ⟹ DNE η ⟹ MT1 η" nitpick oops
lemma "DNI η ⟹ DNE η ⟹ MT2 η" nitpick oops
lemma "DNI η ⟹ DNE η ⟹ MT3 η" nitpick oops

text‹\noindent{DNI/DNE: double negation introduction/elimination (as rules).}›
abbreviation prDNI ("rDNI⇧_ _") where "rDNI⇧a η ≡ a ❙≈ ❙⊤ ⟶ η (η a) ❙≈ ❙⊤"
abbreviation prDNE ("rDNE⇧_ _") where "rDNE⇧a η ≡ η (η a) ❙≈ ❙⊤ ⟶ a ❙≈ ❙⊤"
definition "rDNI η ≡ ∀a. rDNI⇧a η"
definition "rDNE η ≡ ∀a. rDNE⇧a η"
declare rDNI_def[Defs] rDNE_def[Defs]

text‹\noindent{The rule variants are strictly weaker than the axiom variants,}›
lemma "DNI η ⟹ rDNI η" by (simp add: DNI_def rDNI_def top_def)
lemma "rDNI η ⟹ DNI η" nitpick oops
lemma "DNE η ⟹ rDNE η" by (metis DNE_def rDNE_def top_def)
lemma "rDNE η ⟹ DNE η" nitpick oops
lemma MT1_rDNI: "MT1 η ⟹ rDNI η" unfolding Defs by blast
lemma MT2_rDNE: "MT2 η ⟹ rDNE η" unfolding Defs by blast

subsubsection ‹Normality and its dual›

text‹\noindent{n(D)Nor: negative (dual) 'normality'.}›
definition "nNor η ≡ (η ❙⊥) ❙≈ ❙⊤"
definition "nDNor η ≡ (η ❙⊤) ❙≈ ❙⊥"
declare nNor_def[Defs] nDNor_def[Defs]

text‹\noindent{nNor (resp. nDNor) is entailed by CoP1 (resp. CoP2). }›
lemma CoP1_Nor: "CoP1 η ⟹ nNor η" unfolding Defs conn by simp
lemma CoP2_DNor: "CoP2 η ⟹ nDNor η" unfolding Defs conn by fastforce
lemma "DNI η ⟹ nNor η" nitpick oops
lemma "DNE η ⟹ nDNor η" nitpick oops
text‹\noindent{nNor and nDNor together entail the rule variant of DNI (rDNI).}›
lemma nDNor_rDNI: "nNor η ⟹ nDNor η ⟹ rDNI η" unfolding Defs using nDNor_def nNor_def eq_ext by metis
lemma "nNor η ⟹ nDNor η ⟹ rDNE η" nitpick oops

subsubsection ‹De Morgan laws›

text‹\noindent{DM: De Morgan laws.}›
abbreviation pDM1 ("DM1⇧_⇧_ _") where "DM1⇧a⇧b η ≡ η(a ❙∨ b) ❙≼ (η a) ❙∧ (η b)"
abbreviation pDM2 ("DM2⇧_⇧_ _") where "DM2⇧a⇧b η ≡ (η a) ❙∨ (η b) ❙≼ η(a ❙∧ b)"
abbreviation pDM3 ("DM3⇧_⇧_ _") where "DM3⇧a⇧b η ≡ η(a ❙∧ b) ❙≼ (η a) ❙∨ (η b)"
abbreviation pDM4 ("DM4⇧_⇧_ _") where "DM4⇧a⇧b η ≡ (η a) ❙∧ (η b) ❙≼  η(a ❙∨ b)"
definition "DM1 η ≡ ∀a b. DM1⇧a⇧b η"
definition "DM2 η ≡ ∀a b. DM2⇧a⇧b η"
definition "DM3 η ≡ ∀a b. DM3⇧a⇧b η"
definition "DM4 η ≡ ∀a b. DM4⇧a⇧b η"
declare DM1_def[Defs] DM2_def[Defs] DM3_def[Defs] DM4_def[Defs]

text‹\noindent{CoPw, DM1 and DM2 are indeed equivalent.}›
lemma DM1_CoPw: "DM1 η = CoPw η" proof -
have LtoR: "DM1 η ⟹ CoPw η" proof -
assume dm1: "DM1 η"
{ fix a b
{ assume "a ❙≼ b"
hence 1: "a ❙∨ b ❙≼ b" unfolding conn by simp
have 2: "b ❙≼ a ❙∨ b" unfolding conn by simp
from 1 2 have "b = a ❙∨ b" using eq_ext by blast
hence 3: "η b ❙≈ η (a ❙∨ b)" by auto
from dm1 have "η(a ❙∨ b) ❙≼ (η a) ❙∧ (η b)" unfolding Defs by blast
hence 4: "(η b) ❙≼ (η a) ❙∧ (η b)" using 3 by simp
have 5: "(η a) ❙∧ (η b) ❙≼ (η a)" unfolding conn by simp
from 4 5 have "(η b) ❙≼ (η a)" by simp
} hence "a ❙≼ b ⟶ (η b) ❙≼ (η a)" by (rule impI)
} thus ?thesis unfolding Defs by simp
qed
have RtoL: "CoPw η ⟹ DM1 η" unfolding Defs conn by (metis (no_types, lifting))
thus ?thesis using LtoR RtoL by blast
qed
lemma DM2_CoPw: "DM2 η = CoPw η" proof -
have LtoR: "DM2 η ⟹ CoPw η" proof -
assume dm2: "DM2 η"
{ fix a b
{ assume "a ❙≼ b"
hence 1: "a ❙≼ a ❙∧ b" unfolding conn by simp
have 2: "a ❙∧ b ❙≼ a" unfolding conn by simp
from 1 2 have "a = a ❙∧ b" using eq_ext by blast
hence 3: "η a ❙≈ η (a ❙∧ b)" by auto
from dm2 have "(η a) ❙∨ (η b) ❙≼ η(a ❙∧ b)" unfolding Defs by blast
hence 4: "(η a) ❙∨ (η b) ❙≼ (η a) " using 3 by simp
have 5: "(η b) ❙≼ (η a) ❙∨ (η b)" unfolding conn by simp
from 4 5 have "(η b) ❙≼ (η a)" by simp
} hence "a ❙≼ b ⟶ (η b) ❙≼ (η a)" by (rule impI)
} thus ?thesis unfolding Defs by simp
qed
have RtoL: "CoPw η ⟹ DM2 η" unfolding Defs conn by (metis (no_types, lifting))
thus ?thesis using LtoR RtoL by blast
qed
lemma DM12: "DM1 η = DM2 η" by (simp add: DM1_CoPw DM2_CoPw)

text‹\noindent{DM3 (resp. DM4) are entailed by CoPw together with DNE (resp. DNI).}›
lemma CoPw_DNE_DM3: "CoPw η ⟹ DNE η ⟹ DM3 η" proof -
assume copw: "CoPw η" and dne: "DNE η"
{ fix a b
have "η(a) ❙≼ (η a) ❙∨ (η b)" unfolding conn by simp
hence "η(η(a) ❙∨ η(b)) ❙≼ η((η a))" using CoPw_def copw by (metis (no_types, lifting))
hence 1: "η(η(a) ❙∨ η(b)) ❙≼ a" using DNE_def dne by metis
have "η(b) ❙≼ (η a) ❙∨ (η b)" unfolding conn by simp
hence "η(η(a) ❙∨ η(b)) ❙≼ η((η b))" using CoPw_def copw by (metis (no_types, lifting))
hence 2: "η(η(a) ❙∨ η(b)) ❙≼ b" using DNE_def dne by metis
from 1 2 have "η(η(a) ❙∨ η(b)) ❙≼ a ❙∧ b" unfolding conn by simp
hence "η(a ❙∧ b) ❙≼ η(η(η(a) ❙∨ η(b)))" using CoPw_def copw by smt
hence "η(a ❙∧ b) ❙≼ (η a) ❙∨ (η b)" using DNE_def dne by metis
} thus ?thesis by (simp add: DM3_def)
qed
lemma CoPw_DNI_DM4: "CoPw η ⟹ DNI η ⟹ DM4 η" proof -
assume copw: "CoPw η" and dni: "DNI η"
{ fix a b
have "(η a) ❙∧ (η b) ❙≼ η(a)" unfolding conn by simp
hence "η((η a)) ❙≼ η(η(a) ❙∧ η(b))" using CoPw_def copw by (metis (no_types, lifting))
hence 1: "a ❙≼ η(η(a) ❙∧ η(b))" using DNI_def dni by metis
have "(η a) ❙∧ (η b) ❙≼ η(b)" unfolding conn by simp
hence "η((η b)) ❙≼ η(η(a) ❙∧ η(b))" using CoPw_def copw by (metis (no_types, lifting))
hence 2: "b ❙≼ η(η(a) ❙∧ η(b))" using DNI_def dni by metis
from 1 2 have "a ❙∨ b ❙≼ η(η(a) ❙∧ η(b))" unfolding conn by simp
hence "η(η(η(a) ❙∧ η(b))) ❙≼ η(a ❙∨ b)" using CoPw_def copw by auto
hence "η(a) ❙∧ η(b) ❙≼ η(a ❙∨ b)" using DNI_def dni by simp
} thus ?thesis by (simp add: DM4_def)
qed
text‹\noindent{From this follows that DM3 (resp. DM4) is entailed by CoP2 (resp. CoP1).}›
lemma CoP2_DM3: "CoP2 η ⟹ DM3 η" by (simp add: CoP2_def2 CoPw_DNE_DM3)
lemma CoP1_DM4: "CoP1 η ⟹ DM4 η" by (simp add: CoP1_def2 CoPw_DNI_DM4)
text‹\noindent{Explore some non-entailment relations:}›
lemma "CoPw η ⟹ DM3 η ⟹ DM4 η ⟹ nNor η ⟹ nDNor η ⟹ DNI η" nitpick oops
lemma "CoPw η ⟹ DM3 η ⟹ DM4 η ⟹ nNor η ⟹ nDNor η ⟹ DNE η" nitpick oops
lemma "CoPw η ⟹ DM3 η ⟹ DM4 η ⟹ DNI η ⟹ DNE η ⟹ ECQm η" nitpick oops
lemma "CoPw η ⟹ DM3 η ⟹ DM4 η ⟹ DNI η ⟹ DNE η ⟹ TNDm η" nitpick oops

subsubsection ‹Contextual (strong) contraposition rule›

text‹\noindent{XCoP: contextual contraposition (global/rule variant).}›
abbreviation pXCoP ("XCoP⇧_⇧_ _") where "XCoP⇧a⇧b η ≡ ∀c. c ❙∧ a ❙≼ b ⟶ c ❙∧ (η b) ❙≼ (η a)"
definition "XCoP η ≡ ∀a b. XCoP⇧a⇧b η"
declare XCoP_def[Defs]

text‹\noindent{XCoP can alternatively be defined as ECQw plus TNDw.}›
lemma XCoP_def2: "XCoP η = (ECQw η ∧ TNDw η)" proof -
have LtoR1: "XCoP η ⟹ ECQw η" unfolding XCoP_def ECQw_def conn by auto
have LtoR2: "XCoP η ⟹ TNDw η" unfolding XCoP_def TNDw_def conn by (smt atom_def atomic2 conn)
have RtoL: "ECQw η ∧ TNDw η ⟹ XCoP η" using XCoP_def ECQw_def TNDw_def unfolding conn by metis
from LtoR1 LtoR2 RtoL show ?thesis by blast
qed
text‹\noindent{Explore some (non)entailment relations:}›
lemma "XCoP η ⟹ ECQ η" nitpick oops
lemma "XCoP η ⟹ TND η" nitpick oops
lemma XCoP_CoPw: "XCoP η ⟹ CoPw η" unfolding Defs conn by metis
lemma "XCoP η ⟹ CoP1 η" nitpick oops
lemma "XCoP η ⟹ CoP2 η" nitpick oops
lemma "XCoP η ⟹ CoP3 η" nitpick oops
lemma "CoP1 η ∧ CoP2 η ⟹ XCoP η" nitpick oops
lemma "XCoP η ⟹ nNor η" nitpick oops
lemma "XCoP η ⟹ nDNor η" nitpick oops
lemma "XCoP η ⟹ rDNI η" nitpick oops
lemma "XCoP η ⟹ rDNE η" nitpick oops
lemma XCoP_DM3: "XCoP η ⟹ DM3 η" unfolding DM3_def XCoP_def conn using ECQw_def TNDw_def atom_def atomic2 conn by smt
lemma XCoP_DM4: "XCoP η ⟹ DM4 η" unfolding DM4_def XCoP_def conn using ECQw_def TNDw_def atom_def atomic2 conn by smt

subsubsection ‹Local contraposition axioms›
text‹\noindent{Observe that the definitions below take implication as an additional parameter: @{text "ι"}.}›

text‹\noindent{lCoP: contraposition (local/axiom variants).}›
abbreviation plCoPw ("lCoPw⇧_⇧_ _ _") where "lCoPw⇧a⇧b ι η ≡ (ι a b::σ) ❙≼ (ι (η b) (η a))"
abbreviation plCoP1 ("lCoP1⇧_⇧_ _ _") where "lCoP1⇧a⇧b ι η ≡ (ι a (η b::σ)) ❙≼ (ι b (η a))"
abbreviation plCoP2 ("lCoP2⇧_⇧_ _ _") where "lCoP2⇧a⇧b ι η ≡ (ι (η a) b::σ) ❙≼ (ι (η b) a)"
abbreviation plCoP3 ("lCoP3⇧_⇧_ _ _") where "lCoP3⇧a⇧b ι η ≡ (ι (η a) (η b::σ)) ❙≼ (ι b a)"
definition "lCoPw  ι η ≡ ∀a b. lCoPw⇧a⇧b ι η"
definition "lCoP1  ι η ≡ ∀a b. lCoP1⇧a⇧b ι η"
definition "lCoP1' ι η ≡ ∀a b. (ι a (η b)) ❙≈ (ι b (η a))"
definition "lCoP2  ι η ≡ ∀a b. lCoP2⇧a⇧b ι η"
definition "lCoP2' ι η ≡ ∀a b. (ι (η a) b) ❙≈ (ι (η b) a)"
definition "lCoP3  ι η ≡ ∀a b. lCoP3⇧a⇧b ι η"
declare lCoPw_def[Defs] lCoP1_def[Defs] lCoP1'_def[Defs]
lCoP2_def[Defs] lCoP2'_def[Defs] lCoP3_def[Defs]

lemma lCoP1_defs_rel: "lCoP1 ι η = lCoP1' ι η" by (metis (full_types) lCoP1'_def lCoP1_def)
lemma lCoP2_defs_rel: "lCoP2 ι η = lCoP2' ι η" by (metis (full_types) lCoP2'_def lCoP2_def)

text‹\noindent{All local contraposition variants are in general independent from each other. However if we take
classical implication we can verify some relationships.}›

lemma lCoP1_def2: "lCoP1(❙→) η = (lCoPw(❙→) η ∧ DNI η)" unfolding Defs conn by smt
lemma lCoP2_def2: "lCoP2(❙→) η = (lCoPw(❙→) η ∧ DNE η)" unfolding Defs conn by smt

lemma "lCoP1(❙→) η ⟹ lCoPw(❙→) η" unfolding Defs conn by metis
lemma "lCoPw(❙→) η ⟹ lCoP1(❙→) η" nitpick oops
lemma "lCoP2(❙→) η ⟹ lCoPw(❙→) η" unfolding Defs conn by metis
lemma "lCoPw(❙→) η ⟹ lCoP2(❙→) η" nitpick oops
lemma "lCoP3(❙→) η ⟹ lCoPw(❙→) η" unfolding Defs conn by blast
lemma "lCoPw(❙→) η ⟹ lCoP3(❙→) η" nitpick oops
lemma lCoP123: "lCoP1(❙→) η ∧ lCoP2(❙→) η ⟹ lCoP3(❙→) η" unfolding Defs conn by metis

text‹\noindent{Local variants imply global ones as expected.}›
lemma "lCoPw(❙→) η ⟹ CoPw η" unfolding Defs conn by metis
lemma "lCoP1(❙→) η ⟹ CoP1 η" unfolding Defs conn by metis
lemma "lCoP2(❙→) η ⟹ CoP2 η" unfolding Defs conn by metis
lemma "lCoP3(❙→) η ⟹ CoP3 η" unfolding Defs conn by metis

text‹\noindent{Explore some (non)entailment relations.}›
lemma lCoPw_XCoP: "lCoPw(❙→) η = XCoP η" unfolding Defs conn by (smt XCoP_def XCoP_def2 TNDw_def conn)
lemma lCoP1_TND: "lCoP1(❙→) η ⟹ TND η" by (smt XCoP_CoPw XCoP_def2 CoP1_Nor CoP1_def2 nNor_def TND_def TNDw_def lCoP1_def2 lCoPw_XCoP conn)
lemma "TND η ⟹ lCoP1(❙→) η" nitpick oops
lemma lCoP2_ECQ: "lCoP2(❙→) η ⟹ ECQ η" by (smt XCoP_CoPw XCoP_def2 CoP2_DNor CoP2_def2 nDNor_def ECQ_def ECQw_def lCoP2_def2 lCoPw_XCoP conn)
lemma "ECQ η ⟹ lCoP2(❙→) η" nitpick oops

subsubsection ‹Local modus tollens axioms›

text‹\noindent{lMT: Modus tollens (local/axiom variants).}›
abbreviation plMT0 ("lMT0⇧_⇧_ _ _") where "lMT0⇧a⇧b ι η ≡ (ι a b::σ) ❙∧ (η b) ❙≼ (η a)"
abbreviation plMT1 ("lMT1⇧_⇧_ _ _") where "lMT1⇧a⇧b ι η ≡ (ι a (η b::σ)) ❙∧ b ❙≼ (η a)"
abbreviation plMT2 ("lMT2⇧_⇧_ _ _") where "lMT2⇧a⇧b ι η ≡ (ι (η a) b::σ) ❙∧ (η b) ❙≼ a"
abbreviation plMT3 ("lMT3⇧_⇧_ _ _") where "lMT3⇧a⇧b ι η ≡ (ι (η a) (η b::σ)) ❙∧ b ❙≼ a"
definition "lMT0 ι η ≡ ∀a b. lMT0⇧a⇧b ι η"
definition "lMT1 ι η ≡ ∀a b. lMT1⇧a⇧b ι η"
definition "lMT2 ι η ≡ ∀a b. lMT2⇧a⇧b ι η"
definition "lMT3 ι η ≡ ∀a b. lMT3⇧a⇧b ι η"
declare lMT0_def[Defs] lMT1_def[Defs] lMT2_def[Defs] lMT3_def[Defs]

text‹\noindent{All local MT variants are in general independent from each other and also from local CoP instances.
However if we take classical implication we can verify that local MT and CoP are indeed equivalent.}›
lemma "lMT0(❙→) η = lCoPw(❙→) η" unfolding Defs conn by metis
lemma "lMT1(❙→) η = lCoP1(❙→) η" unfolding Defs conn by metis
lemma "lMT2(❙→) η = lCoP2(❙→) η" unfolding Defs conn by metis
lemma "lMT3(❙→) η = lCoP3(❙→) η" unfolding Defs conn by metis

subsubsection ‹Disjunctive syllogism›

text‹\noindent{DS: disjunctive syllogism.}›
abbreviation pDS1 ("DS1⇧_⇧_ _ _") where "DS1⇧a⇧b ι η ≡ (a ❙∨ b::σ) ❙≼ (ι (η a) b)"
abbreviation pDS2 ("DS2⇧_⇧_ _ _") where "DS2⇧a⇧b ι η ≡ (ι (η a) b::σ) ❙≼ (a ❙∨ b)"
abbreviation pDS3 ("DS3⇧_⇧_ _ _") where "DS3⇧a⇧b ι η ≡ ((η a) ❙∨ b::σ) ❙≼ (ι a b)"
abbreviation pDS4 ("DS4⇧_⇧_ _ _") where "DS4⇧a⇧b ι η ≡ (ι a b::σ) ❙≼ ((η a) ❙∨ b)"
definition "DS1 ι η ≡ ∀a b. DS1⇧a⇧b ι η"
definition "DS2 ι η ≡ ∀a b. DS2⇧a⇧b ι η"
definition "DS3 ι η ≡ ∀a b. DS3⇧a⇧b ι η"
definition "DS4 ι η ≡ ∀a b. DS4⇧a⇧b ι η"
declare DS1_def[Defs] DS2_def[Defs] DS3_def[Defs] DS4_def[Defs]

text‹\noindent{All DS variants are in general independent from each other. However if we take classical implication
we can verify that the pairs DS1-DS3 and DS2-DS4 are indeed equivalent. }›
lemma "DS1(❙→) η = DS3(❙→) η" unfolding Defs by (metis impl_def join_def)
lemma "DS2(❙→) η = DS4(❙→) η" unfolding Defs by (metis impl_def join_def)

text‹\noindent{Explore some (non)entailment relations.}›
lemma DS1_nDNor: "DS1(❙→) η ⟹ nDNor η" unfolding Defs by (metis bottom_def impl_def join_def top_def)
lemma DS2_nNor:  "DS2(❙→) η ⟹ nNor η" unfolding Defs by (metis bottom_def impl_def join_def top_def)
lemma lCoP2_DS1: "lCoP2(❙→) η ⟹ DS1(❙→) η" unfolding Defs conn by metis
lemma lCoP1_DS2: "lCoP1(❙→) η ⟹ DS2(❙→) η" unfolding Defs by (metis (no_types, lifting) conn)
lemma "CoP2 η ⟹ DS1(❙→) η" nitpick oops
lemma "CoP1 η ⟹ DS2(❙→) η" nitpick oops

end