Theory topo_negation_conditions

theory topo_negation_conditions
  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 - Semantic conditions›

text‹\noindent{We define a paracomplete and a paraconsistent negation employing the interior and closure operation resp.
We take the frontier operator as primitive and explore which semantic conditions are minimally required
to obtain some relevant properties of negation.}›

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

text‹\noindent{(We rename the meta-logical HOL negation to avoid terminological confusion)}›
abbreviation cneg::"bool⇒bool" ("∼_" [40]40) where "∼φ ≡ ¬φ" 

subsection ‹'Explosion' (ECQ), non-contradiction (LNC) and excluded middle (TND)›

text‹\noindent{TND}›
lemma "𝔉 ℱ ⟹ TNDm ❙¬⇧I" nitpick oops (*minimally weak TND not valid*)
lemma TND_C: "TND ❙¬⇧C" by (simp add: pC2 Defs conn) (*TND valid in general*)

text‹\noindent{ECQ}›
lemma ECQ_I: "ECQ ❙¬⇧I" by (simp add: pI2 Defs conn) (*ECQ valid in general*)
lemma "𝔉 ℱ ⟹ ECQm ❙¬⇧C" nitpick oops (*minimally weak ECQ not valid*)

text‹\noindent{LNC}›
lemma "LNC ❙¬⇧I" nitpick oops (*countermodel*)
lemma LNC_I: "Fr_2 ℱ ⟹ Fr_3 ℱ ⟹  LNC ❙¬⇧I" using ECQ_I ECQ_def IF3 LNC_def dNOR_def unfolding conn by auto
lemma "LNC ❙¬⇧C" nitpick oops (*countermodel*)
lemma LNC_C: "Fr_6 ℱ ⟹ LNC ❙¬⇧C" unfolding Defs by (smt Cl_fr_def MONO_def compl_def join_def meet_def monC neg_C_def top_def)

text‹\noindent{Relations between LNC and different ECQ variants (only relevant for paraconsistent negation).}›
lemma "ECQ ❙¬⇧C ⟶  LNC ❙¬⇧C" by (simp add: pC2 Defs conn)
lemma ECQw_LNC: "ECQw ❙¬⇧C ⟶  LNC ❙¬⇧C" by (smt ECQw_def LNC_def pC2 conn)
lemma ECQm_LNC: "Fr_1 ℱ ⟹ Fr_2 ℱ ⟹ ECQm ❙¬⇧C ⟶ LNC ❙¬⇧C" using Cl_fr_def Fr_1_def pF2 unfolding Defs conn by metis
lemma "𝔉 ℱ ⟹ LNC ❙¬⇧C ⟶  ECQm ❙¬⇧C" nitpick oops  (*countermodel*)

text‹\noindent{Below we show that enforcing all conditions on the frontier operator still leaves room
for both boldly paraconsistent and paracomplete models. We use Nitpick to generate a non-trivial 
model (here a set algebra with 8 elements).}›
lemma "𝔉 ℱ ∧ ∼ECQm ❙¬⇧C" nitpick[satisfy,card w=3] oops (*boldly paraconsistent model found*)
lemma "𝔉 ℱ ∧ ∼TNDm ❙¬⇧I" nitpick[satisfy,card w=3] oops (*boldly paracomplete model found*)


subsection ‹Modus tollens (MT)›

