Theory topo_strict_implication

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

section ‹Strict implication›

text‹\noindent{We can also employ the closure and interior operations to define different sorts of implications.
In this section we preliminary explore a sort of strict implication and check some relevant properties.}›

text‹\noindent{A 'strict' implication should entail the classical one. Hence we define it using the interior operator.}›
definition imp_I::σσ" (infix "" 51) where "α  β (α  β)"
abbreviation imp_I'::σσ" (infix "" 51) where "β  α  α  β"
declare imp_I_def[conn]

lemma imp_rel: "a b. a  b  a  b" by (simp add: Int_fr_def conn)

text‹\noindent{Under appropriate conditions this implication satisfies a weak variant of the deduction theorem (DT),}›
lemma DTw1: "a b. a  b    a  b" by (simp add: Int_fr_def conn)
lemma DTw2: "Fr_2 ℱ  Fr_3 ℱ  a b.  a  b  a  b  " using IF3 dNOR_def unfolding conn by auto
text‹\noindent{and a variant of modus ponens and modus tollens resp.}›
lemma MP: "a b. a  (a  b)  b" by (simp add: Int_fr_def conn)
lemma MT: "a b. (a  b)  b  a" using MP conn by auto

text‹\noindent{However the full DT (actually right-to-left: implication introduction) is not valid.}›
lemma DT1: "a b X. X  a  b  X  a  b" by (simp add: Int_fr_def conn)
lemma DT2: "𝔉 ℱ  a b X. X  a  b  X  a  b" nitpick oops (*counterexample*)

text‹\noindent{This implication has thus a sort of 'relevant' behaviour. For instance, the following are not valid:}›
lemma "𝔉 ℱ  a b. (a  (b  a))  " nitpick oops (*counterexample*)
lemma "𝔉 ℱ  a b. (a  ((a  b)  b))  " nitpick oops (*counterexample*)
lemma "𝔉 ℱ  a b c. (a  b)  (b  c)  " nitpick oops (*counterexample*)
lemma "𝔉 ℱ  a b. ((a  b)  a)  a  " nitpick oops (*counterexample*) 

text‹\noindent{In contrast the properties below are valid for appropriate conditions.}›
lemma iprop0: "Fr_2 ℱ  Fr_3 ℱ  a. a  a  " using DTw2 pI2 by fastforce
lemma iprop1: "Fr_2 ℱ  Fr_3 ℱ  a b. a  (a  b)  b   " using DTw2 pI2 unfolding conn by fastforce
lemma iprop2: "Fr_2 ℱ  Fr_3 ℱ  a b. a  (b  b)  " using DTw2 pI2 unfolding conn by fastforce
lemma iprop3: "Fr_2 ℱ  Fr_3 ℱ  a b. ((a  a)  b)  b  " using DTw2 pI2 unfolding conn by fastforce
lemma iprop4: "Fr_2 ℱ  Fr_3 ℱ  a b. (a  b)  a  " using DTw2 pI2 unfolding conn by fastforce
lemma iprop5: "Fr_2 ℱ  Fr_3 ℱ  a b. a  (a  b)  " using DTw2 pI2 unfolding conn by fastforce
lemma iprop6a: "Fr_2 ℱ  Fr_3 ℱ  a b c. (a  (b  c))  ((a  b)  (a  c))  " using DTw2 pI2 unfolding conn by fastforce
lemma iprop6b: "Fr_2 ℱ  Fr_3 ℱ  a b c. (a  (b  c))  ((a  b)  (a  c))  " using DTw2 unfolding conn by fastforce

lemma iprop7': "Fr_1 ℱ  a b c. (a  b)  (b  c)  (a  c)" proof -
 assume fr1: "Fr_1 ℱ"
  { fix a b c
    have "(a  b)  (b  c)  (a  c)" unfolding conn by simp
    hence "ℐ((a  b)  (b  c)) (a  c)" using MONO_def PF1 fr1 monI by simp 
    moreover from fr1 have "let A=(a  b); B=(b  c) in(A  B) A B" using IF1 MULT_def by simp
    ultimately have "ℐ(a  b) (b  c) (a  c)" unfolding conn by simp
  } thus ?thesis unfolding conn by blast