text‹\noindent{MT-I}›
lemma MT0_I: "Fr_1b ℱ ⟹ MT0 ❙¬⇧I"  unfolding Defs by (smt MONO_def compl_def monI neg_I_def top_def)
lemma MT1_I: "Fr_1b ℱ ⟹ Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ MT1 ❙¬⇧I" unfolding Defs by (metis MONO_def monI IF3 Int_fr_def compl_def dNOR_def diff_def neg_I_def top_def)
lemma "𝔉 ℱ ⟹ MT2 ❙¬⇧I" nitpick oops (*countermodel*)
lemma "∼TND ❙¬⇧I ∧ Fr_1 ℱ ∧ Fr_2 ℱ ∧ Fr_4 ℱ ∧ MT2 ❙¬⇧I" nitpick[satisfy,card w=3] oops
lemma "∼TNDm ❙¬⇧I ∧ Fr_1a ℱ ∧ Fr_2 ℱ ∧ Fr_3 ℱ ∧ Fr_4 ℱ ∧ MT2 ❙¬⇧I" nitpick[satisfy] oops
lemma "∼TNDm ❙¬⇧I ∧ Fr_1 ℱ ∧ Fr_2 ℱ ∧ Fr_4 ℱ ∧ MT2 ❙¬⇧I" nitpick[satisfy,card w=3] oops
lemma "∼TNDm ❙¬⇧I ∧ Fr_1 ℱ ∧ Fr_3 ℱ ∧ Fr_4 ℱ ∧ MT2 ❙¬⇧I" nitpick[satisfy,card w=3] oops
lemma "𝔉 ℱ ⟹ MT3 ❙¬⇧I" nitpick oops (*countermodel*)
lemma "∼TNDm ❙¬⇧I ∧ Fr_1a ℱ ∧ Fr_2 ℱ ∧ Fr_3 ℱ ∧ Fr_4 ℱ ∧ MT3 ❙¬⇧I" nitpick[satisfy,card w=3] oops
lemma "∼TNDm ❙¬⇧I ∧ MT0 ❙¬⇧I ∧ MT1 ❙¬⇧I ∧ MT2 ❙¬⇧I ∧ MT3 ❙¬⇧I" nitpick[satisfy,card w=3] oops
text‹\noindent{MT-C}›
lemma "Fr_2 ℱ ⟹ MT0 ❙¬⇧C" nitpick oops (*countermodel*)
lemma MT0_C: "Fr_6 ℱ ⟹ MT0 ❙¬⇧C" unfolding Defs by (smt ICdual MONO_def compl_def monC neg_C_def top_def)
lemma MT1_C: "Fr_6 ℱ ⟹ MT1 ❙¬⇧C" unfolding Defs by (smt Cl_fr_def Fr_6_def conn)
lemma "𝔉 ℱ ⟹ MT2 ❙¬⇧C" nitpick oops (*countermodel*)
lemma "∼ECQm ❙¬⇧C ∧ 𝔉 ℱ ∧ MT2 ❙¬⇧C" nitpick[satisfy,card w=3] oops (*model found*)
lemma MT3_C: "Fr_1b ℱ ⟹ Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ MT3 ❙¬⇧C" unfolding Defs using MONO_def monI by (metis ClOpdual IF3 compl_def dNOR_def diff_def neg_C_def pA2 top_def)
lemma "∼ECQm ❙¬⇧C ∧ MT0 ❙¬⇧C ∧ MT1 ❙¬⇧C ∧ MT2 ❙¬⇧C ∧ MT3 ❙¬⇧C" nitpick[satisfy,card w=3] oops


subsection ‹Contraposition rules (CoP)›

text‹\noindent{CoPw-I}›
lemma "CoPw ❙¬⇧I" nitpick oops (*countermodel*)
lemma CoPw_I: "Fr_1b ℱ ⟹ CoPw ❙¬⇧I" unfolding Defs conn by (metis (no_types, lifting) MONO_def monI)
text‹\noindent{CoPw-C}›
lemma "CoPw ❙¬⇧C" nitpick oops (*countermodel*)
lemma CoPw_C: "Fr_6 ℱ ⟹ CoPw ❙¬⇧C" by (smt CoPw_def MONO_def monC conn)

text‹\noindent{We can indeed prove that XCoP is entailed by CoP1 (CoP2) in the particular case of a closure- (interior-)based negation.}›
lemma CoP1_XCoP: "CoP1 ❙¬⇧C ⟶  XCoP ❙¬⇧C" by (metis XCoP_def2 CoP1_def CoP1_def2 DM2_CoPw DM2_def ECQw_def TND_C TND_def TNDw_def top_def)
lemma CoP2_XCoP: "CoP2 ❙¬⇧I ⟶  XCoP ❙¬⇧I" by (smt XCoP_def2 CoP2_DM3 CoP2_def2 CoPw_def DM3_def DNE_def ECQ_I ECQ_def ECQw_def TNDw_def bottom_def join_def)

text‹\noindent{CoP1-I}›
lemma "𝔉 ℱ ⟹ CoP1 ❙¬⇧I" nitpick oops (*countermodel*)
lemma "∼TNDm ❙¬⇧I ∧ 𝔉 ℱ ∧ CoP1 ❙¬⇧I" nitpick[satisfy,card w=3] oops
text‹\noindent{CoP1-C}›
lemma "𝔉 ℱ ⟹ CoP1 ❙¬⇧C" nitpick oops (*countermodel*)
lemma "∼ECQ ❙¬⇧C ∧ Fr_1 ℱ ∧ Fr_2 ℱ ∧ Fr_4 ℱ ∧ CoP1 ❙¬⇧C" nitpick[satisfy,card w=3] oops
lemma "CoP1 ❙¬⇧C ⟶ ECQm ❙¬⇧C" using XCoP_def2 CoP1_XCoP ECQm_def ECQw_def by blast

text‹\noindent{CoP2-I}›
lemma "𝔉 ℱ ⟹ CoP2 ❙¬⇧I" nitpick oops (*countermodel*)
lemma "∼TND ❙¬⇧I ∧ Fr_1 ℱ ∧ Fr_2 ℱ ∧ Fr_4 ℱ ∧ CoP2 ❙¬⇧I" nitpick[satisfy,card w=3] oops
lemma "∼TND ❙¬⇧I ∧ Fr_1 ℱ ∧ Fr_3 ℱ ∧ Fr_4 ℱ ∧ CoP2 ❙¬⇧I" nitpick[satisfy,card w=3] oops
lemma "CoP2 ❙¬⇧I ⟶ TNDm ❙¬⇧I" using XCoP_def2 CoP2_XCoP TNDm_def TNDw_def by auto
text‹\noindent{CoP2-C}›
lemma "𝔉 ℱ ⟹ CoP2 ❙¬⇧C" nitpick oops (*countermodel*)
lemma "∼ECQm ❙¬⇧C ∧ 𝔉 ℱ ∧ CoP2 ❙¬⇧C" nitpick[satisfy,card w=3] oops

text‹\noindent{CoP3-I}›
lemma "𝔉 ℱ ⟹ CoP3 ❙¬⇧I" nitpick oops (*countermodel*)
lemma "∼TND ❙¬⇧I ∧ CoP3 ❙¬⇧I" (*nitpick[satisfy]*) oops (*cannot find (finite) models*)
text‹\noindent{CoP3-C}›
lemma "𝔉 ℱ ⟹ CoP3 ❙¬⇧C" nitpick oops (*countermodel*)
lemma "∼ECQ ❙¬⇧C ∧ CoP3 ❙¬⇧C" (*nitpick[satisfy]*) oops (*cannot find (finite) models*)

text‹\noindent{XCoP-I}›
lemma "𝔉 ℱ ⟹ XCoP ❙¬⇧I" nitpick oops (*countermodel*)
lemma "∼TND ❙¬⇧I ∧ Fr_1 ℱ ∧ Fr_2 ℱ ∧ Fr_4 ℱ ∧ XCoP ❙¬⇧I" nitpick[satisfy,card w=3] oops
lemma "∼TND ❙¬⇧I ∧ Fr_1 ℱ ∧ Fr_3 ℱ ∧ Fr_4 ℱ ∧ XCoP ❙¬⇧I" nitpick[satisfy,card w=3] oops
lemma "XCoP ❙¬⇧I ⟶ TNDm ❙¬⇧I" by (simp add: XCoP_def2 TNDm_def TNDw_def)
text‹\noindent{XCoP-C}›
lemma "𝔉 ℱ ⟹ XCoP ❙¬⇧C" nitpick oops (*countermodel*)
lemma "∼ECQ ❙¬⇧C ∧ Fr_1 ℱ ∧ Fr_2 ℱ ∧ Fr_4 ℱ ∧ XCoP ❙¬⇧C" nitpick[satisfy,card w=3] oops
lemma "XCoP ❙¬⇧C ⟶ ECQm ❙¬⇧C" by (simp add: XCoP_def2 ECQm_def ECQw_def)