qed
lemma iprop7: "Fr_1 ℱ  Fr_2 ℱ  Fr_3 ℱ  a b c. ((a  b)  (b  c))  (a  c)  " by (simp add: DTw2 iprop7')

lemma iprop8a': "Fr_1 ℱ  a b c. (a  b)  (a  c)  a  (b  c)" proof -
  assume fr1: "Fr_1 ℱ"
  { fix a b c
    have "(a  b)  (a  c)  (a  (b  c))" unfolding conn by simp
    hence "ℐ((a  b)  (a  c)) (a  (b  c))" using MONO_def PF1 fr1 monI by simp
    moreover from fr1 have "let A=(a  b); B=(a  c) in(A  B) A B" using IF1 MULT_def by simp
    ultimately have "ℐ(a  b) (a  c) (a  (b  c))" unfolding conn by simp
  } thus ?thesis unfolding conn by simp
qed
lemma iprop8b': "Fr_1b ℱ  a b c. (a  b)  (a  c)  a  (b  c)" by (smt MONO_def monI conn)
lemma iprop8a: "Fr_1 ℱ   Fr_2 ℱ  Fr_3 ℱ  a b c. ((a  b)  (a  c))  (a  (b  c))  " by (simp add: DTw2 iprop8a')
lemma iprop8b: "Fr_1b ℱ  Fr_2 ℱ  Fr_3 ℱ  a b c. ((a  b)  (a  c))  (a  (b  c))  " by (simp add: DTw2 iprop8b')

lemma iprop9a': "Fr_1 ℱ  a b c. ((a  b)  (c  b))  ((a  c)  b)" proof -
  assume fr1: "Fr_1 ℱ"
  { fix a b c
    have "(a  b)  (c  b)  (a  c)  b" unfolding conn by simp
    hence "ℐ((a  b)  (c  b)) ((a  c)  b)" using MONO_def PF1 fr1 monI by simp
    moreover from fr1 have "let A=(a  b); B=(c  b) in(A  B) A B" using IF1 MULT_def by simp
    ultimately have "ℐ(a  b) (c  b) ((a  c)  b)" unfolding conn by simp
  } thus ?thesis unfolding conn by simp
qed
lemma iprop9b': "Fr_1b ℱ  a b c. ((a  b)  (c  b))  ((a  c)  b)" by (smt MONO_def monI conn)
lemma iprop9a: "Fr_1 ℱ   Fr_2 ℱ  Fr_3 ℱ  a b c. ((a  b)  (c  b))  ((a  c)  b)  " by (simp add: DTw2 iprop9a')
lemma iprop9b: "Fr_1b ℱ  Fr_2 ℱ  Fr_3 ℱ  a b c. ((a  b)  (c  b))  ((a  c)  b)  " by (simp add: DTw2 iprop9b')

lemma iprop10': "Fr_1 ℱ  Fr_2 ℱ  Fr_4 ℱ  a b c. a  (b  c)  (a  b)  (a  c)" proof -
  assume fr1: "Fr_1 ℱ" and fr2: "Fr_2 ℱ" and fr4: "Fr_4 ℱ"
  { fix a b c
    have "a  (b  c)  (a  b)  (a  c)" unfolding conn by simp
    hence "a  (b  c)  (a  b)  (a  c)" using Int_fr_def conn by auto
    hence "ℐ(a  (b  c)) ((a  b)  (a  c))" using MONO_def PF1 fr1 monI by simp
    moreover from fr1 have "let A=(a  b); B=(a  c) in(A  B) A B" using IF1 Int_7_def PI7 by auto
    ultimately have "ℐ(a  (b  c)) (a  b) (a  c)" by (metis (full_types))
    hence "ℐ((a  (b  c))) ((a  b) (a  c))" using MONO_def PF1 fr1 monI by simp
    hence "ℐ(a  (b  c)) ((a  b) (a  c))" using Int_Open PF1 fr1 fr2 fr4 by blast
    hence "(a  (b  c))  (a  b)  (a  c)" using Int_Open PF1 fr1 fr2 fr4 unfolding conn by blast
  } thus ?thesis by blast
qed
lemma iprop10: "Fr_1 ℱ  Fr_2 ℱ  Fr_3 ℱ  Fr_4 ℱ  a b c. (a  (b  c))  ((a  b)  (a  c))  " by (simp add: DTw2 iprop10')
lemma "𝔉 ℱ  a b c. a  (b  c)  (a  b)  (a  c)" nitpick oops (*counterexample*)

lemma iprop11a': "Fr_1 ℱ  a b. (a  (a  b))  (a  b)" by (smt MONO_def PF1 imp_rel monI conn)
lemma iprop11b': "𝔉 ℱ     a b. (a  (a  b))  (a  b)" unfolding PF1 by (metis Int_Open MONO_def imp_I_def impl_def monI)
lemma iprop11a: "Fr_1 ℱ  Fr_2 ℱ  Fr_3 ℱ   a b. (a  (a  b))  (a  b)  " using DTw2 iprop11a' by blast
lemma iprop11b: "𝔉 ℱ                             a b. (a  (a  b))  (a  b)  " using DTw2 iprop11b' by blast

text‹\noindent{In particular, 'strenghening the antecedent' is valid only under certain conditions:}›
lemma SA':"Fr_1b ℱ                         a b c.  a  c    (a  b)  c" by (smt MONO_def monI conn)
lemma SA: "Fr_1b ℱ  Fr_2 ℱ  Fr_3 ℱ  a b c. (a  c)  ((a  b)  c)  " using SA' using DTw2 by fastforce 
lemma "Fr_1a ℱ  Fr_2 ℱ  Fr_3 ℱ  Fr_4 ℱ  a b c.  a  c    (a  b)  c" nitpick oops (*counterexample*)
lemma "Fr_1a ℱ  Fr_2 ℱ  Fr_3 ℱ  Fr_4 ℱ  a b c. (a  c)  ((a  b)  c)  " nitpick oops  (*counterexample*)

text‹\noindent{Similarly, 'weakening the consequent' is valid only under certain conditions.}›
lemma WC':"Fr_1b ℱ                         a b c.  a  c    a  (c  b)" by (smt MONO_def monI conn)
lemma WC: "Fr_1b ℱ  Fr_2 ℱ  Fr_3 ℱ  a b c. (a  c)  (a  (c  b))  " using DTw2 WC' by fastforce
lemma "Fr_1a ℱ  Fr_2 ℱ  Fr_3 ℱ  Fr_4 ℱ  a b c.  a  c    a  (c  b)" nitpick oops (*counterexample*)
lemma "Fr_1a ℱ  Fr_2 ℱ  Fr_3 ℱ  Fr_4 ℱ  a b c. (a  c)  (a  (c  b))  " nitpick oops (*counterexample*)

end