subsection ‹Normality (negative) and its dual (nNor/nDNor)›

text‹\noindent{nNor-I}› 
lemma "nNor ❙¬⇧I" nitpick oops (*countermodel*)
lemma nNor_I: "Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ nNor ❙¬⇧I"  using IF3 dNOR_def unfolding Defs conn by auto
text‹\noindent{nNor-C}› 
lemma nNor_C: "nNor ❙¬⇧C" unfolding Cl_fr_def Defs conn by simp

text‹\noindent{nDNor-I}› 
lemma nDNor_I: "nDNor ❙¬⇧I" unfolding Int_fr_def Defs conn by simp
text‹\noindent{nDNor-C}› 
lemma "nDNor ❙¬⇧C" nitpick oops (*countermodel*)
lemma nDNor_C: "Fr_3 ℱ ⟹ nDNor ❙¬⇧C" using pC2 NOR_def unfolding Defs conn by simp


subsection ‹Double negation introduction/elimination (DNI/DNE)›

text‹\noindent{DNI-I}›
lemma "𝔉 ℱ ⟹ DNI ❙¬⇧I" nitpick oops (*countermodel*)
lemma "∼TNDm ❙¬⇧I ∧ 𝔉 ℱ ∧ DNI ❙¬⇧I" nitpick[satisfy,card w=3] oops
text‹\noindent{DNI-C}›
lemma "𝔉 ℱ ⟹ DNI ❙¬⇧C" nitpick oops (*countermodel*)
lemma "∼ECQ ❙¬⇧C ∧ Fr_1 ℱ ∧ Fr_2 ℱ ∧ Fr_4 ℱ ∧ DNI ❙¬⇧C" nitpick[satisfy,card w=3] oops
lemma "∼ECQm ❙¬⇧C ∧ Fr_1 ℱ ∧ Fr_3 ℱ ∧ Fr_4 ℱ ∧ DNI ❙¬⇧C" nitpick[satisfy,card w=3] oops
lemma "∼ECQm ❙¬⇧C ∧ Fr_2 ℱ ∧ Fr_3 ℱ ∧ Fr_4 ℱ ∧ DNI ❙¬⇧C" nitpick[satisfy,card w=3] oops

text‹\noindent{DNE-I}›
lemma "𝔉 ℱ ⟹ DNE ❙¬⇧I" nitpick oops (*countermodel*)
lemma "∼TND ❙¬⇧I ∧ Fr_1 ℱ ∧ Fr_2 ℱ ∧ Fr_4 ℱ ∧ DNE ❙¬⇧I" nitpick[satisfy,card w=3] oops
lemma "∼TND ❙¬⇧I ∧ Fr_1 ℱ ∧ Fr_3 ℱ ∧ Fr_4 ℱ ∧ DNE ❙¬⇧I" nitpick[satisfy,card w=3] oops
lemma "∼TNDm ❙¬⇧I ∧ Fr_2 ℱ ∧ Fr_3 ℱ ∧ Fr_4 ℱ ∧ DNE ❙¬⇧I" nitpick[satisfy,card w=3] oops
lemma "∼TND ❙¬⇧I  ∧ DNE ❙¬⇧I ∧ DNI ❙¬⇧I" (*nitpick[satisfy]*) oops (*cannot find (finite) models*)
text‹\noindent{DNE-C}›
lemma "𝔉 ℱ ⟹ DNE ❙¬⇧C" nitpick oops (*countermodel*)
lemma "∼ECQm ❙¬⇧C ∧ 𝔉 ℱ ∧ DNE ❙¬⇧C" nitpick[satisfy,card w=3] oops

lemma "∼ECQ ❙¬⇧C  ∧ DNE ❙¬⇧C ∧ DNI ❙¬⇧C" (*nitpick[satisfy]*) oops (*cannot find (finite) models*)

text‹\noindent{rDNI-I}›
lemma "Fr_2 ℱ ⟹ Fr_3 ℱ ⟹ rDNI ❙¬⇧I" using nNor_I nDNor_I nDNor_rDNI by simp
text‹\noindent{rDNI-C}›
lemma "Fr_3 ℱ ⟹ rDNI ❙¬⇧C" using nNor_C nDNor_C nDNor_rDNI by simp

text‹\noindent{rDNE-I}›
lemma "𝔉 ℱ ⟹ rDNE ❙¬⇧I" nitpick oops (*countermodel*)
lemma "∼TNDm ❙¬⇧I ∧ Fr_1 ℱ ∧ Fr_2 ℱ ∧ Fr_4 ℱ ∧ rDNE ❙¬⇧I" nitpick[satisfy,card w=3] oops
lemma "∼TNDm ❙¬⇧I ∧ Fr_1 ℱ ∧ Fr_3 ℱ ∧ Fr_4 ℱ ∧ rDNE ❙¬⇧I" nitpick[satisfy,card w=3] oops
lemma "∼TNDm ❙¬⇧I ∧ Fr_2 ℱ ∧ Fr_3 ℱ ∧ Fr_4 ℱ ∧ rDNE ❙¬⇧I" nitpick[satisfy,card w=3] oops
text‹\noindent{rDNE-C}›
lemma "𝔉 ℱ ⟹ rDNE ❙¬⇧C" nitpick oops (*countermodel*)
lemma "∼ECQm ❙¬⇧C ∧ 𝔉 ℱ ∧ rDNE ❙¬⇧C" nitpick[satisfy,card w=3] oops

lemma "∼ECQm ❙¬⇧C  ∧ rDNE ❙¬⇧C ∧ rDNI ❙¬⇧C" nitpick[satisfy,card w=3] oops


subsection ‹De Morgan laws›

text‹\noindent{DM1/2 (see CoPw)}›

text‹\noindent{DM3-I}›
lemma "𝔉 ℱ ⟹ DM3 ❙¬⇧I" nitpick oops (*countermodel*)
lemma "∼TND ❙¬⇧I ∧ Fr_1 ℱ ∧ Fr_2 ℱ ∧ Fr_4 ℱ ∧ DM3 ❙¬⇧I" nitpick[satisfy,card w=3] oops
lemma "∼TND ❙¬⇧I ∧ Fr_1 ℱ ∧ Fr_3 ℱ ∧ Fr_4 ℱ ∧ DM3 ❙¬⇧I" nitpick[satisfy,card w=3] oops
lemma "∼TNDm ❙¬⇧I ∧ DM3 ❙¬⇧I" (*nitpick[satisfy]*) oops (*cannot find (finite) models*)
text‹\noindent{DM3-C}›
lemma "DM3 ❙¬⇧C" nitpick oops (*countermodel*)
lemma DM3_C: "Fr_1a ℱ ⟹ Fr_2 ℱ ⟹ DM3 ❙¬⇧C" using  DM3_def Fr_1a_def pA2 pF2 unfolding conn by smt
lemma "∼ECQm ❙¬⇧C ∧ 𝔉 ℱ ∧ DM3 ❙¬⇧C" nitpick[satisfy,card w=3] oops

text‹\noindent{DM4-I}›
lemma "DM4 ❙¬⇧I" nitpick oops (*countermodel*)
lemma DM4_I: "Fr_1a ℱ ⟹ DM4 ❙¬⇧I" using ADDI_a_def Cl_fr_def DM4_def IC1b IF1b dual_def unfolding conn by smt
lemma "∼TNDm ❙¬⇧I ∧ 𝔉 ℱ ∧ DM4 ❙¬⇧I" nitpick[satisfy,card w=3] oops
text‹\noindent{DM4-C}›
lemma "𝔉 ℱ ⟹ DM4 ❙¬⇧C" nitpick oops (*countermodel*)
lemma "∼ECQ ❙¬⇧C ∧ Fr_1 ℱ ∧ Fr_2 ℱ ∧ Fr_4 ℱ ∧ DM4 ❙¬⇧C" nitpick[satisfy,card w=3] oops
lemma "∼ECQm ❙¬⇧C ∧ DM4 ❙¬⇧C" (*nitpick[satisfy]*) oops (*cannot find (finite) models*)

text‹\noindent{iDM1/2 (see CoPw)}›

text‹\noindent{iDM3-I}›
lemma "𝔉 ℱ ⟹ Fr_inf ℱ ⟹ iDM3 ❙¬⇧I" nitpick oops (*countermodel*)
lemma "∼TND ❙¬⇧I ∧ Fr_1 ℱ ∧ Fr_2 ℱ ∧ Fr_4 ℱ ∧ iDM3 ❙¬⇧I" nitpick[satisfy] oops
lemma "∼TND ❙¬⇧I ∧ Fr_1 ℱ ∧ Fr_3 ℱ ∧ Fr_4 ℱ ∧ iDM3 ❙¬⇧I" nitpick[satisfy] oops
lemma "∼TNDm ❙¬⇧I ∧ iDM3 ❙¬⇧I" (*nitpick[satisfy]*) oops (*cannot find (finite) models*)
text‹\noindent{iDM3-C}›
lemma "iDM3 ❙¬⇧C" nitpick oops (*countermodel*)
lemma iDM3_C: "Fr_2 ℱ ⟹ Fr_inf ℱ ⟹ iDM3 ❙¬⇧C" unfolding Defs by (metis (full_types) CF_inf Ra_restr_ex dom_compl_def iADDI_a_def iDM_a neg_C_def)
text‹\noindent{iDM4-I}›
lemma "iDM4 ❙¬⇧I" nitpick oops (*countermodel*)
lemma iDM4_I: "Fr_inf ℱ ⟹ iDM4 ❙¬⇧I" unfolding Defs by (metis IF_inf Ra_restr_all dom_compl_def iDM_b iMULT_b_def neg_I_def)
text‹\noindent{iDM4-C}›
lemma "𝔉 ℱ ⟹ Fr_inf ℱ ⟹ iDM4 ❙¬⇧C" nitpick oops (*countermodel*)
lemma "∼ECQ ❙¬⇧C ∧ Fr_1 ℱ ∧ Fr_2 ℱ ∧ Fr_4 ℱ ∧ iDM4 ❙¬⇧C" nitpick[satisfy] oops
lemma "∼ECQm ❙¬⇧C ∧ iDM4 ❙¬⇧C" (*nitpick[satisfy]*) oops (*cannot find (finite) models*)


subsection ‹Local contraposition axioms (lCoP)›

text‹\noindent{lCoPw-I}›
lemma "𝔉 ℱ ⟹ lCoPw(❙→) ❙¬⇧I" nitpick oops (*countermodel*)
lemma "∼TND ❙¬⇧I ∧ Fr_1 ℱ ∧ Fr_2 ℱ ∧ Fr_4 ℱ ∧ lCoPw(❙→) ❙¬⇧I" nitpick[satisfy,card w=3] oops
lemma "∼TND ❙¬⇧I ∧ Fr_1 ℱ ∧ Fr_3 ℱ ∧ Fr_4 ℱ ∧ lCoPw(❙→) ❙¬⇧I" nitpick[satisfy,card w=3] oops
lemma "lCoPw(❙→) ❙¬⇧I ⟶ TNDm ❙¬⇧I" by (simp add: XCoP_def2 TNDm_def TNDw_def lCoPw_XCoP)
text‹\noindent{lCoPw-C}›
lemma "𝔉 ℱ ⟹ lCoPw(❙→) ❙¬⇧C" nitpick oops (*countermodel*)
lemma "∼ECQ ❙¬⇧C ∧ Fr_1 ℱ ∧ Fr_2 ℱ ∧ Fr_4 ℱ ∧ lCoPw(❙→) ❙¬⇧C" nitpick[satisfy,card w=3] oops
lemma "lCoPw(❙→) ❙¬⇧C ⟶ ECQm ❙¬⇧C" by (simp add: XCoP_def2 ECQm_def ECQw_def lCoPw_XCoP)

text‹\noindent{lCoP1-I}›
lemma "𝔉 ℱ ⟹ lCoP1(❙→) ❙¬⇧I" nitpick oops (*countermodel*)
lemma "lCoP1(❙→) ❙¬⇧I ⟶ TND ❙¬⇧I" by (simp add: lCoP1_TND)
text‹\noindent{lCoP1-C}›
lemma "𝔉 ℱ ⟹ lCoP1(❙→) ❙¬⇧C" nitpick oops (*countermodel*)
lemma "∼ECQ ❙¬⇧C ∧ Fr_1 ℱ ∧ Fr_2 ℱ ∧ Fr_4 ℱ ∧ lCoP1(❙→) ❙¬⇧C" nitpick[satisfy,card w=3] oops
lemma "lCoP1(❙→) ❙¬⇧C ⟶ ECQm ❙¬⇧C" by (simp add: XCoP_def2 ECQm_def ECQw_def lCoP1_def2 lCoPw_XCoP)

text‹\noindent{lCoP2-I}›
lemma "𝔉 ℱ ⟹ lCoP2(❙→) ❙¬⇧I" nitpick oops (*countermodel*)
lemma "∼TND ❙¬⇧I ∧ Fr_1 ℱ ∧ Fr_2 ℱ ∧ Fr_4 ℱ ∧ lCoP2(❙→) ❙¬⇧I" nitpick[satisfy,card w=3] oops
lemma "∼TND ❙¬⇧I ∧ Fr_1 ℱ ∧ Fr_3 ℱ ∧ Fr_4 ℱ ∧ lCoP2(❙→) ❙¬⇧I" nitpick[satisfy,card w=3] oops
lemma "lCoP2(❙→) ❙¬⇧I ⟶ TNDm ❙¬⇧I" by (simp add: XCoP_def2 TNDm_def TNDw_def lCoP2_def2 lCoPw_XCoP)
text‹\noindent{lCoP2-C}›
lemma "𝔉 ℱ ⟹ lCoP2(❙→) ❙¬⇧C" nitpick oops (*countermodel*)
lemma "lCoP2(❙→) ❙¬⇧C ⟶ ECQ ❙¬⇧C" by (simp add: lCoP2_ECQ)

text‹\noindent{lCoP3-I}›
lemma "𝔉 ℱ ⟹ lCoP3(❙→) ❙¬⇧I" nitpick oops (*countermodel*)
lemma "lCoP3(❙→) ❙¬⇧I ⟶ TND ❙¬⇧I" unfolding Defs conn by metis
text‹\noindent{lCoP3-C}›
lemma "𝔉 ℱ ⟹ lCoP3(❙→) ❙¬⇧C" nitpick oops (*countermodel*)
lemma "lCoP3(❙→) ❙¬⇧C ⟶ ECQ ❙¬⇧C" unfolding Defs conn by metis


subsection ‹Disjunctive syllogism›

text‹\noindent{DS1-I}›
lemma "DS1(❙→) ❙¬⇧I" using DS1_def ECQ_I ECQ_def unfolding conn by auto
text‹\noindent{DS1-C}›
lemma "𝔉 ℱ ⟹ DS1(❙→) ❙¬⇧C" nitpick oops (*countermodel*)
lemma "DS1(❙→) ❙¬⇧C ⟶ ECQ ❙¬⇧C" unfolding Defs conn by metis

text‹\noindent{DS2-I}›
lemma "𝔉 ℱ ⟹ DS2(❙→) ❙¬⇧I" nitpick oops (*countermodel*)
lemma "DS2(❙→) ❙¬⇧I ⟶ TND ❙¬⇧I" by (simp add: Defs conn)
text‹\noindent{DS2-C}›
lemma "DS2(❙→) ❙¬⇧C" using TND_C unfolding Defs conn by auto

end